四色問題とHadwiger予想。二色目。

四色問題とHadwiger予想。二色目。at MATH

四色問題とHadwiger予想。二色目。 - 暇つぶし2ch■コピペモード
□スレを通常表示
□オプションモード
□このｽﾚｯﾄﾞのURL
■項目テキスト

529:hadwiger
 10/01/24 01:43:27 
おかしいな。インターネットを探しても、『数学ガール』の 
不完全性定理の証明が納得できない、という主張はみつからなかった。 
本当に理解できた人はいるのか？　351頁からの議論をステップごとに 
確認した人はいないのだろうか？　検索がへたなだけなのか？ 
もう、わけがわからない。

530:１３２人目の素数さん
 10/01/24 01:52:31 
あんたおかしいだろ。 
そんなものまで検索して見つかるかよ。 
ふつう、勉強ノートを詳細まで公開する人はいないだろ。 
 
本にはけっこう嘘の証明が書いていることがあるよ。この件については知らないが。

531:hadwiger
 10/01/24 02:15:27 
いや、他人の勉強ノートまで見たいんじゃなくて、 
議論があってもいいんじゃないか、ということ。 
インターネットで、ここがわからないよ、と質問するとか。 
あのレベルの本を読む人で、ちゃんと読んで、 
理解しようとする人は、いないのかもしれない。

532:hadwiger
 10/01/26 00:26:10 
ごめんなさい。私がバカでした。 
>>528 表現定理は∃r ∀m∀n  でいいんですね。これは、 
たとえば、x^n + y^n = z^n も、x,y,z,n が数値で与えられていれば、 
原理的には計算で成立しているかどうか、確かめられますよ、というような 
意味の定理なんですね。 
≪x は z の“形式的証明”でない≫　の数値別表現を u(-x, -z) 、 
≪z は subst(y, [y1], -y) である≫　の数値別表現を v(-z, -y)、 
≪x は subst(y, [y1], -y) の“形式的証明”でない≫　の数値別表現を q(-x, -y)、 
とすると、 
q(-x, -y) ⇔ ∃-z( v(-z, -y) ∧ u(-x, -z) ) 
とかなんとかなって、351頁のように、p<-p>をつくると、 
p<-p> = forall( [x1], ∃-z( v(-z, -p) ∧ u([x1], -z)) ) 
とかなんとかなって、この意味はp<-p>は誤り、ということになる。 
ゲーデル数p<-p>を調べると、p<-p>は誤りと書いてある。 
それで、矛盾するということなんですね。 
これは普通の数学でいうと、1/x にx=0 を入れるみたいな、特異な状況で、 
普通の数学では除外できるけど、形式的体系Pでは除外できる規則はない、 
ということですね。ミルカさんの証明は見事としか言いようがない、 
なかなかすごい、かなりのもんです。 
でも、これから得られる、普通の数学のための教訓としては、 
ちゃんと well-define してるか調べろ、ぐらいしかないような…

次ページ