ゲーデル《不完全性定理》
1 ：１３２人目の素数さん：
ないので立ててみました。
|
|
|
2 ：１３２人目の素数さん：04/02/05 14:52
ぬるぽ
3 ：１３２人目の素数さん：04/02/05 14:59
基礎論スレッドでやれよ
4 ：１３２人目の素数さん：04/02/05 15:05
いや、あるから。単独の定理スレなんて
作るもんじゃないだろ。
作るもんじゃないだろ。
5 ：１３２人目の素数さん：04/02/05 15:09
すいません。下げます。文系ド素人のもんで。
わからないところがあったので質問したいと思っただけなんです。
すいませんでした。
わからないところがあったので質問したいと思っただけなんです。
すいませんでした。
6 ：１３２人目の素数さん：04/02/05 16:51
>>1
削除依頼だしなさい
削除依頼だしなさい
7 ：１３２人目の素数さん：04/02/05 20:53
不確定性定理と誤読される定理ナンバーワン。
8 ：１３２人目の素数さん：04/02/06 00:33
げー
9 ：１３２人目の素数さん：04/02/06 07:18
10 ：１３２人目の素数さん：04/02/06 19:22
でもまぁ不完全性定理について質問する厨房は多いから、
その基礎論スレからの隔離スレとしては機能するかも。
その基礎論スレからの隔離スレとしては機能するかも。
11 ：１３２人目の素数さん：04/02/06 21:20
有意義なスレになるといいな。
12 ：１３２人目の素数さん：04/02/06 21:24
ゲーデルの不完全性定理
出典: フリー百科事典『ウィキペディア (Wikipedia) 』
ゲーデルの不完全性定理（ - ふかんぜんせいていり、または不完全性定理）は、数学基礎論における重要な定理の一つで、クルト・ゲーデルが1931年に発表した。
第1不完全性定理 自然数論を含む公理系が、無矛盾であれば、内容的には真であるが、証明できない命題が存在する。
第2不完全性定理 自然数論を含む公理系が、無矛盾であれば、自身の無矛盾性を証明できない。
なお、第1不完全性定理の拡張として、証明も反証もできない命題の存在はロッサー (1936) によって示された。また、第2不完全性定理に関して、ロッサーによる証明の定義を用いれば、体系自身の無矛盾性が証明できることが、クライゼル (1960) によって指摘されている。
関連項目
チューリングマシン
チューリングマシンの停止問題
--------------------------------------------------------------------------------
この記事は 書きかけです。この記事を直して下さる協力者を求めています。
出典: フリー百科事典『ウィキペディア (Wikipedia) 』
ゲーデルの不完全性定理（ - ふかんぜんせいていり、または不完全性定理）は、数学基礎論における重要な定理の一つで、クルト・ゲーデルが1931年に発表した。
第1不完全性定理 自然数論を含む公理系が、無矛盾であれば、内容的には真であるが、証明できない命題が存在する。
第2不完全性定理 自然数論を含む公理系が、無矛盾であれば、自身の無矛盾性を証明できない。
なお、第1不完全性定理の拡張として、証明も反証もできない命題の存在はロッサー (1936) によって示された。また、第2不完全性定理に関して、ロッサーによる証明の定義を用いれば、体系自身の無矛盾性が証明できることが、クライゼル (1960) によって指摘されている。
関連項目
チューリングマシン
チューリングマシンの停止問題
--------------------------------------------------------------------------------
この記事は 書きかけです。この記事を直して下さる協力者を求めています。
13 ：１３２人目の素数さん：04/02/07 04:07
おれも,新しい定理を発見したと思ったが,先生が証明が不完全だといったな.
14 ：１３２人目の素数さん：04/02/07 05:39
>>13 ﾜﾛﾀ
15 ：１３２人目の素数さん：04/02/07 09:54
かっこいい定理の名前No.1の「不完全性定理」
16 ：１３２人目の素数さん：04/02/07 16:03
ゲーデルはスコ―レムから何をぱくったんでしょうか？
17 ：１３２人目の素数さん：04/02/07 17:52
18 ：１３２人目の素数さん：04/02/07 23:37
「集合序説」なにげに良書
19 ：１３２人目の素数さん：04/02/07 23:41
ゲーデルはカフカ好きだったらしい
20 ：１３２人目の素数さん：04/02/08 00:02
ゲーデルとカフカって顔が似てません？
21 ：１３２人目の素数さん：04/02/08 00:03
フォン・ノイマンが世界一の天才とか言われたときに「それは私ではなくゲーデルです」と言ったそうな。
22 ：１３２人目の素数さん：04/02/08 00:07
23 ：１３２人目の素数さん：04/02/08 01:03
24 ：１３２人目の素数さん：04/02/08 04:16
25 ：１３２人目の素数さん：04/02/08 07:24
>>20
そうでもないと思う。
そうでもないと思う。
26 ：１３２人目の素数さん：04/02/08 21:31
ヤバイ。不完全性定理ヤバイ。まじでヤバイよ、マジヤバイ。
不完全性定理ヤバイ。
それは超数学。もう数学なんてもんじゃない。超数学。
数学といっても
「鶴亀算20個ぶんくらい？」
とか、もう、そういうレベルじゃない。
何しろ無限を扱う。スゲェ！なんか単位とか無いの。何坪とか何?fとかを超越してる。無限だし超スゴイ。
しかも公理を拡張してるらしい。ヤバイよ、拡張だよ。
だって普通は公理とか拡張しないじゃん。公理が変わってしまうと困るっしょ。
公理が拡張されて昔は1+2=3だったのが、1+2=4とかになったら泣くっしょ。
だから自然数論の公理とか拡張しない。話のわかるヤツだ。
けど不完全性定理はヤバイ。そんなの気にしない。拡張しまくり。しかも、どれだけ拡張しても証明できない数学上の命題がある。ヤバすぎ。
証明できないっていたけど、もしかしたら証明できるかもしんない。でも証明できるってことにすると
「じゃあ、数学上の真の命題の証明が全て完了するのはいつよ？」
って事になるし、それは誰もわからない。ヤバイ。誰にも分からないなんて凄すぎる。
あと超深遠。フォンノイマンも太鼓判。文学で言うとカフカくらい。ヤバイ。深遠すぎ。不条理を感じる間もなく死ぬ。怖い。
なんつっても不完全性定理は内容が凄い。無限とか平気だし。
うちらなんて無限とかたかだか積分計算で出てきただけで上手く扱えないから有限にしたり、fと置いてみたり、演算子使ったりするのに、
不完全性定理は全然平気。無限を無限のまま扱ってる。凄い。ヤバイ。
とにかく貴様ら、不完全性定理のヤバさをもっと知るべきだと思います。
そんな不完全性定理を証明したゲーデルとか超偉い。もっとがんばれ。超がんばれ。
不完全性定理ヤバイ。
それは超数学。もう数学なんてもんじゃない。超数学。
数学といっても
「鶴亀算20個ぶんくらい？」
とか、もう、そういうレベルじゃない。
何しろ無限を扱う。スゲェ！なんか単位とか無いの。何坪とか何?fとかを超越してる。無限だし超スゴイ。
しかも公理を拡張してるらしい。ヤバイよ、拡張だよ。
だって普通は公理とか拡張しないじゃん。公理が変わってしまうと困るっしょ。
公理が拡張されて昔は1+2=3だったのが、1+2=4とかになったら泣くっしょ。
だから自然数論の公理とか拡張しない。話のわかるヤツだ。
けど不完全性定理はヤバイ。そんなの気にしない。拡張しまくり。しかも、どれだけ拡張しても証明できない数学上の命題がある。ヤバすぎ。
証明できないっていたけど、もしかしたら証明できるかもしんない。でも証明できるってことにすると
「じゃあ、数学上の真の命題の証明が全て完了するのはいつよ？」
って事になるし、それは誰もわからない。ヤバイ。誰にも分からないなんて凄すぎる。
あと超深遠。フォンノイマンも太鼓判。文学で言うとカフカくらい。ヤバイ。深遠すぎ。不条理を感じる間もなく死ぬ。怖い。
なんつっても不完全性定理は内容が凄い。無限とか平気だし。
うちらなんて無限とかたかだか積分計算で出てきただけで上手く扱えないから有限にしたり、fと置いてみたり、演算子使ったりするのに、
不完全性定理は全然平気。無限を無限のまま扱ってる。凄い。ヤバイ。
とにかく貴様ら、不完全性定理のヤバさをもっと知るべきだと思います。
そんな不完全性定理を証明したゲーデルとか超偉い。もっとがんばれ。超がんばれ。
27 ：１３２人目の素数さん：04/02/09 01:55
この微妙に間違ったレスはどうすればいいですかね
28 ：１３２人目の素数さん：04/02/09 03:18
>>27
間違いは微妙でもないと思うが、まあ、ネタだし。
間違いは微妙でもないと思うが、まあ、ネタだし。
29 ：１３２人目の素数さん：04/02/09 04:17
>>27-28
添削、というか改良してみては？
添削、というか改良してみては？
30 ：１３２人目の素数さん：04/02/09 05:30
31 ：１３２人目の素数さん：04/02/09 09:18
32 ：１３２人目の素数さん：04/02/09 11:28
ゲ-デルの証明自体が不完全である可能性は?
33 ：１３２人目の素数さん：04/02/09 12:09
>32
それはないそうな。
不完全性定理の証明は、専門家から見ればかなりスッキリしているもののようで、
フェルマーの大定理の証明とかなら、「もしかしてもしかしたら」検証漏れがあるかもしれないけど、
ゲーデルのには、それはないんだって。
それはないそうな。
不完全性定理の証明は、専門家から見ればかなりスッキリしているもののようで、
フェルマーの大定理の証明とかなら、「もしかしてもしかしたら」検証漏れがあるかもしれないけど、
ゲーデルのには、それはないんだって。
34 ：１３２人目の素数さん：04/02/10 23:58
ないだろ。もう何通りも証明が与えられてるんだから。
35 ： ：04/02/11 22:01
連続体仮説の証明ってこの人やったよね。
あれどういうことなの？
あれどういうことなの？
36 ：１３２人目の素数さん：04/02/11 22:22
連続体仮説の証明じゃなくて、一般連続体仮説の相対無矛盾性
の証明でしょ。1938年だっけ。
の証明でしょ。1938年だっけ。
37 ：１３２人目の素数さん：04/02/12 00:24
>>34
上げ取り足のようだけど、32をよく読んでね。
上げ取り足のようだけど、32をよく読んでね。
38 ：１３２人目の素数さん：04/02/12 02:16
Goedel自身の論文はいろんな本に載ってるし、論理学の
基礎的な知識以外要らないから数学や論理学が好きな人は
自分で検証することが出来る。
今までGoedelの証明は実際に何千、何万という人が自分で
読んで確かめただろうから論理的な間違いはないだろう。
基礎的な知識以外要らないから数学や論理学が好きな人は
自分で検証することが出来る。
今までGoedelの証明は実際に何千、何万という人が自分で
読んで確かめただろうから論理的な間違いはないだろう。
39 ：１３２人目の素数さん：04/02/12 07:43
>>32
定理があってるかどうか、というのも厳密には難しいが
38 のいってるような傍証ともいうべきものがある。そして
証明が完全ということになれば正しいということになる。
しかし、数学の定理は余程簡単なことでない限り、完全な証明を
与えることは、なかなか難しい。つまり、形式体系をきめ、その
形式による計算機による検証ができるようなものでも書かなければ
「完全な証明」とはいいにくい。しかし、数学の論文誌に載るよう
な結果の形式的証明が書かれたなんてことはない。不完全性定理
のそのような証明はずっと前に近々つくられるとネットで有名な
先生のホームページに書いてあったけど、それから随分たってるが、
できたという報告はない。
定理があってるかどうか、というのも厳密には難しいが
38 のいってるような傍証ともいうべきものがある。そして
証明が完全ということになれば正しいということになる。
しかし、数学の定理は余程簡単なことでない限り、完全な証明を
与えることは、なかなか難しい。つまり、形式体系をきめ、その
形式による計算機による検証ができるようなものでも書かなければ
「完全な証明」とはいいにくい。しかし、数学の論文誌に載るよう
な結果の形式的証明が書かれたなんてことはない。不完全性定理
のそのような証明はずっと前に近々つくられるとネットで有名な
先生のホームページに書いてあったけど、それから随分たってるが、
できたという報告はない。
40 ：１３２人目の素数さん：04/02/12 21:19
>>39
知ったかぶるなよ。
ゲーデルの不完全性定理の形式的証明は
N.Shankarによって行われている。
Metamathematics, Machines and Godel's Proof
(Cambridge Tracts in Theoretical Computer Science, 38)
知ったかぶるなよ。
ゲーデルの不完全性定理の形式的証明は
N.Shankarによって行われている。
Metamathematics, Machines and Godel's Proof
(Cambridge Tracts in Theoretical Computer Science, 38)
41 ：１３２人目の素数さん：04/02/12 23:56
林先生のページに不完全性定理の或るパターンは
計算機で証明されている、と書いてあるね。
まぁ今はUMLをやっている先生だから数学の人にはあまり
興味はないかも知れんが
計算機で証明されている、と書いてあるね。
まぁ今はUMLをやっている先生だから数学の人にはあまり
興味はないかも知れんが
42 ：１３２人目の素数さん：04/02/13 00:31
これこそ俺の求めてた定理
死ぬまでにこれだけは理解しておきたいと思った
死ぬまでにこれだけは理解しておきたいと思った
43 ：１３２人目の素数さん：04/02/13 22:49
>>40
ずいぶん詳しくごぞんじのようなので伺いたいのですが、
その形式的証明があるゲーデルの不完全性定理というのは
どのような定理なのですか? つまり、「帰納的公理化可能な
任意の形式体系に対して、、、」という部分はどう述べられて
いるのでしょうか? もしこれが、一つの論理式とするとそれは
どういう形式体系の論理式なのでしょうか?
ずいぶん詳しくごぞんじのようなので伺いたいのですが、
その形式的証明があるゲーデルの不完全性定理というのは
どのような定理なのですか? つまり、「帰納的公理化可能な
任意の形式体系に対して、、、」という部分はどう述べられて
いるのでしょうか? もしこれが、一つの論理式とするとそれは
どういう形式体系の論理式なのでしょうか?
44 ：１３２人目の素数さん：04/02/13 23:44
実際人間が直感で理解できる公理系と
帰納的集合である公理系との差ってどれくらいあるんだ？
帰納的集合である公理系との差ってどれくらいあるんだ？
45 ：１３２人目の素数さん：04/02/14 15:28
>>43
形式的な証明の前に、自然言語での証明を理解したほうが…
形式的な証明の前に、自然言語での証明を理解したほうが…
46 ：１３２人目の素数さん：04/02/14 17:24
>>43
ShankarはZ2という二階の算術に対する不完全性定理を証明した。
Z2の公理および証明可能性の具体的定義は>>40の本を見てほしい。
形式化の労力は主にこの点に集中している。
＞「帰納的公理化可能な任意の形式体系に対して、、、」
Shankarの証明はZ2という具体的な公理系の上でのものであるが、
「」内のスタイルのものは、むしろ帰納的関数における不動点定理
の応用として述べられるべきものである。つまり全ての命題について
真とか偽とかを決定しきれるならば、不動点が存在しなくなるから
不動点定理に反するというわけだ。もちろん、不動点は具体的に
構成することができる。ゲーデルの証明のうち、対角線論法に関する
部分は、この不動点の構築方法だと考えられる。
ShankarはZ2という二階の算術に対する不完全性定理を証明した。
Z2の公理および証明可能性の具体的定義は>>40の本を見てほしい。
形式化の労力は主にこの点に集中している。
＞「帰納的公理化可能な任意の形式体系に対して、、、」
Shankarの証明はZ2という具体的な公理系の上でのものであるが、
「」内のスタイルのものは、むしろ帰納的関数における不動点定理
の応用として述べられるべきものである。つまり全ての命題について
真とか偽とかを決定しきれるならば、不動点が存在しなくなるから
不動点定理に反するというわけだ。もちろん、不動点は具体的に
構成することができる。ゲーデルの証明のうち、対角線論法に関する
部分は、この不動点の構築方法だと考えられる。
47 ：１３２人目の素数さん：04/02/14 18:52
>>46
まあ、そういうことだと思いました。
「帰納的公理化可能な任意の形式体系に対して、、、」という形の定理と
すると、「帰納的である」ということの定義を実行する形式体系を用意
しないとひとつの論理式として書くことができません。
ゲーデルの不完全性定理を、40の意味の形のものをいうとすれば、一つの
論理式で書かれたものでなく、色々な形式体系についてひとつづつ論理式
がある、Theorem sheme といったものであると思います。
なお、「このことと不動点、、、」というくだりは全く理解不能です。
まあ、そういうことだと思いました。
「帰納的公理化可能な任意の形式体系に対して、、、」という形の定理と
すると、「帰納的である」ということの定義を実行する形式体系を用意
しないとひとつの論理式として書くことができません。
ゲーデルの不完全性定理を、40の意味の形のものをいうとすれば、一つの
論理式で書かれたものでなく、色々な形式体系についてひとつづつ論理式
がある、Theorem sheme といったものであると思います。
なお、「このことと不動点、、、」というくだりは全く理解不能です。
48 ：１３２人目の素数さん：04/02/14 21:41
49 ：１３２人目の素数さん：04/02/14 22:31
>>48
そうでしょうか？
帰納的関数論での不動点定理といえば、Kleene の Recursion Theorem
であり、その元はゲーデルの対角化定理でしょう。それはいわれるとおり
ですが、43で問題にしてるのは、47にも書いてあるように、「任意の、、、」
というところです。
いま、ある帰納的公理化可能な形式体系、たとえば２階の自然数論のような体系
では「その体系についてのロッサー文が肯定も否定証明できない」ということの
計算機で検証できる証明ができているというのが40の内容であると46に書いてある
と解釈していますが、つまり43の意味でのゲーデルの不完全性定理の形式的証明が
得られているわけではないということだと思います。
そうでしょうか？
帰納的関数論での不動点定理といえば、Kleene の Recursion Theorem
であり、その元はゲーデルの対角化定理でしょう。それはいわれるとおり
ですが、43で問題にしてるのは、47にも書いてあるように、「任意の、、、」
というところです。
いま、ある帰納的公理化可能な形式体系、たとえば２階の自然数論のような体系
では「その体系についてのロッサー文が肯定も否定証明できない」ということの
計算機で検証できる証明ができているというのが40の内容であると46に書いてある
と解釈していますが、つまり43の意味でのゲーデルの不完全性定理の形式的証明が
得られているわけではないということだと思います。
50 ：１３２人目の素数さん：04/02/14 23:17
＞43で問題にしてるのは、47にも書いてあるように、
＞「任意の、、、」 というところです。
だから、何なんだろう？
証明可能性が帰納的関数として記述できればいいだけだろう。
＞「任意の、、、」 というところです。
だから、何なんだろう？
証明可能性が帰納的関数として記述できればいいだけだろう。
51 ：１３２人目の素数さん：04/02/15 16:54
>>50
形式的証明をつくるという話しのとき、「、、、できればいい
だけだろう」って話しではないと思いますがねぇ。
通常、不完全性定理の証明では、このようにして、、、という部分
があるわけで形式的証明をつくるときはそれは許されないから大変
なはずです。
また、一般に具体例に定理を適用する場合では形式的証明を与えよ
うとすると具体例の定義のために厖大な証明が必要なこともある。
だから、形式的証明を与えるということは、かなり大変な作業で
あると思います。原理的にできることであるだけに、どこまでや
ればよいのかわからないようなところもあると思う。41 に書いて
ある、あるパターンは、というのはどの程度の意味かしらないが
どうなんでしょうか? 詳しい方!
形式的証明をつくるという話しのとき、「、、、できればいい
だけだろう」って話しではないと思いますがねぇ。
通常、不完全性定理の証明では、このようにして、、、という部分
があるわけで形式的証明をつくるときはそれは許されないから大変
なはずです。
また、一般に具体例に定理を適用する場合では形式的証明を与えよ
うとすると具体例の定義のために厖大な証明が必要なこともある。
だから、形式的証明を与えるということは、かなり大変な作業で
あると思います。原理的にできることであるだけに、どこまでや
ればよいのかわからないようなところもあると思う。41 に書いて
ある、あるパターンは、というのはどの程度の意味かしらないが
どうなんでしょうか? 詳しい方!
52 ：１３２人目の素数さん：04/02/15 20:42
>>51
君が何を形式的証明と思ってるのかちっとも明らかじゃないから
なんともいいようがないな。
それはともかく、「帰納的公理化可能」というのは、
証明可能性が帰納的述語として表現できることを指す
わけで、一旦それが表現されてしまえば、形式化は
雑作もないことは明らか。
むしろ、困難は、「帰納的公理化可能」を示す点にある。
もちろん、それはわかってていってるんだよな？
君が何を形式的証明と思ってるのかちっとも明らかじゃないから
なんともいいようがないな。
それはともかく、「帰納的公理化可能」というのは、
証明可能性が帰納的述語として表現できることを指す
わけで、一旦それが表現されてしまえば、形式化は
雑作もないことは明らか。
むしろ、困難は、「帰納的公理化可能」を示す点にある。
もちろん、それはわかってていってるんだよな？
53 ：１３２人目の素数さん：04/02/15 20:54
ゲーデルの仕事の最も大変な部分は
「自然数論の形式的体系が、帰納的述語として表現可能」
であることを示す点にある。わかるか？>>43=>>51
それに比べて
「帰納的公理化可能な任意の形式体系に対して、、、」
というのは、それ以後の話だから、むしろ大変な部分を
カットしているわけだ。
「自然数論の形式的体系が、帰納的述語として表現可能」
であることを示す点にある。わかるか？>>43=>>51
それに比べて
「帰納的公理化可能な任意の形式体系に対して、、、」
というのは、それ以後の話だから、むしろ大変な部分を
カットしているわけだ。
54 ：１３２人目の素数さん：04/02/16 21:09
55 ：１３２人目の素数さん：04/02/17 01:02
参上
56 ：１３２人目の素数さん：04/02/18 13:24
初等的な質問をしてもよろしいでしょうか？ 関数についてです。
公理的集合論では関数(写像)はdomainとcodomainが決まっていて、
しかも関数自体が集合だから、はっきりと理解できるんですが、
一般の数学基礎論ではdomainやcodomainが大きすぎるような気がするし、
例えば、[P(x)≡x>1]という関数Pを定めるといっても、Pが何なんのかよく分かりません。
どのように理解した良いんでしょうか？
公理的集合論では関数(写像)はdomainとcodomainが決まっていて、
しかも関数自体が集合だから、はっきりと理解できるんですが、
一般の数学基礎論ではdomainやcodomainが大きすぎるような気がするし、
例えば、[P(x)≡x>1]という関数Pを定めるといっても、Pが何なんのかよく分かりません。
どのように理解した良いんでしょうか？
57 ：１３２人目の素数さん：04/02/19 18:12
>>56
他のスレッドの方がよいのでしょうが、簡単に書きます。
公理的集合論では関数(写像)は一般には集合ではありません、クラス
と呼ばれます。これの定義域を集合に限ると値域が集合になるという
のが置換公理と呼ばれているものです。
また P(x)≡x>1 で定められる P は述語であり、関数ではありません。
他のスレッドの方がよいのでしょうが、簡単に書きます。
公理的集合論では関数(写像)は一般には集合ではありません、クラス
と呼ばれます。これの定義域を集合に限ると値域が集合になるという
のが置換公理と呼ばれているものです。
また P(x)≡x>1 で定められる P は述語であり、関数ではありません。
58 ：１３２人目の素数さん：04/02/19 22:33
>>52
お詳しいかたのようなので単なるいい間違いなのでしょうが証明可能性は一般に
帰納的ではなく、帰納枚挙的（recursively enumerable）です。そして「表現可能」
という言葉が不完全性定理の関係で使われるときは numeralwise expressible という
ことをいっているのが普通だと思うのですが、そのとき、53にあるようないいかた
ってあるのでしょうか？
たとえば、ペアノの自然数論において論理式の列が証明であるか、ないかは帰納的
であり numeralwise expressible です。一方、論理式の証明可能性は帰納枚挙的
ですが numeralwise expressible ではありません。
昨年の今ごろ、高名なネット数学者であり不完全性定理の権威者でもあるマツシンと
いう方が numeralwise expressible という不完全性定理では極めて大切な概念を
理解していなかったことが発覚しました。ですから、随分詳しい >>52 のような方
でも、理解していないということなのでしょうか？
43で問題としているのは、計算機で検証するとき証明というものがある書式で
書かれるわけでしょうが、その結論となる論理式は何か？ということを聞いて
いるのです。その説明は47に書いてありますから、新たに説明はいたしません、
お詳しい方には、興味のないことのようですね。お詳しい方の興味は、私に
不完全性定理について教えて下さることのようです、しかしそれは無理でしょう。
お詳しいかたのようなので単なるいい間違いなのでしょうが証明可能性は一般に
帰納的ではなく、帰納枚挙的（recursively enumerable）です。そして「表現可能」
という言葉が不完全性定理の関係で使われるときは numeralwise expressible という
ことをいっているのが普通だと思うのですが、そのとき、53にあるようないいかた
ってあるのでしょうか？
たとえば、ペアノの自然数論において論理式の列が証明であるか、ないかは帰納的
であり numeralwise expressible です。一方、論理式の証明可能性は帰納枚挙的
ですが numeralwise expressible ではありません。
昨年の今ごろ、高名なネット数学者であり不完全性定理の権威者でもあるマツシンと
いう方が numeralwise expressible という不完全性定理では極めて大切な概念を
理解していなかったことが発覚しました。ですから、随分詳しい >>52 のような方
でも、理解していないということなのでしょうか？
43で問題としているのは、計算機で検証するとき証明というものがある書式で
書かれるわけでしょうが、その結論となる論理式は何か？ということを聞いて
いるのです。その説明は47に書いてありますから、新たに説明はいたしません、
お詳しい方には、興味のないことのようですね。お詳しい方の興味は、私に
不完全性定理について教えて下さることのようです、しかしそれは無理でしょう。
59 ：１３２人目の素数さん：04/02/20 09:28
＞証明可能性は一般に帰納的ではなく、
＞帰納枚挙的（recursively enumerable）です。
では
「論理式の列が証明であるか、ないか」
と訂正しておいてくれたまえ。
ここではrecursively enumerableについては議論していないので、
君が求めるような「精密な云い回し」を用いる必要性を感じない。
現に君はちゃんと言い直せた。それが証拠。
マツシンとかいう人は私と同様のことをやったのかもしれないが
そうだとすれば気の毒な人だ。
無意味に厳密性を振りまわす場合、大抵、本筋が見えていない。
＞帰納枚挙的（recursively enumerable）です。
では
「論理式の列が証明であるか、ないか」
と訂正しておいてくれたまえ。
ここではrecursively enumerableについては議論していないので、
君が求めるような「精密な云い回し」を用いる必要性を感じない。
現に君はちゃんと言い直せた。それが証拠。
マツシンとかいう人は私と同様のことをやったのかもしれないが
そうだとすれば気の毒な人だ。
無意味に厳密性を振りまわす場合、大抵、本筋が見えていない。
60 ：１３２人目の素数さん：04/02/20 09:37
＞43で問題としているのは、計算機で検証するとき証明というものが
＞ある書式で書かれるわけでしょうが、その結論となる論理式は何か？
＞ということを聞いているのです。
その答は46に書かれていると思う。
そして47はそれで納得したのではないのかな？。
＞その説明は47に書いてありますから、新たに説明はいたしません
＞「帰納的公理化可能な任意の形式体系に対して、、、」
＞という形の定理とすると、「帰納的である」ということの
＞定義を実行する形式体系を用意しないと
＞ひとつの論理式として書くことができません。
ごもっともだが…
ところで、君は一度でもゲーデルの証明を読んだことがあるのかい？
もし一度でも読んだことがあるのなら、そもそも43でいうような
「「帰納的である」ということの（完全な）定義」
を詮索することが無駄であると分かる筈だが、違うかい？
それとも無駄と分かっていて他人に駄々をこねているのかい？
＞ある書式で書かれるわけでしょうが、その結論となる論理式は何か？
＞ということを聞いているのです。
その答は46に書かれていると思う。
そして47はそれで納得したのではないのかな？。
＞その説明は47に書いてありますから、新たに説明はいたしません
＞「帰納的公理化可能な任意の形式体系に対して、、、」
＞という形の定理とすると、「帰納的である」ということの
＞定義を実行する形式体系を用意しないと
＞ひとつの論理式として書くことができません。
ごもっともだが…
ところで、君は一度でもゲーデルの証明を読んだことがあるのかい？
もし一度でも読んだことがあるのなら、そもそも43でいうような
「「帰納的である」ということの（完全な）定義」
を詮索することが無駄であると分かる筈だが、違うかい？
それとも無駄と分かっていて他人に駄々をこねているのかい？
61 ：１３２人目の素数さん：04/02/20 09:44
＞ゲーデルの不完全性定理を、40の意味の形のものをいうとすれば、
＞一つの論理式で書かれたものでなく、色々な形式体系について
＞ひとつづつ論理式がある、Theorem sheme といったものである
＞と思います。
shemeはschemeの打ち間違いだな。
50は上の文章を否定してはいない。
要は証明判定が帰納的関数として記述できればいい。
君のようにルイス・キャロルのパラドックスに
まともにドップリはまることに何の意義があるのかな？
＞一つの論理式で書かれたものでなく、色々な形式体系について
＞ひとつづつ論理式がある、Theorem sheme といったものである
＞と思います。
shemeはschemeの打ち間違いだな。
50は上の文章を否定してはいない。
要は証明判定が帰納的関数として記述できればいい。
君のようにルイス・キャロルのパラドックスに
まともにドップリはまることに何の意義があるのかな？
62 ：１３２人目の素数さん：04/02/20 09:57
>>39
＞しかし、数学の論文誌に載るような結果の
＞形式的証明が書かれたなんてことはない。
「数学の論文誌に載るような結果」が
君が43と47でいう
「帰納的公理化可能な任意の形式体系に対して…」
か。
証明可能性云々につっこむ前に君自身の文章を
明確にするべきだったな。これは議論の重要な
ポイントだ。
＞不完全性定理のそのような証明はずっと前に近々つくられると
＞ネットで有名な先生のホームページに書いてあったけど、
＞それから随分たってるが、できたという報告はない。
誰がいつどこでそういうことを言ったのかは興味があるが
それはともかく、数学者が望む証明は、君がいうような
ものとは異なる。
＞しかし、数学の論文誌に載るような結果の
＞形式的証明が書かれたなんてことはない。
「数学の論文誌に載るような結果」が
君が43と47でいう
「帰納的公理化可能な任意の形式体系に対して…」
か。
証明可能性云々につっこむ前に君自身の文章を
明確にするべきだったな。これは議論の重要な
ポイントだ。
＞不完全性定理のそのような証明はずっと前に近々つくられると
＞ネットで有名な先生のホームページに書いてあったけど、
＞それから随分たってるが、できたという報告はない。
誰がいつどこでそういうことを言ったのかは興味があるが
それはともかく、数学者が望む証明は、君がいうような
ものとは異なる。
63 ：１３２人目の素数さん：04/02/20 11:39
>>62
＞「数学の論文誌に載るような結果」が
＞君が43と47でいう
＞「帰納的公理化可能な任意の形式体系に対して…」
＞か。
これって Kleene の定理だったような。
(もうちょっと強い主張だったかも)
＞「数学の論文誌に載るような結果」が
＞君が43と47でいう
＞「帰納的公理化可能な任意の形式体系に対して…」
＞か。
これって Kleene の定理だったような。
(もうちょっと強い主張だったかも)
64 ：１３２人目の素数さん：04/02/20 11:42
>>49
＞帰納的関数論での不動点定理といえば、
＞Kleene の Recursion Theoremであり、
＞その元はゲーデルの対角化定理でしょう。
＞それはいわれるとおりですが
なら、何もいうことはないね。
（終）
＞帰納的関数論での不動点定理といえば、
＞Kleene の Recursion Theoremであり、
＞その元はゲーデルの対角化定理でしょう。
＞それはいわれるとおりですが
なら、何もいうことはないね。
（終）
65 ：１３２人目の素数さん：04/02/21 21:06
うーん、やっぱりそうなんじゃないかなぁー?
お詳しい方って、マツシンっていわれてるネット数学の有名人なん
じゃないのぉー? 前にゲーデルBBS で叩かれてそこでちょっと2 階
の論理を学んで、1 年前に表現可能ってのを学んで、でも結局ちっと
もわかっちゃいないってことなんだよね。まあ、以前よりはわかって
はきてるんだろうけど、そういうのって、よくわかることにつながら
ないんだよねぇー。マツシンっていわれてる方じゃないんなら、まあ
おんなじような人ってことなんだろうけど、でも、あんまり人に教え
ようとしない方がいいと思うよぉー、やめられないんだろうけど。
お詳しい方って、マツシンっていわれてるネット数学の有名人なん
じゃないのぉー? 前にゲーデルBBS で叩かれてそこでちょっと2 階
の論理を学んで、1 年前に表現可能ってのを学んで、でも結局ちっと
もわかっちゃいないってことなんだよね。まあ、以前よりはわかって
はきてるんだろうけど、そういうのって、よくわかることにつながら
ないんだよねぇー。マツシンっていわれてる方じゃないんなら、まあ
おんなじような人ってことなんだろうけど、でも、あんまり人に教え
ようとしない方がいいと思うよぉー、やめられないんだろうけど。
66 ：１３２人目の素数さん：04/02/24 10:17
でもでもー、お詳しい方っていってる人もー、
お詳しい方と同レベルなんじゃないのぉー？
形式化の話なのに、numeralwise expressibleなんて
いっちゃうのはぜんぜんわかっちゃいないってこと
なんだよねー。ま、本人は、わかってるつもりなんだろう
けどー、そういうのって、ただ字面だけ追ってるだけ
なんだよねぇー。ま、あんまり得意になって語らない
ほうがいいと思うよぉー。まぁ、マツシンにどうしても
勝ちたいんだろうけど。
お詳しい方と同レベルなんじゃないのぉー？
形式化の話なのに、numeralwise expressibleなんて
いっちゃうのはぜんぜんわかっちゃいないってこと
なんだよねー。ま、本人は、わかってるつもりなんだろう
けどー、そういうのって、ただ字面だけ追ってるだけ
なんだよねぇー。ま、あんまり得意になって語らない
ほうがいいと思うよぉー。まぁ、マツシンにどうしても
勝ちたいんだろうけど。
67 ：１３２人目の素数さん：04/02/24 10:41
03/03/12 07:42
「表現可能性というのは semantics と syntax をつなぐ関係である。
この関係の成立の証明がどのような形式体系で実行できるかをみて
これを形式体系(syntax) で実行した結果を使うと第2不完全性定理が
みちびかれる。」
パシャ パシャ パシャ パシャ パシャ パシャ パシャ パシャ パシャ パシャ パシャ
パシャ パシャ パシャ パシャ パシャ パシャ パシャ パシャ パシャ パシャ
∧_∧ ∧_∧ ∧_∧ ∧_∧ ∧_∧ ∧_∧
( )】 ( )】 ( )】 【( ) 【( ) 【( )
/ /┘ . / /┘. / /┘ └＼＼ └＼＼ └＼＼
ノ￣ゝ ノ￣ゝ ノ￣ゝ ノ￣ゝ ノ￣ゝ ノ￣ゝ
「表現可能性というのは semantics と syntax をつなぐ関係である。
この関係の成立の証明がどのような形式体系で実行できるかをみて
これを形式体系(syntax) で実行した結果を使うと第2不完全性定理が
みちびかれる。」
パシャ パシャ パシャ パシャ パシャ パシャ パシャ パシャ パシャ パシャ パシャ
パシャ パシャ パシャ パシャ パシャ パシャ パシャ パシャ パシャ パシャ
∧_∧ ∧_∧ ∧_∧ ∧_∧ ∧_∧ ∧_∧
( )】 ( )】 ( )】 【( ) 【( ) 【( )
/ /┘ . / /┘. / /┘ └＼＼ └＼＼ └＼＼
ノ￣ゝ ノ￣ゝ ノ￣ゝ ノ￣ゝ ノ￣ゝ ノ￣ゝ
68 ：１３２人目の素数さん：04/02/24 10:49
03/03/13 07:14
「semantics と syntax をつなぐ関係というのは同値という意味ではない。
述語 R の表現可能性ということだが、不完全性定理に関し、
この概念を使う R は原始帰納的述語である。
さてこの述語の主語となる自然数というのはどこにあるものか？
ということを考える。
すると、これは自分のものを考えている場にあるものだと気づく。
つぎに述語 R からどのように論理式 phi をつくるかということ、
そして第２不完全性定理の証明でこの表現可能性が成立していることを
論理式で書くことを考えれば、R に何らかの論理式が対応していないと
そのようなことが実行できないことがわかる。」
パシャ パシャ パシャ パシャ パシャ パシャ パシャ パシャ パシャ パシャ パシャ
パシャ パシャ パシャ パシャ パシャ パシャ パシャ パシャ パシャ パシャ
∧_∧ ∧_∧ ∧_∧ ∧_∧ ∧_∧ ∧_∧
( )】 ( )】 ( )】 【( ) 【( ) 【( )
/ /┘ . / /┘. / /┘ └＼＼ └＼＼ └＼＼
ノ￣ゝ ノ￣ゝ ノ￣ゝ ノ￣ゝ ノ￣ゝ ノ￣ゝ
「semantics と syntax をつなぐ関係というのは同値という意味ではない。
述語 R の表現可能性ということだが、不完全性定理に関し、
この概念を使う R は原始帰納的述語である。
さてこの述語の主語となる自然数というのはどこにあるものか？
ということを考える。
すると、これは自分のものを考えている場にあるものだと気づく。
つぎに述語 R からどのように論理式 phi をつくるかということ、
そして第２不完全性定理の証明でこの表現可能性が成立していることを
論理式で書くことを考えれば、R に何らかの論理式が対応していないと
そのようなことが実行できないことがわかる。」
パシャ パシャ パシャ パシャ パシャ パシャ パシャ パシャ パシャ パシャ パシャ
パシャ パシャ パシャ パシャ パシャ パシャ パシャ パシャ パシャ パシャ
∧_∧ ∧_∧ ∧_∧ ∧_∧ ∧_∧ ∧_∧
( )】 ( )】 ( )】 【( ) 【( ) 【( )
/ /┘ . / /┘. / /┘ └＼＼ └＼＼ └＼＼
ノ￣ゝ ノ￣ゝ ノ￣ゝ ノ￣ゝ ノ￣ゝ ノ￣ゝ
69 ：１３２人目の素数さん：04/02/24 10:58
03/03/14 07:13
「”＜自然数上のｋ項関係（述語）Ｒ(n_1,…,n_k)のＴにおける表現可能性＞
・Ｒ(n_1,…,n_k)が成り立つときにはＴ |- φ(n_1,…,n_k)
・Ｒ(n_1,…,n_k)が成り立たないときにはＴ |- ¬φ(n_1,…,n_k)
を満たす論理式φ(x_1,…,x_k)が存在する”
は semantics における x_i と対応するsyntax の numeral が
同じ記号となっているが印刷物では間違わないように
違う字体の文字あるいは下線、上線などを使う。
しかし、これはその定義を意味あるものとして理解しようとすれば、
これ以外の理解はできないものである。」
パシャ パシャ パシャ パシャ パシャ パシャ パシャ パシャ パシャ パシャ パシャ
パシャ パシャ パシャ パシャ パシャ パシャ パシャ パシャ パシャ パシャ
∧_∧ ∧_∧ ∧_∧ ∧_∧ ∧_∧ ∧_∧
( )】 ( )】 ( )】 【( ) 【( ) 【( )
/ /┘ . / /┘. / /┘ └＼＼ └＼＼ └＼＼
ノ￣ゝ ノ￣ゝ ノ￣ゝ ノ￣ゝ ノ￣ゝ ノ￣ゝ
「”＜自然数上のｋ項関係（述語）Ｒ(n_1,…,n_k)のＴにおける表現可能性＞
・Ｒ(n_1,…,n_k)が成り立つときにはＴ |- φ(n_1,…,n_k)
・Ｒ(n_1,…,n_k)が成り立たないときにはＴ |- ¬φ(n_1,…,n_k)
を満たす論理式φ(x_1,…,x_k)が存在する”
は semantics における x_i と対応するsyntax の numeral が
同じ記号となっているが印刷物では間違わないように
違う字体の文字あるいは下線、上線などを使う。
しかし、これはその定義を意味あるものとして理解しようとすれば、
これ以外の理解はできないものである。」
パシャ パシャ パシャ パシャ パシャ パシャ パシャ パシャ パシャ パシャ パシャ
パシャ パシャ パシャ パシャ パシャ パシャ パシャ パシャ パシャ パシャ
∧_∧ ∧_∧ ∧_∧ ∧_∧ ∧_∧ ∧_∧
( )】 ( )】 ( )】 【( ) 【( ) 【( )
/ /┘ . / /┘. / /┘ └＼＼ └＼＼ └＼＼
ノ￣ゝ ノ￣ゝ ノ￣ゝ ノ￣ゝ ノ￣ゝ ノ￣ゝ
70 ：１３２人目の素数さん：04/02/26 22:10
67-69 はとても 66 やお詳しい方が書いたものとは思えないから、どこから
かのコピーなのだろうけど、もし、マツシンという方だとしたら、このような
コピーができるようになっただけ去年よりだいぶ進歩したってことなんだろうね。
かのコピーなのだろうけど、もし、マツシンという方だとしたら、このような
コピーができるようになっただけ去年よりだいぶ進歩したってことなんだろうね。
71 ：１３２人目の素数さん：04/02/27 10:43
>>70
パシャ パシャ パシャ パシャ パシャ パシャ パシャ パシャ パシャ パシャ パシャ
パシャ パシャ パシャ パシャ パシャ パシャ パシャ パシャ パシャ パシャ
∧_∧ ∧_∧ ∧_∧ ∧_∧ ∧_∧ ∧_∧
( )】 ( )】 ( )】 【( ) 【( ) 【( )
/ /┘ . / /┘. / /┘ └＼＼ └＼＼ └＼＼
ノ￣ゝ ノ￣ゝ ノ￣ゝ ノ￣ゝ ノ￣ゝ ノ￣ゝ
パシャ パシャ パシャ パシャ パシャ パシャ パシャ パシャ パシャ パシャ パシャ
パシャ パシャ パシャ パシャ パシャ パシャ パシャ パシャ パシャ パシャ
∧_∧ ∧_∧ ∧_∧ ∧_∧ ∧_∧ ∧_∧
( )】 ( )】 ( )】 【( ) 【( ) 【( )
/ /┘ . / /┘. / /┘ └＼＼ └＼＼ └＼＼
ノ￣ゝ ノ￣ゝ ノ￣ゝ ノ￣ゝ ノ￣ゝ ノ￣ゝ
72 ：１３２人目の素数さん：04/02/29 09:35
ふーん、マツシンも進歩してるんだ、コピーの選び方が!
73 ：１３２人目の素数さん：04/02/29 15:22
74 ：１３２人目の素数さん：04/03/03 11:44
ふーん、じゃマツシンって進歩してないんだ。
75 ：１３２人目の素数さん：04/03/05 08:51
76 ：１３２人目の素数さん：04/03/06 06:49
>>75
それじゃー、形式化がうまくいってるかどうかって判定は全く
個人個人の判断にまかせるってことになっちゃうんじゃないのー?
ある性質を論理式で書いたとき、うまく書けているかどうかを
numeralwise expressible で判断するんだから、これって形式化が
うまくできってるかどうか? ってことじゃないのー?
お詳しいかたー?
それじゃー、形式化がうまくいってるかどうかって判定は全く
個人個人の判断にまかせるってことになっちゃうんじゃないのー?
ある性質を論理式で書いたとき、うまく書けているかどうかを
numeralwise expressible で判断するんだから、これって形式化が
うまくできってるかどうか? ってことじゃないのー?
お詳しいかたー?
77 ：１３２人目の素数さん：04/03/06 10:02
>>76
＞ある性質を論理式で書いたとき、うまく書けているかどうか
＞numeralwise expressible で判断するんだから
ﾜﾗﾀ
76は帰納的でない述語は「うまく書けてない」というそうだ(ﾌﾟ
＞ある性質を論理式で書いたとき、うまく書けているかどうか
＞numeralwise expressible で判断するんだから
ﾜﾗﾀ
76は帰納的でない述語は「うまく書けてない」というそうだ(ﾌﾟ
78 ：１３２人目の素数さん：04/03/06 12:26
79 ：１３２人目の素数さん：04/03/06 16:38
>>78
ﾃﾞﾑﾊﾟですか？
ﾃﾞﾑﾊﾟですか？
80 ：１３２人目の素数さん：04/03/07 19:06
>>79
それはどうかなぁー?
例えば、証明図をコード化して a より小さいところに PA から矛盾
に至る証明図があるってことを考えるとき、これって PA でうまく
書けるのぉー?
もっと簡単に a < a+1 って 1 足したら大きくなることだっていう
ことをうまく書いているっていうのはどうやっていうのぉー?
お詳しいかたー?
それはどうかなぁー?
例えば、証明図をコード化して a より小さいところに PA から矛盾
に至る証明図があるってことを考えるとき、これって PA でうまく
書けるのぉー?
もっと簡単に a < a+1 って 1 足したら大きくなることだっていう
ことをうまく書いているっていうのはどうやっていうのぉー?
お詳しいかたー?
81 ：１３２人目の素数さん：04/03/07 23:22
とりあえず
逝 っ て よ し
逝 っ て よ し
82 ：１３２人目の素数さん：04/03/08 16:41
>>80
ﾃﾞﾑﾊﾟですな
ﾃﾞﾑﾊﾟですな
83 ：１３２人目の素数さん：04/03/08 22:36
どうもよくわかってないようだね。
なんで、表現可能とか、numeralwise expressible とかいわれるん
だか考えてごらん？
マツシンとそのご親戚のみなさん！
なんで、表現可能とか、numeralwise expressible とかいわれるん
だか考えてごらん？
マツシンとそのご親戚のみなさん！
84 ：１３２人目の素数さん：04/03/09 11:53
85 ：１３２人目の素数さん ：04/03/09 14:12
age
86 ：１３２人目の素数さん：04/03/15 20:03
"真である命題か否か"は証明によってのみ決められる。
としておけば、不完全性定理は破壊される。
としておけば、不完全性定理は破壊される。
87 ：１３２人目の素数さん：04/03/16 02:11
>>86
そうでもないと思うけど？不完全性定理のG\"odelオリジナルの
証明では、真理概念は極力使わないようにすることが出来る。
（そのせいか、真理概念を積極的に用いた証明を、毛嫌いする
日本の数学者もいる）或いは、直観主義（数学の定理は先験的な真理
ではなく、数学者の精神の賜である、と言う考え方）見たいな事を
考えているのかも知れないけど、ゲーデルは、彼自身が論文中で
述べているように「構成的」な証明を行っていて、特定の公理系が
与えられれば、それ自体もその否定も証明できないような命題を
構成することが出来る。不完全性定理を拒否する為には、数学の
公理化というEuclidの時代からの考え方を手放さなくてはならない。
（Brouwerはそもそも公理化自体を否定しているらしいけどね。）
ついでに、下のリンク先に的確な解説があるので、貼っときます。
昨年の春〜夏は直観主義に対して、ある種の憧れを持ってました。
ttp://ja.wikipedia.org/wiki/%E6%95%B0%E5%AD%A6%E7%9A%84%E7%9B%B4%E8%A6%B3%E4%B8%BB%E7%BE%A9
そうでもないと思うけど？不完全性定理のG\"odelオリジナルの
証明では、真理概念は極力使わないようにすることが出来る。
（そのせいか、真理概念を積極的に用いた証明を、毛嫌いする
日本の数学者もいる）或いは、直観主義（数学の定理は先験的な真理
ではなく、数学者の精神の賜である、と言う考え方）見たいな事を
考えているのかも知れないけど、ゲーデルは、彼自身が論文中で
述べているように「構成的」な証明を行っていて、特定の公理系が
与えられれば、それ自体もその否定も証明できないような命題を
構成することが出来る。不完全性定理を拒否する為には、数学の
公理化というEuclidの時代からの考え方を手放さなくてはならない。
（Brouwerはそもそも公理化自体を否定しているらしいけどね。）
ついでに、下のリンク先に的確な解説があるので、貼っときます。
昨年の春〜夏は直観主義に対して、ある種の憧れを持ってました。
ttp://ja.wikipedia.org/wiki/%E6%95%B0%E5%AD%A6%E7%9A%84%E7%9B%B4%E8%A6%B3%E4%B8%BB%E7%BE%A9
88 ：１３２人目の素数さん：04/03/16 02:20
「見たいな」→「みたいな」
要するに、第一不完全性定理の言明は「直観的に真であるのに
証明できない命題が存在する」と言ってもいいが、別に
「それ自体もその否定も証明可能でない命題が存在する。
（具体的に構成できる）」といってもいいんだよ、ということ。
これなら「真」==「証明可能」と定義しても第一定理は
そのまま成立する。
要するに、第一不完全性定理の言明は「直観的に真であるのに
証明できない命題が存在する」と言ってもいいが、別に
「それ自体もその否定も証明可能でない命題が存在する。
（具体的に構成できる）」といってもいいんだよ、ということ。
これなら「真」==「証明可能」と定義しても第一定理は
そのまま成立する。
89 ：１３２人目の素数さん：04/03/16 14:52
そうか、不完全性定理って"真偽を証明できない命題が存在する"ってことだもんな。
ありがとう。
ありがとう。
90 ：晩年のゲーデル：04/03/25 22:55
http://i.timeinc.net/time/time100/scientist/images/profilepix/goedel.jpg
http://www.stauff.de/matgesch/bilder/goedel.jpg
http://www.stauff.de/matgesch/bilder/goedel.jpg
91 ：１３２人目の素数さん：04/03/25 23:15
>>89
「その公理系が無矛盾であれば」っていう条件が必要だよ
「その公理系が無矛盾であれば」っていう条件が必要だよ
92 ：エレガントな解答求む。：04/03/26 00:36
あほですか。
＞"真である命題か否か"は証明によってのみ決められる。
としておけば、不完全性定理は破壊される。
"真である命題か否か"は証明によってのみ決められる。"ということの
反証でしょうが。
＞"真である命題か否か"は証明によってのみ決められる。
としておけば、不完全性定理は破壊される。
"真である命題か否か"は証明によってのみ決められる。"ということの
反証でしょうが。
93 ：１３２人目の素数さん：04/03/26 00:39
"真か否か"は証明によって「完全に」決められる
と言うことの反証であるような。
と言うことの反証であるような。
94 ：エレガントな解答求む。：04/03/26 00:52
御意。すまん。＞93
95 ：１３２人目の素数さん：04/03/26 13:04
適当に解釈して、俺の考え↓
>"真である命題か否か"は証明によってのみ決められる"
というのは、
[真の定義]
任意の命題Aが証明可能であるとき、Aを真であるという。
[偽の定義]
任意の命題Aが反証可能であるとき、Aを偽であるという。
という公理系において不完全性定理が成り立つか?
ということとする。
ゲーデルは
"あらゆる公理系に証明も反証も不可能な命題がある" ……[1]
ことを示しただけだから、帰結は二通り。
(i)上の公理系に、"すべての命題は真か偽のどちらかである"という公理がある場合
上の真偽の定義と不完全性定理により、真でも偽でもない命題が存在することが示されたので、上の公理系は矛盾を含んでいる。
∴ この場合は"真である命題か否かは証明によってのみ決められる。"という公理が他の公理と整合性がないことの証明になる。
∴ >>92は正しい
(ii)上の公理系に、"すべての命題は真か偽のどちらかである"という公理がない場合
系 "真でも偽でもない命題が存在する"
が得られる。
∴ この場合は「"真である命題か否か"は証明によってのみ決められる。"ということの反証」にならない。
∴ >>92は間違い
と思うのだが、いかがでしょうか。
>"真である命題か否か"は証明によってのみ決められる"
というのは、
[真の定義]
任意の命題Aが証明可能であるとき、Aを真であるという。
[偽の定義]
任意の命題Aが反証可能であるとき、Aを偽であるという。
という公理系において不完全性定理が成り立つか?
ということとする。
ゲーデルは
"あらゆる公理系に証明も反証も不可能な命題がある" ……[1]
ことを示しただけだから、帰結は二通り。
(i)上の公理系に、"すべての命題は真か偽のどちらかである"という公理がある場合
上の真偽の定義と不完全性定理により、真でも偽でもない命題が存在することが示されたので、上の公理系は矛盾を含んでいる。
∴ この場合は"真である命題か否かは証明によってのみ決められる。"という公理が他の公理と整合性がないことの証明になる。
∴ >>92は正しい
(ii)上の公理系に、"すべての命題は真か偽のどちらかである"という公理がない場合
系 "真でも偽でもない命題が存在する"
が得られる。
∴ この場合は「"真である命題か否か"は証明によってのみ決められる。"ということの反証」にならない。
∴ >>92は間違い
と思うのだが、いかがでしょうか。
96 ：１３２人目の素数さん：04/03/27 10:59
97 ：１３２人目の素数さん：04/03/27 17:02
>>95
適当に解釈しすぎ
適当に解釈しすぎ
98 ：１３２人目の素数さん：04/03/27 21:41
>>96
どういう前提においての話なんだ?
(x) 任意の命題Aは証明、反証の可能性に関わらず真、偽のどちらかである とする場合 (こっちが普通の公理系だと思う
"証明できない"ことは真、偽に関係ない
∴ >>96は誤り
(xx)>>95で示された、[真偽の定義]による場合
Gは証明できないから、真の定義より、Gは真でない。
∴ >>96は正しい
[注意]
一応、釘を刺しておく。これは決して"Gが偽である"ということを示していない。
何故ならば公理系(ii)においては"真でも偽でもない命題が存在する"から、。
--俺が主張したかったこと--
"証明、反証の可能性に関わらず命題には真、偽がある"
とする一般的な見方ではなく、
"証明可能ならば真、証明不可能ならば偽である"
という定義をした場合、不完全性定理の帰結は"真でも偽でも命題が存在する"となる、と言いたかったわけ。
蛇足 この定義を押し通そうとするなら、当然"命題は真か偽のどちらかである"という一般的な公理を捨て去らねばならぬ。
どちらにしても>>86は誤り。
>>97
じゃあ"適当じゃない解釈"について語れ。
どういう前提においての話なんだ?
(x) 任意の命題Aは証明、反証の可能性に関わらず真、偽のどちらかである とする場合 (こっちが普通の公理系だと思う
"証明できない"ことは真、偽に関係ない
∴ >>96は誤り
(xx)>>95で示された、[真偽の定義]による場合
Gは証明できないから、真の定義より、Gは真でない。
∴ >>96は正しい
[注意]
一応、釘を刺しておく。これは決して"Gが偽である"ということを示していない。
何故ならば公理系(ii)においては"真でも偽でもない命題が存在する"から、。
--俺が主張したかったこと--
"証明、反証の可能性に関わらず命題には真、偽がある"
とする一般的な見方ではなく、
"証明可能ならば真、証明不可能ならば偽である"
という定義をした場合、不完全性定理の帰結は"真でも偽でも命題が存在する"となる、と言いたかったわけ。
蛇足 この定義を押し通そうとするなら、当然"命題は真か偽のどちらかである"という一般的な公理を捨て去らねばならぬ。
どちらにしても>>86は誤り。
>>97
じゃあ"適当じゃない解釈"について語れ。
99 ：１３２人目の素数さん：04/03/28 18:14
直観主義論理でも勉強したら？
任意の命題は真または偽、が成り立たない
（証明に使ってはいけない）世界だから
解釈も何も、命題の真偽はその公理系で定義するような
事柄ではありません。
任意の命題は真または偽、が成り立たない
（証明に使ってはいけない）世界だから
解釈も何も、命題の真偽はその公理系で定義するような
事柄ではありません。
100 ：１３２人目の素数さん：04/03/30 03:43
>>92
ヴィトゲンシュタインか、おまいわ（笑）
ヴィトゲンシュタインか、おまいわ（笑）
101 ：１３２人目の素数さん：04/03/30 11:10
>>99
>直観主義論理でも勉強したら？
それは知ってるよ。
俺は別に上で示した公理系を薦めているわけでも、実際に使おうとしているわけでもない。
それに、公理系を動かすことによる定理の変化を探ることは形式主義論理のやることだぞ。
>解釈も何も、命題の真偽はその公理系で定義するような事柄ではありません。
それは最初に"真偽"がある場合のみ正しい。
"証明、反証の可能性"が最初にあれば、
>解釈も何も、証明、反証の可能性はその公理系で定義するような事柄ではありません。
ということになる。
>直観主義論理でも勉強したら？
それは知ってるよ。
俺は別に上で示した公理系を薦めているわけでも、実際に使おうとしているわけでもない。
それに、公理系を動かすことによる定理の変化を探ることは形式主義論理のやることだぞ。
>解釈も何も、命題の真偽はその公理系で定義するような事柄ではありません。
それは最初に"真偽"がある場合のみ正しい。
"証明、反証の可能性"が最初にあれば、
>解釈も何も、証明、反証の可能性はその公理系で定義するような事柄ではありません。
ということになる。
102 ：１３２人目の素数さん：04/03/30 17:58
>>101
バカですか？
バカですか？
103 ：１３２人目の素数さん：04/03/30 18:57
104 ：１３２人目の素数さん：04/03/30 22:47
105 ：１３２人目の素数さん：04/03/31 13:13
106 ：１３２人目の素数さん：04/03/31 18:50
>>101
うしろ半分が全く趣旨が分からん
>>104
漏れも前から良く分からんなとは思ってたんだけど、
BrouwerとHeytingの差、位に考えていいの？
Heytingの思想って殆ど知らないんだけど
うしろ半分が全く趣旨が分からん
>>104
漏れも前から良く分からんなとは思ってたんだけど、
BrouwerとHeytingの差、位に考えていいの？
Heytingの思想って殆ど知らないんだけど
直観主義論理⊂形式主義だろ。
原理的に今の数学は形式主義じゃないの？飽くまで原理的には。
原理的に今の数学は形式主義じゃないの？飽くまで原理的には。
108 ：１３２人目の素数さん：04/03/31 18:53
ごめん、あげちゃった………………
109 ：１３２人目の素数さん：04/04/06 10:33
234
110 ：１３２人目の素数さん：04/04/25 22:32
390
111 ：１３２人目の素数さん：04/04/30 20:07
ゲット？
191