ジョルダンの曲線定理が完全証明される
■ このスレッドは過去ログ倉庫に格納されています
0001１３２人目の素数さん
2005/09/28(水) 02:15:26・フランスの数学者カミーユ・ジョルダンが１８８７年に概念を確立し、その後多くの
数学者らが完全証明に挑んできた「ジョルダンの曲線定理」について、信州大
工学部の中村八束（やつか）教授（６２）が２７日、ポーランドの数学者ら１６人との
約１４年間にわたる共同作業で、完全証明に成功したと発表した。数式上の誤り
などを確認するコンピューターシステムのチェックを経て、約２０万行にわたる証明が
完成。中村教授らは「完全証明したのは世界初」としている。
「ジョルダンの曲線定理」は「平面上の閉じた曲線は、平面を曲線の内と外に分ける」
というもの。直感的には明らかだが、数学的な証明は難しいとされてきた。
中村教授によると、人間が行った数学的な証明をチェックする「プルーフ・チェッカー」
というコンピューターシステムのうち、今回はポーランド・ビアリストーク大のアンジェイ・
トリブレッツ博士（６４）らが開発した「ＭＩＺＡＲ（ミザール）」と呼ばれるシステムを使用
したという。中村教授は「同様のシステムでコンピュータープログラムにミスがない
ことを確認するなど、今回の成果は実社会にも応用できる可能性がある」と話している。
http://www.mainichi-msn.co.jp/shakai/wadai/news/20050928k0000m040137000c.html
0232The_Knight_of_Mathematics ◆uGlSZOV4Kc
2005/09/29(木) 18:23:30パズルが噛み合うから証明できたよーんっていうようなものだろ
ほら見ろよ 噛み合ってんじゃん！って
その証明を否定しようにもスパコンひっぱってこなきゃならんし
20万行読まなきゃならんしで大変･･･
今後はこういう証明が台頭する状況になっていくかと
0233１３２人目の素数さん
2005/09/29(木) 18:25:17>ペアノ公理系から
なんでペアノ公理系からなの？
集合論の公理系でいいじゃない。
そこからフェルマーは証明されてんでしょ。
0234１３２人目の素数さん
2005/09/29(木) 18:28:43ああ、いろいろ使ってるからなあ。
しかし、素人の誤解とかいう時点で
君も玄人の誤解に陥ってるな（ｗ
0235１３２人目の素数さん
2005/09/29(木) 18:30:13＞理解せずに正しさを確認できるという発想は
＞どこか精神を患っている希ガス
別に理解しなくても。「正しさだけなら確認」
できる。というのが、ヒルベルトの形式主義。
もちろん、それに対して貴方がどう思うかは、
自由だよ。
ま、単に「正しい」という言葉で意味しいてる
事が違うだけと思うが
ただ、「君の考える正しさ」は、主観的にのみ
確認できるものだと思うけど。それはプラトニ
ズムだな。もちろん、そういう立場もあるよね
0236１３２人目の素数さん
2005/09/29(木) 18:31:26＞集合論の公理系でいいじゃない。
それも分かってないけど
0237１３２人目の素数さん
2005/09/29(木) 18:33:30はあ？ それじゃ証明されてないんじゃない。
0238１３２人目の素数さん
2005/09/29(木) 18:33:39＞だからよ 例えばこういうのとか
＞http://image.blog.livedoor.jp/thinkdeep/imgs/3/4/341da381.jpg
＞図形動かして証明するほうが早いんだよ
これはどうかな？
上は、実はすごーく平べったい平行四辺形が隠れてるのが
トリックなわけだが、絵で書いても容易には見つからない。
0239The_Knight_of_Mathematics ◆uGlSZOV4Kc
2005/09/29(木) 18:34:18俺にはもうついてけんよ
0240１３２人目の素数さん
2005/09/29(木) 18:36:04だから、「基礎論の初歩」を知っている数学の先生に
聞いてみな、ね
この「中村氏の完全証明」と「普通の証明」の違いが
分からないんですけど、どういうことですか？、って
結論から言えば、「普通の数学者の証明」は形式的に
証明できるということとは違うんだ、って答えになる
0241１３２人目の素数さん
2005/09/29(木) 18:40:15＞別に理解しなくても「正しさだけなら確認」できる。
＞というのが、ヒルベルトの形式主義。
違うなあ。「理解しなくても」「確認できる」なんていうのは
君が勝手にそう思ってるだけのこと。
実際には数学の理屈は文字の操作に完全に還元できるという発想。
まあ、唯名論だな。
しかしこれは大きな落とし穴がある。
つまりそもそも文字操作として表した形式化が正しいかどうかは
分からんってこと。だから実は理解ぬきには客観性なんかないって
ことさ。論理マンセーの素人が必ず陥る初歩的な穴だな。
0242１３２人目の素数さん
2005/09/29(木) 18:40:19だから、中村氏の発言になるんでしょ？
ジョルダンの曲線定理は、数学者の言う普通の意味では
証明はできていたけど、形式的証明はできていなかった。
今回、我々はそれに成功したぜ
って言っているの。
0243１３２人目の素数さん
2005/09/29(木) 18:43:05君はもしかしてワイルズの証明はどこかで
公理に拠らない直観を使用しているかもしれないから
計算機で確認するまで証明されたとは認めないつもりかな
おかしな人だなあ、というのが普通の数学の人の反応な訳だけど
0244１３２人目の素数さん
2005/09/29(木) 18:43:58たとえ証明の途中で集合論的な選択公理を援用したにせよ、
原理的には証明からそのような除去できる、って定理があったから
かなり弱い公理から導けると思って間違いないかと
0245１３２人目の素数さん
2005/09/29(木) 18:44:05いまどき、基礎論なんて古臭い言葉を繰り返す奴は
ロジックの初歩も知らんというのが相場。
こっちは、ロジシャンから聞いたこと書いてるんだよ。
0246１３２人目の素数さん
2005/09/29(木) 18:45:50>結論から言えば、「普通の数学者の証明」は形式的に
>証明できるということとは違うんだ、って答えになる
それは程度問題じゃないの。本質的違いじゃなくて。
だから今回みたいに数学者の証明を書き下していけば機械に通るわけで。
0247１３２人目の素数さん
2005/09/29(木) 18:46:08マジックの初歩も知らんというのが相場。
こっちは、マジシャンから聞いたこと書いてるんだよ。
0248１３２人目の素数さん
2005/09/29(木) 18:46:30あのねえ、普通の数学者は、原理的には時間をかければ
計算機で検証可能なレベルで、厳密に定理を証明できるだけの能力は持ってるよ
（まあ幾何学者とか一部あまり厳密で無い人も居るけど）
単に時間が無駄だからそうしないだけでね
0249１３２人目の素数さん
2005/09/29(木) 18:46:45そこは問題にしない、というのが形式主義だろ？
君がその考えは取りたくないというのは勝手だよ
しかし、それだとどこにも客観性はないが。別に
そういう立場はありだ、と思うよ。でも、それは
貴方の考えで。いろんな考え方があるの。
形式主義の考え方ならこうなるよ、って言ってる。
で、中村の完全証明っていうのは、そう言う話だ。
それに価値があるか、どうかは人それぞれの価値
観だ。俺も「ジョルダンの曲線定理の形式証明」
自体にそんなに価値がある、とは思ってないけど。
これは俺の個人的価値観だから。
0250The_Knight_of_Mathematics ◆uGlSZOV4Kc
2005/09/29(木) 18:46:58平面上の閉じた曲線は、
↓
○
↑
平面を曲線の内と外に分ける
これが「ジョルダンの曲線定理」だっ！！！
生徒→ ('A`)「････」
0251１３２人目の素数さん
2005/09/29(木) 18:49:13激しく勘違い。もう君は駄目だ。「基礎論の初歩」を知ってる
普通の（基礎論でない）数学者に聞いてみろよ。直接
やっぱり公式見解が必要かな。こういう勘違い君がいるとこを
見ると。どうにかしてくれって感じだが
0252１３２人目の素数さん
2005/09/29(木) 18:50:23＞そこは問題にしない、というのが形式主義だろ？
重大な間違いだな。誰もそんな馬鹿げたことはいっていない。
＞しかし、それだとどこにも客観性はないが。
君が間違ってる。むしろ問題にしないほうが客観性がない。
そういう立場は君だけの主観的なものだな。他人には通用しない。
君の同類には通用するかもしれないが、具体的な事例になると
君と君の同類の見解はことごとく相違し、了解がとれなくなるだろう。
要するにコミュニケーションを否定した独我論に陥ってるわけだ。
プライドばかり強いとそういう馬鹿げたことになる。
0253１３２人目の素数さん
2005/09/29(木) 18:52:44だから、君のいう「基礎論の初歩」は間違いだよ。
まったく素人に限って勝手に自分の中に似非専門家を
つくるから困ったもんだ。素人が即座に専門家に
なれるわけがないだろ。
0254１３２人目の素数さん
2005/09/29(木) 18:55:36何だか、数学の話じゃなくなってるんですが…
何だか、君は哲学的見解を主張されてるようで
数学者は「数学者同士で」、ある程度、共通の
主観を持っているから高度な数学の話が通じる。
実際、俺はそう感じているよ
0255１３２人目の素数さん
2005/09/29(木) 18:57:41はあ？初歩なんだから、専門家じゃなくても分かっていても
可笑しくないだろ。
数学の専門家じゃなくても、数学の初歩を知ってる人はいる
よね。
0256１３２人目の素数さん
2005/09/29(木) 18:58:350257１３２人目の素数さん
2005/09/29(木) 18:59:10>>249の「そこは問題にしない」というのは数学じゃないよ。
＞数学者は「数学者同士で」、ある程度、共通の主観を
＞持っているから高度な数学の話が通じる。
＞実際、俺はそう感じているよ
共通かどうかはともかくとして、実際には数学者自身の理解と
相互の了解が、数学の定理の正しさを根拠づけているという
主張は私自身がここでしてきたことで、いまさら君の主張だと
言い張られても迷惑なんだが。
0258１３２人目の素数さん
2005/09/29(木) 19:01:22いや、初歩だから、素人が誤解しても可笑しくないんだよ。
見当違いのことをいう人は、たいてい初歩からダメだよね。
君がそう。どうせ独学だろ？だから誤解したまま気づかないんだ。
独学は結局自慰だからな。
0259１３２人目の素数さん
2005/09/29(木) 19:03:00勘違いしてるのは君だよ
俺は別に数学の普通の論文がどれくらい論理的に緻密に
書かれてるか、なんてことは主張して無い
ただ書こうと思ったら書けるよ、と言ったまでのこと
0260１３２人目の素数さん
2005/09/29(木) 19:04:04＞相互の了解が、数学の定理の正しさを根拠づけているという
＞主張は私自身がここでしてきたことで、いまさら君の主張だと
＞言い張られても迷惑なんだが。
だから、それが数学者が普通の意味で言う証明です。
それと、「形式的証明」は違いますよ、って言う話
なんだがなあ。それは分かるでしょ。
俺は、普段、形式的証明なぞ全くしないし、貴方の
定理は（かくかくしかじかの形式体系で）証明でき
ますか？と聞かれたら、「全く分かりません。どう
なんでしょう？」としか、答えようがないよ。
0261１３２人目の素数さん
2005/09/29(木) 19:05:390262１３２人目の素数さん
2005/09/29(木) 19:10:17普通はしない。それに普通の証明したからって、
それで形式的に証明できるのか、どうかなんて、
全然、分からないよ
で、今回、中村は形式的に証明できましたって
話でしょ。
もし、今までの数学者の証明＝形式的証明なら
中村の「初めて」って話は嘘になるけど、俺は
嘘だと別に思わないな
0263１３２人目の素数さん
2005/09/29(木) 19:12:30一階の述語論理が人間の推論様式を全般に渡って記述しうるというのは
十分な検証を要する一種のドグマである。」 by 某W先生
「一階の述語論理」の部分を「NBG集合論」にしてみたり、
「人間の推論様式」の部分を「数学者の推論様式」にしてみると、
＞書こうと思ったら書けるよ
ってのは楽観的すぎかなとも思う。
0264１３２人目の素数さん
2005/09/29(木) 19:14:23ホモロジーって結局何なの？
ttp://cheese.2ch.net/math/kako/1009/10092/1009270205.html
0265１３２人目の素数さん
2005/09/29(木) 19:15:40まあ初めて「形式的に証明」できました、じゃ無くて
初めて「完全証明」できました、なんて言っちゃってるけどな
>>263
まあそりゃそうだね
0266１３２人目の素数さん
2005/09/29(木) 19:19:22しかし、「形式的証明」は今回、初めて我々の手によって与えら
れましたって言うんだから
結局、ジュルダンの定理の「普通の証明」と「形式的な証明」は
違うわけで
0267The_Knight_of_Mathematics ◆uGlSZOV4Kc
2005/09/29(木) 19:28:29ジョルダンの曲線定理とジュルダンの定理はどう違うんだ？
0268１３２人目の素数さん
2005/09/29(木) 19:32:02ジェルダンの曲線定理の「普通の証明」なら、とっくに
あった、でＦＡ。
0269１３２人目の素数さん
2005/09/29(木) 19:33:30>結局、ジュルダンの定理の「普通の証明」と「形式的な証明」は
>違うわけで
誰も同じとは思ってないだろ。
だけど、これは量の問題であって質の問題じゃないだろ。
他の証明、例えばフェルマーの定理の証明だって時間と手間を
かければ形式証明が出来るだろう。そんなことは昔からわかってることだろう。
0270１３２人目の素数さん
2005/09/29(木) 19:35:57＞ポーランドの数学者ら１６人との約１４年間にわたる共同作業
って14年間も何してたんだろ
0271１３２人目の素数さん
2005/09/29(木) 19:43:06＞かければ形式証明が出来るだろう。
その肯定が形式体系から証明できるか、どうかは
分かりません。
ただし、その手の専門家によれば、今までの経験
から予想するに証明できる公算が高いのではない
か、という噂なら聞いたよ
「時間と手間を掛ければ、形式的証明ができる」
ことが分かってるなら形式式証明ができてるのと
同じことじゃないか？
でも、少なくともジョルダンの曲線定理は、そう
じゃなかったよね。ということは「数学者の言う
証明」は「形式的証明」では必ずしもないという
ことだ。
で、ワイルズのフェルマーの定理の証明が形式的
証明だと言う根拠は何なの？
数学者が「形式的証明」であると言ってたかな？
0272１３２人目の素数さん
2005/09/29(木) 19:46:15形式的に証明できるか、どうかは分からない
よね
形式的にも証明できそうだ、という「予想」
することは何ら問題ではないけどね
0273１３２人目の素数さん
2005/09/29(木) 19:49:29＞かければ形式証明が出来るだろう。そんなことは、
＞昔からわかってることだろう。
何が分かってるの？フェルマーが証明されたのは最近。
今もまだ形式的な証明ができるかどうかは分からない。
基礎論の専門家の間では、できるのではないか？、と
予想されているという噂は聞いたよ。
0274１３２人目の素数さん
2005/09/29(木) 19:52:04誰もWilesの200ページ弱の証明がそのまま形式的証明だなんて言ってないだろ？
そんな勘違いをしてるのは君だけ
＞でも、少なくともジョルダンの曲線定理は、そうじゃなかったよね。
実際に形式的な証明が出来ただろ？
「直感的には当然だが、誰も数学的に完全な証明ができなかった」
なんていってるのは中村教授とそのお仲間だけで
平地健吾だって小島定吉だって、オリジナリティの低い低レベルな結果だ、と
内心考えてると思うよ
0275１３２人目の素数さん
2005/09/29(木) 19:54:54＞そんなことは昔からわかってることだろう。
分かってる、ということは
仮定：数学者が（数学者じゃなくてもいいが）こうこうこう言う風に証明
⇒
結論：その定理は形式的に証明可能
という定理でもあるのかい？そんなのがあったら
教えて欲しいなあ。で、ワイルズの証明が、その
定理の仮定を満たしてる事も確認できてるのかな
0276１３２人目の素数さん
2005/09/29(木) 20:00:02＞実際に形式的な証明が出来ただろ？
ジョルダンの場合はね。他の定理もそうだ、というのは
どうして分かるんだい？
分かるというなら『「普通の証明」⇒「形式的証明」』
という定理が成り立つんだよねえ。
つか、その前に「普通の証明」というのを数学的に定義
しなきゃならんがｗｗｗ
0277１３２人目の素数さん
2005/09/29(木) 20:01:46単に、必要があれば、充分形式的なレベルまで証明を緻密にする
自信がある、というだけだろ
証明の形式化のどの部分がそんなに難しいと考えてるのかな？
少なくともZFCの公理から、必要な諸概念を定義して、
完全に形式的に証明するのは、述語論理の基礎を理解している数学者には
簡単なことだと思うがな
今回14年掛かったことだって、単に能力が欠けていた、としか思われない
0278１３２人目の素数さん
2005/09/29(木) 20:06:18ほとんどは「形式的にも証明できる」だろう、という予想でしょ。
よく考えたらゲーデルの第二不完全性定理があるじゃん。
「無矛盾性を意味する（とある）命題」が正しいけれども、
それは形式体系では証明できないって定理だね。
0279１３２人目の素数さん
2005/09/29(木) 20:07:16他の場合も出来るはずだ、という強い確信があるだけだよ
もちろん確実な根拠なんて無いわけだが、
それは、集合論の公理系は矛盾しているかもしれないのに、
実際には現今の数学者は、そんな可能性微塵も考えずに、
無矛盾に決まっている、その無矛盾な集合論で基礎付けできる現在の数学も
無矛盾だろう、と判断して研究を進めるのと同じことでしょ？
それを、無駄に不安を煽るのは、昔杞の国の人が、
天が崩れて落ちてきたらどうしようと憂いて夜も眠れなかった、という故事と一緒で
単なる無駄な取り越し苦労だと考えるべきかと
0280１３２人目の素数さん
2005/09/29(木) 20:11:23＞自信がある、というだけだろ
何だ、自信の話ですか。それは「かくかくしかじかの定理」は
形式的にも証明できると私は予想しています、って話だね。
予想することと、確認することは別だよね。
0281１３２人目の素数さん
2005/09/29(木) 20:12:41他の場合って、どの場合よ。現に出来ないものを
ゲーデルは見つけたでしょ？
0282１３２人目の素数さん
2005/09/29(木) 20:13:04それがどうしたの？
もしかしてそれが
＞「数学者によって証明されている定理」の
＞ほとんどは「形式的にも証明できる」だろう、という予想
に対する反例になると考えているのかな？
君はゲーデルの第二不完全性定理を理解していませんね
そもそもその文脈で挙げるのは第一不完全性定理で充分なはずだけど
0283１３２人目の素数さん
2005/09/29(木) 20:15:30そりゃ手でやりゃあ 14 年もかからずできるさ
問題はどうやって数学的概念を計算機に理解させるか．
俺らが何気なく定義するようなものも，直感(というよりも常識)が多分に入るから，
それを計算機に理解させるためにたくさん手続きが必要になる．
だいぶ基本的な定義が出来上がった後でも，「領域が有界」であることを定義するために
120個も条件連ねなきゃならんのだから，全部証明するのに苦労するかは押して知るべし．
0284１３２人目の素数さん
2005/09/29(木) 20:19:22別に「形式的証明」がなくても不安じゃありませんけど。
というか、形式的証明ができない事が分かったとしても
不安じゃないよ
無矛盾性の証明は形式的に証明できないね。でも、不安
じゃありません。自分の定理が、仮に「形式的に証明」
できなかったとしても不安ではありませんね。
その否定が形式的に証明されたのなら、俺って馬鹿、と
思うだろうけど。そんなことをする暇人はいないから、
気にしてないけどね
0285１３２人目の素数さん
2005/09/29(木) 20:23:07＞ほとんどは「形式的にも証明できる」だろう、という予想
に対する反例になると考えているのかな？
はあ？反例って、予想って書いたけどさ、これは
数学的な定理じゃないよね。
「ほとんど」ってあるよね。これって、数学的な
定義になってないじゃんか？
だから、この予想って書いたけど、これはただの
感想だから。反例も証明もあるわけない。人それ
ぞれの感想だからさ
0286１３２人目の素数さん
2005/09/29(木) 20:23:56（無矛盾で、再帰的に公理化可能ならば、）
その体系の無矛盾性とメタレベルで同値になる、従って直観的には真となるはずの
命題ConTが、【その体系内では】証明できない、という定理でしょ？
だからその体系内でその定理がたとえ証明できなくても、
適当に公理を付け加えた体系T'では普通に証明できて何も困らない
だから計算機で検証不可能な定理の存在を示していることにはならないよね
だから
＞現に出来ないものをゲーデルは見つけたでしょ？
これは君の明らかな勘違い
0287１３２人目の素数さん
2005/09/29(木) 20:25:15＞「数学者によって証明されている定理」の
＞ほとんどは「形式的にも証明できる」だろう
と言ったとしても、これはその人の感想を述べただけね
0288１３２人目の素数さん
2005/09/29(木) 20:26:24予想に反する例、「ほとんど」に当てはまらない例、と言わないと分かって貰えないかな
0289１３２人目の素数さん
2005/09/29(木) 20:27:32＞適当に公理を付け加えた体系T'では普通に証明できて何も困らない
それは分かってる、ってば。
でもさ、「証明したい定理を公理に加えた体系T'」では、その定理は
証明できるよねｗｗｗ
0290１３２人目の素数さん
2005/09/29(木) 20:29:20そうだよ
だからどうしたの？
じゃあ>>281の＞現に出来ないもの
って何のことだよ？言ってみてくれよ
0291１３２人目の素数さん
2005/09/29(木) 20:31:05当てはまるか、当てはまらないか、はどうやって決めるの？
＞予想に反する
予想に反してないか、どうか、は？
ただの感想ですか？
0292１３２人目の素数さん
2005/09/29(木) 20:35:14どうやら、終わったみたいだね。
だから、「無矛盾性を意味する（とある）命題」が
その形式体系では証明できないってこと。
「無矛盾性を意味する」というのは、ここでの話し
ではあまり関係ないがな。
0293１３２人目の素数さん
2005/09/29(木) 20:38:49形式的に証明できれば当てはまるし、予想に反しない、
形式的に証明できないものは当てはまらないし、予想に反する
それくらい文脈から明らかだろうに
>>281によると
＞現に出来ないものをゲーデルは見つけたでしょ？
だそうだから、その「現に出来ないもの」が予想に反するんじゃないかな
それと、数学的なstatement以外を全て「感想」で片付けるのは
止めてくれないかな
別にこのスレはひたすら数学的な定理と証明を書き込むスレじゃないんだからさ
0294１３２人目の素数さん
2005/09/29(木) 20:42:18＞ある定理を正しいと認めた数学者が、
＞その定理が成り立つ適当な公理系が
＞何であるか？についてまで分かって
＞いるとは限らないよ。
もちろん、適当でなければ、いくら
でも思いつくよ。例えばその定理を
定理を含んだ公理系とかね。ｗｗｗ
0295１３２人目の素数さん
2005/09/29(木) 20:43:24頼むから名前欄に仮のハンドルをつけてくれ
0296１３２人目の素数さん
2005/09/29(木) 20:48:25＞その定理が成り立つ適当な公理系が
＞何であるか？についてまで分かって
＞いるとは限らないよ。
で、ジョルダンについては、ごくごく常識的な
公理系で形式的に証明できました、ということ
でしょう
もちろん、これも感想だけどさ。何か異論ある
感想を否定はしてない。感想は感想に過ぎない
というだけのことだよ。
0297１３２人目の素数さん
2005/09/29(木) 20:51:060298１３２人目の素数さん
2005/09/29(木) 20:51:34＞定理は（かくかくしかじかの形式体系で）証明でき
＞ますか？と聞かれたら、「全く分かりません。どう
＞なんでしょう？」としか、答えようがないよ。
これも結論だね。感想だけどさ。
0299１３２人目の素数さん
2005/09/29(木) 20:55:03普通の数学をやっているから。
で、自分が証明した定理が成立する適当な「形式
体系」なぞさっぱり分からないね。それで不安に
なったりはしないよ
これも感想だ
0300１３２人目の素数さん
2005/09/29(木) 20:55:380301１３２人目の素数さん
2005/09/29(木) 20:58:37証明できる、というのは大昔に数学者が確認したことなんだよ
今回の「完全証明」とやらの意義は、Jordan曲線定理を証明するのに
必要な公理の強さを確定したとか言うことじゃなくて、
proof checkerが、実用化に近づいた、ということだろ
0302１３２人目の素数さん
2005/09/29(木) 21:00:28＞証明できる、というのは大昔に数学者が確認した
＞ことなんだよ
じゃあ、その体系で形式的に証明されてたんだね。
ホント？
0303１３２人目の素数さん
2005/09/29(木) 21:02:32＞その定理が成り立つ適当な公理系が
＞何であるか？についてまで分かって
＞いるとは限らない
しかし、集合論的な一部の数学を除けば、ZFCの範囲で大体事足りる
事足りない場合でも、基本的には、ZFCから独立かどうかを判定する
ための一般論は確立されている、というのが
常識的な数学者の所信（君の言う「感想」ｗ）だと思うがな
そう思わないとしたら、基本的に感覚がずれている
0304１３２人目の素数さん
2005/09/29(木) 21:04:05何が「じゃあ」なのか分からないが
まだ形式的な証明と、普通の数学者の証明の区別も付かないのかなあ、、
もう説明する気無いよ
0305１３２人目の素数さん
2005/09/29(木) 21:04:10俺は自分の証明して、論文に発表した定理が、
「適当な公理系から形式的に証明できること」
なんて全く確認してない。他人の論文を読む
ときもね。
形式的に証明できることなんて、普通の数学
者は全然、確認しないと思うが？
0306１３２人目の素数さん
2005/09/29(木) 21:06:26だから、違うんでしょ。違うなら
普通に証明したからって、形式的に証明できるか
どうかは、分からないよね
0307１３２人目の素数さん
2005/09/29(木) 21:07:10＞普通に証明したからって、形式的に証明できるか
＞どうかは、分からない
0308１３２人目の素数さん
2005/09/29(木) 21:07:10とりあえず http://mizar.org/fm/ と20万行目に目を通したんだけど，ほとんど全てが
定式化のための定式化で冗長としか思えんかった．
知識蓄積する以外になんかこのあたり簡単にできんかな？
0309１３２人目の素数さん
2005/09/29(木) 21:07:31多少論理学の知識があれば、形式的に証明するのは簡単そうだ、
と分かるはずだから問題ないよ
0310１３２人目の素数さん
2005/09/29(木) 21:08:37PCにWebブラウザのクッキー情報が残ると、なんか不都合なことでもあるの？
0311１３２人目の素数さん
2005/09/29(木) 21:09:23＞どうかは、分からない
ジョルダンの定理は普通に証明されていたが、今回、
形式的に証明がなされた、ということでいい訳だね
0312１３２人目の素数さん
2005/09/29(木) 21:12:12Goedelがある論文の中で
これこれのformal proofは、まともに書くと長くなるが、
これこれメカニズムを入れれば、短縮できる、みたいな
証明工学なことにも触れているのは流石だ、と言って
林晋が褒めてたかと
もうそのページ消されたのでInternet Archive探さないと残ってないっぽいけど
0313１３２人目の素数さん
2005/09/29(木) 21:15:30全然、思わないがな。それに「公理系」と「定理」の
採用の仕方によるね。普通の数学者は、どんな形式的
体系で、どんな命題に置き換えるかなんて、意識して
ないと思うが。
だから、お前らの言っていることは、多くの場合には
数学者の証明を見ると適当な公理系と定理に対応する
適当な命題を思いつく自信があるよということでしょ。
君の感想だよね。別に、否定するつもりはないけどね。
0314１３２人目の素数さん
2005/09/29(木) 21:17:50http://www.shayashi.jp/HistorySociology/HistoryOfFOM/Books/books.html かな？
>この本では技術的には一貫して計算機科学的視点からゲーデルの定理を見ています。
>その方が自然なのです。例えば，ゲーデル数を素因数分解で定義しますと、
>実際にやるとトンでもないことになりますが、普通の文字列のコード化と同じにすれば
>スイスイです。また、対角線論法も、コンピュータでは、例えば、lisp を使えば、
>本当に実行して遊ぶことができます。
0315１３２人目の素数さん
2005/09/29(木) 21:18:360316１３２人目の素数さん
2005/09/29(木) 21:21:25もう一度、書いておく。
＞自分が証明するときに形式的に証明されるか、どうか、なんて
＞気にしちゃいねーよ。だから、形式的に証明できるか、どうか
＞なんて分からないし、仮に形式的に証明ができないものだった
＞としても、気にしないね。普通に証明できればＯＫだ。
0317１３２人目の素数さん
2005/09/29(木) 21:21:57＞しかし、さすがゲーデルというか、そういう定義を完全に展開してしまうと
＞扱っている論理式が非常に大きくなるだろうとか、Principia Mathematica のよう、
＞定義のメカニズムが入っていれば、短くなるが、などの証明工学的な話もちゃんと議論しています。
＞前原先生がイオタ記号を使われたのは、ここら変を曖昧にしておくのが嫌だったからでしょう。
ここらへんのことです
論理式の長さ、でしたね、失礼
まあ証明の長さにも同じことは言えると思いますが
0318１３２人目の素数さん
2005/09/29(木) 21:23:39だから＞仮に形式的に証明ができないものだった
そんなものがあるかもしれないと信じてる数学者は殆どいねえっていうのに
>>306-307を見てレスする気力がなくなったけどね
0319１３２人目の素数さん
2005/09/29(木) 21:31:43具体的に「定理と公理系」を特定しなければ、
形式的に証明できるとか、できないとかが、
意味を持たないだろう。
ということは、「そういうものがある」という
のもただの感想だし、「そういうものがない」
というのもただの感想にしか過ぎないね。
君は感想を言ってるんだ。俺もだがな。自覚し
ようぜ
0320１３２人目の素数さん
2005/09/29(木) 21:33:03その定理は形式的に証明できるからな。
0321１３２人目の素数さん
2005/09/29(木) 21:34:14Principia Mathematica のようなメカニズムって，数々の省略記号のことかな？
だとしたら相当楽観的な判断に思えるんだがなあ．
0322１３２人目の素数さん
2005/09/29(木) 21:36:48少なとも、俺はあると思うぜ。
ない、と思う奴もいるだろう。
いずれにしても、どちらも間違ってない訳だ。
ということは「意識調査」の問題だな。
各国の数学者に「意識調査」をして見るのも
いいかもしれないね。時代とか、国によって
どう変わるかとかね。ちょっと見てみたい。
0323１３２人目の素数さん
2005/09/29(木) 21:42:57２．「普通に証明できてるものは『適当な』公理系で形式証明可能」
いや、「できないものもある」
→ どちらを考えるにしても、ただの感想。正しい、間違って
いるの問題ではない。因みに、俺は「できない派」だけどね。
0324１３２人目の素数さん
2005/09/29(木) 21:44:28『適当な』という部分が個人の主観だからね。
0325１３２人目の素数さん
2005/09/29(木) 21:48:48だから「確信、所信」を「感想」に変えないでくれないかな
意味が違う言葉だからさ
>>323
具体的にはどういう定理がそうなると思うのかな？
まさか具体例は無い、なんてことは無いだろうけど
0326１３２人目の素数さん
2005/09/29(木) 21:50:37証明ができない定理がある
と俺は思う。もちろん、これはただの感想。『適当な』というのが
個人的主観だから
0327１３２人目の素数さん
2005/09/29(木) 21:53:19＞だから「確信、所信」を「感想」に変えないでくれないかな
＞意味が違う言葉だからさ
意味が分からないな。だって、普通の意味で反証可能命題では
ないじゃない。ということは、感想だろが？
確信という言葉は、反証可能な命題でなければ意味ないぜ
0328１３２人目の素数さん
2005/09/29(木) 22:04:290329１３２人目の素数さん
2005/09/29(木) 22:05:34＞証明可能
これは感想とか、意見の類でしかないよね。ご自由にどうぞ
俺の意見は、「証明不可能なものもある！」だ。というか、実は
どっちでもいいんだけどね。
俺が本当に言いたいことは、「それって、どちらにしても、結局
意見にしか過ぎない！」ということ
0330１３２人目の素数さん
2005/09/29(木) 22:09:52確信って、「正しいか、間違ってるかが決まる」ことに対して
言うんでしょ。決まらないことに言うのは、ただの意見だよ。
というか、どちらも正しい訳だから矛盾が許容される世界での
「おしゃべり」だね。それも、結構だと思うよ
0331１３２人目の素数さん
2005/09/29(木) 22:12:05あんたは不可能なものがあると信じる根拠を挙げなきゃ意見未満だよ
あと確信ってのは正しいと信じていること。決まるかどうかとは無関係。
さらに言えばあんたの立場では決まらないかどうかもわかんないでしょ？
■ このスレッドは過去ログ倉庫に格納されています