ジョルダンの曲線定理が完全証明される
■ このスレッドは過去ログ倉庫に格納されています
0001１３２人目の素数さん
2005/09/28(水) 02:15:26・フランスの数学者カミーユ・ジョルダンが１８８７年に概念を確立し、その後多くの
数学者らが完全証明に挑んできた「ジョルダンの曲線定理」について、信州大
工学部の中村八束（やつか）教授（６２）が２７日、ポーランドの数学者ら１６人との
約１４年間にわたる共同作業で、完全証明に成功したと発表した。数式上の誤り
などを確認するコンピューターシステムのチェックを経て、約２０万行にわたる証明が
完成。中村教授らは「完全証明したのは世界初」としている。
「ジョルダンの曲線定理」は「平面上の閉じた曲線は、平面を曲線の内と外に分ける」
というもの。直感的には明らかだが、数学的な証明は難しいとされてきた。
中村教授によると、人間が行った数学的な証明をチェックする「プルーフ・チェッカー」
というコンピューターシステムのうち、今回はポーランド・ビアリストーク大のアンジェイ・
トリブレッツ博士（６４）らが開発した「ＭＩＺＡＲ（ミザール）」と呼ばれるシステムを使用
したという。中村教授は「同様のシステムでコンピュータープログラムにミスがない
ことを確認するなど、今回の成果は実社会にも応用できる可能性がある」と話している。
http://www.mainichi-msn.co.jp/shakai/wadai/news/20050928k0000m040137000c.html
0153１３２人目の素数さん
2005/09/29(木) 15:02:22非常に好意的に無理矢理解釈すれば、まぁ間違いではないか。
0154１３２人目の素数さん
2005/09/29(木) 15:04:01切った貼ったって三角形の合同だろ。そんなものは、ユークリッドの公理
から出るだろ。
0155１３２人目の素数さん
2005/09/29(木) 15:13:39ttp://e-learn.mine.nu/mizar/jordancurve.htm
>we have finally completed formalizing
>in Mizar the proof of the Jordan Curve Theorem.
を恣意的に誤訳して作り上げた単語だと思う。
0156１３２人目の素数さん
2005/09/29(木) 15:13:53何を当たり前なことを。
誰も非ユークリッド空間でピタゴラスの定理が成立つとは言ってないよ。
トンデモは除いてだが。
0157１３２人目の素数さん
2005/09/29(木) 15:17:45まあ、誤解をまねく用語なことは確か。
形式的証明でもちょっとおかしいけどね。
0158１３２人目の素数さん
2005/09/29(木) 15:32:00くらいにしときゃ誤解も無いんだろうけどな
0159１３２人目の素数さん
2005/09/29(木) 15:33:20数学者の間では既に証明されたと認められている定理でも
形式的証明はなされていないものは、ジュルダンの閉曲線
定理以外にも非常に多い。例えば、ワイルズにより証明が
なされたフェルマーの最終予想もその一つでしょう。この
研究はそれらの定理にも形式的な証明が与えられるように
なる第一歩となるのでないか、と期待できる
そうすると素直に読めるなｗｗｗ
0160１３２人目の素数さん
2005/09/29(木) 15:36:27>>301
ポモ的なのに叩かないのは、そういう理由だったんだね！
土建屋＝宇沢＝長谷川＝黒木 ← 隠れポモ野郎
禿藁＝Ｕ健爾 ← 隠れポモ野郎
あほ鴨＝中村 ← 隠れポモ野郎
303 ：１３２人目の素数さん ：2005/09/29(木) 15:26:53
>>302 >>295
こいつらって、結局
ポモと同じでしょ。
＞そして、別の場所で、極端なことを言っているのではないかと非難された場合には、
＞3 (a) に近い穏健だが当たり前の主張を述べて批判をかわします。
http://www.math.tohoku.ac.jp/~kuroki/FN/relativism.htm
0161１３２人目の素数さん
2005/09/29(木) 16:00:27したがってワイルズの証明は間違っているとやった人が
アメリカに居たねｗ
0162１３２人目の素数さん
2005/09/29(木) 16:04:15No
単に証明の計算機による検証のことを
信州大の教授が完全証明と称しているだけ
0163１３２人目の素数さん
2005/09/29(木) 16:19:35数理論理では、記号論理による数学の定理の証明のことをさす
用語があるんじゃないの？ 形式証明でいいのかな？
0164１３２人目の素数さん
2005/09/29(木) 16:32:59もちろん、メタ論理のレベルでの、たとえば不完全性定理の「証明」とかとは
意味が違う訳ですが、文脈から言って誤解する可能性はほとんど無いですし
まあ、形式的証明とか形式証明とか言っとけば
言いたいことは通じるんじゃ無いでしょうか
0165１３２人目の素数さん
2005/09/29(木) 16:33:38> 形式証明でいいのかな？
他にも、証明図という呼び方をする場合もある。
面倒なので単に「証明」と呼んで、通常の証明を「非形式的証明」と言ったりもする。
0166１３２人目の素数さん
2005/09/29(木) 16:34:16「証明図」とか「証明木」とかは見た事がある。単に「証明」って言う事が多い。
「完全証明」と名付けてるのは見た事がない。
あと「形式証明」って言ったら、
普通は「証明する対象がメタでない」という事の強調として捉えると思う。
0167１３２人目の素数さん
2005/09/29(木) 16:35:30この世界は概ねユークリッド空間だから
非ユークリッド空間で成立するとされている全ての定理は
証明に失敗しているわけですね。
てゆうか１次元や２次元で成立する定理も全部ダメですね。
この世界は概ね３次元なんですから。
自然数もダメ。あれ無限だし。この世界にあるのは自然数の
有限部分集合だけだもんね。数学は窮屈な学問だね。
0168１３２人目の素数さん
2005/09/29(木) 16:36:31一つここに書いてくれないかね。
0169１３２人目の素数さん
2005/09/29(木) 16:41:530170１３２人目の素数さん
2005/09/29(木) 16:43:38計算機でチェックできる形式に書き下してくれ
0171１３２人目の素数さん
2005/09/29(木) 16:43:55そう。
＞そんなものは、ユークリッドの公理から出るだろ。
物理的に切った貼ったするならユークリッドの公理に従うとは限らない（ｗ
つまり、そこが盲点というわけだ。
0172１３２人目の素数さん
2005/09/29(木) 16:46:12勧違いしてしまいそうだから
数学会として公式見解を出しておく
必要がありそうですね
Up野先生，こういうときこそ
その指導力を善用してください
若手いじめではなく
0173１３２人目の素数さん
2005/09/29(木) 16:51:51原理的に計算機でチェックできるくらい厳密じゃないのかな
（実数論の公理を一寸手直しする必要があるかもしれない）
もっとも、この本は全く直観を排して書かれていることで有名だけども、
それでもとある「明らかだが証明が難しい」定理が、
"困難も無く"得られることになっているのだがｗ
0174１３２人目の素数さん
2005/09/29(木) 16:52:22そもそも証明が完全に公表されて無いんじゃなかったっけ
0175１３２人目の素数さん
2005/09/29(木) 16:55:35そのヒルベルトの幾何学基礎論による証明かい？
すり替えはよくないね。学問を否定する悪行だよ。
0176１３２人目の素数さん
2005/09/29(木) 16:57:30いや公表はされてるんだけど
あまりに膨大で入りくんでいるため
確認がとれない
最近の Aschbaher らの仕事で
あやしかった部分が克服されて
ようやく完成したと見ていいでは(？)
という話
0177１３２人目の素数さん
2005/09/29(木) 16:59:17中村八束氏の仕事の先駆といってもよいものだ。
つまり、ヒルベルトの証明と通常の作図による証明の差を理解すれば
形式的証明と通常の証明（あるいは説明）の差を理解できるはずである。
0178１３２人目の素数さん
2005/09/29(木) 17:03:01では、公式見解の叩き台を考えましょう。
数学者の間では既に証明されたと認められている定理ではあっても
形式主義的に満足できる証明がなされているものは、非常に少ない。
例えば、ワイルズによって証明がなされたフェルマーの最終予想も
形式的証明までは、まだ遠いようである。今回の中村氏らの研究は
それらの定理にも、形式的な証明が与えられるようになる第一歩と
なるのではないか、と大きな期待を抱かせるものである。
0179１３２人目の素数さん
2005/09/29(木) 17:05:12別にそんなこと一言も主張してないが
初めて習うときに多分に直観的な証明がされて何が悪い？
0180１３２人目の素数さん
2005/09/29(木) 17:08:29数学者の間では既に証明されたと認められている定理ではあっても
形式主義的に満足できる証明がなされているものは、非常に少ない。
例えば、ワイルズによって証明がなされたフェルマーの最終予想も
形式的証明までは、まだ遠いようである。今回の中村氏らの研究は
それらの定理にも、形式的な証明が与えられるようになる第一歩と
なるのではないかと我々数学者に大きな期待を抱かせるものである。
最後の行に「我々数学者に」を入れてみたけど
0181１３２人目の素数さん
2005/09/29(木) 17:08:47計算機によって証明が検証された！とか言っても
今度は計算機とそのプログラムの信頼性の問題が出てくるわけで
往々にして健全な直観の方が信頼が置けたりするわけで
まあ、たとえJordan曲線定理にしか適用できないようなモノだったにせよ、
それまで殆ど計算機科学者の机上の空論だった証明チェッカが
初めて実際に実際の数学の定理の証明をチェックした、
という意味で意義の有る仕事だとは思うけどね
0182１３２人目の素数さん
2005/09/29(木) 17:11:47形式的証明以外はすべてただの説明である、証明に非ず
って暗に言ってるような感じで一寸違和感があるな、、
直観が混じった証明か、原理的に論理規則と公理だけからできる証明かは
数学者だったら簡単に区別くらいつけられる
0183１３２人目の素数さん
2005/09/29(木) 17:13:51だから形式証明なんかほとんどの数学者は必要としてないんだって。
手軽に出来るならケアレスミスのチェック用に便利っていうだけ。
だけど手軽になんか出来ないだろ。
0184１３２人目の素数さん
2005/09/29(木) 17:14:12＞初めて習うときに多分に直観的な証明がされて何が悪い？
問題は、その直観が隠れた前提を持っているかどうか。
例えば作図の場合、たいていの人は作図による合同と
物理的な「切った貼った」の違いに気づかない。
しかし、非ユークリッド幾何学のクラインモデルや
ポアンカレモデルを理解するにはこの違いに気づく必要がある。
0185１３２人目の素数さん
2005/09/29(木) 17:15:18＞往々にして健全な直観の方が信頼が置けたりするわけで
それは今のところね。しかも、健全な直観を獲得するのは
ごく専門領域に限ったとしても大きな労力を要することは
君もよく知っているはずだよね
だから、コンピュータによる自動化が今後なされることは、
それなりに意味のあることだろう。まだ実用段階にはない
だろうけど。特に数学の証明問題の自習に役立つと思うし、
数学者だって自分の証明のチェックに使えるだろう
0186１３２人目の素数さん
2005/09/29(木) 17:17:51「必要ない」なんていったら、角が立つだろう。
これは政治的な話でもあるんだよ。素人の誤解を
解きつつ、見解は相手を立てる言い方にしないと
0187１３２人目の素数さん
2005/09/29(木) 17:19:19新聞記者が勝手に都合の良い所だけ切り取ってきた、という可能性もあるがな
0189１３２人目の素数さん
2005/09/29(木) 17:20:25＞往々にして健全な直観の方が信頼が置けたりするわけで
プログラムのミスも人間のミス（ｗ
それも含めて人間がミスしやすいのは明らか。
>>182
そう読むのは間違っている。
＞ 直観が混じった証明か、原理的に論理規則と公理だけから
＞できる証明かは数学者だったら簡単に区別くらいつけられる
これは大嘘。数学者は無意識に直観を混入させている。
その直観が論理規則と公理で正当化できるかどうかなど
数学者にはさしたる関心はない。時間の無駄だからだ。
0190１３２人目の素数さん
2005/09/29(木) 17:21:41そんなに手軽に証明チェックが出来るようになるものかな？
普通証明する場合は同様に、で済ませるようなところだって
機械はそれじゃ理解してくれないし
0191１３２人目の素数さん
2005/09/29(木) 17:23:36当時の現実的可能性の少なさに負けたとも言える
その可能性を追求している人達を無碍に否定する
必要もなかろうて
0192１３２人目の素数さん
2005/09/29(木) 17:26:58いや、必要ないと思ってるならはっきりそういうべきだろ。
喧嘩が怖いチキンは真っ先に食われる。
0193１３２人目の素数さん
2005/09/29(木) 17:27:11＞機械はそれじゃ理解してくれないし
だから、今はね。今後の可能性を否定
しなくてもいいでしょ。そういうこと
やってる人の研究を、部外者が見解を
出すに当たっては気の利いたリップ・
サービスをしてこうぜ
２chで誹謗中傷は、大いに結構だがｗ
0194１３２人目の素数さん
2005/09/29(木) 17:29:10・オレが理解できたらその定理は正しい
（ただしオレ自身が証明した定理を除く）
0195１３２人目の素数さん
2005/09/29(木) 17:30:04やれやれ批判と誹謗中傷と区別できない馬鹿がここにもいたか。
0196１３２人目の素数さん
2005/09/29(木) 17:31:22必要ないのは、多くの数学者の感覚に過ぎないだろ。
大体、数学会には「基礎論屋」だっているんだから
基礎論屋なんて追い出せ、という教条主義を掲げる
決意をこれからは持つというならそれもありかもな
そいつらは必要だと思ってやっているわけだから、
それに合わせてやれ
0197１３２人目の素数さん
2005/09/29(木) 17:32:18・オレが理解できないのに機械が検証したなんて認めない！
0198１３２人目の素数さん
2005/09/29(木) 17:34:34>ヒルベルトは「必要」という立場だったわけでさ
根拠は？
0199１３２人目の素数さん
2005/09/29(木) 17:35:02＞それなりに意味のあることだろう。まだ実用段階にはない
＞だろうけど。特に数学の証明問題の自習に役立つと思うし、
＞数学者だって自分の証明のチェックに使えるだろう
実用化されれば、役立つじゃんか。まあ、実用化されるのに
どれだけ時間が掛かるのは分からんがなｗ
0200１３２人目の素数さん
2005/09/29(木) 17:35:31いまや、ロジシャンなんてソフトウェア科学会とか
科学哲学会あたりに亡命しちまったと思ったが（ｗ
数学屋の嫌論理なんてのはヨーロッパの反ユダヤ主義
くらい根深いもんだろ。
0201１３２人目の素数さん
2005/09/29(木) 17:36:39一般に流布している常識を知らない？まあ、
常識が正しいという確証はないわけだが…
0202１３２人目の素数さん
2005/09/29(木) 17:39:06数学屋のプラトニズムという信仰の虚妄を明らかに
するものだからだろう。
数学的プラトニズムが極右なら
論理的フォーマリズムは極左
0203１３２人目の素数さん
2005/09/29(木) 17:40:24別に基礎論屋がこういう証明を支持するかというと
また微妙かもしれないけどね
>>200
50年前にこういうふいんきは無かったはず
というか、日本特有じゃないのかな、基礎論異端視がこんなに激しいのは
0204１３２人目の素数さん
2005/09/29(木) 17:41:370205１３２人目の素数さん
2005/09/29(木) 17:42:52常識なら根拠くらい挙げられるだろう。
0206１３２人目の素数さん
2005/09/29(木) 17:44:53＞別に基礎論屋がこういう証明を支持するかというと
＞また微妙かもしれないけどね
彼らは専門家だから、より慎重でしょう。
ただ、こういう方向性の研究自体には、普通の数学者
よりも親近感を持つ人が多いでしょう。中には、近親
憎悪的過剰反応を示す香具師もいるかも試練が。
0207１３２人目の素数さん
2005/09/29(木) 17:45:07>するものだからだろう。
どう明らかにするんだよ。
0208１３２人目の素数さん
2005/09/29(木) 17:46:28「ヒルベルトは形式主義の提唱者」という常識
0209１３２人目の素数さん
2005/09/29(木) 17:47:28いや、世界的傾向だね。
ロジックは結局言葉の学問だからね。
たいていの日本人は、ロジックが存在する意味すら理解できていない。
だから、極少数の理解者は、さながら隠れキリシタンのようなもの。
0210１３２人目の素数さん
2005/09/29(木) 17:50:15どっかの研究科みたいに、教条主義を掲げて別分野をパージしますか？ｗ
0211１３２人目の素数さん
2005/09/29(木) 17:52:44『面白さ＆有用さ』にあるからね。
0212１３２人目の素数さん
2005/09/29(木) 17:53:03俺は205じゃないけども
ヒルベルトの形式主義は別に計算機で証明をチェックすれば
厳密性が確保できる、とか言うことじゃなくて
証明を形式的に書き下せば自然数論なり実数論なり、
特定の形式的数学の無矛盾性が証明できるから、（りゃ
という思想だったはず
もちろん俺はヒルベルトの後継者だ！とか自負するのは勝手だけど
一寸ヒルベルトの考えに対する勝手な憶測が入りすぎかと
0213１３２人目の素数さん
2005/09/29(木) 17:53:03ロジシャンは興味を持つだろうね。
ただ、ロジシャンは素人のようにロジックに絶対的信頼は置いてない。
だから、フォーマルだから正しいとは言わない。
彼らが興味を持つというのは、正しいかどうかよりも、どういう
フォーマリズムによってそれが証明されるのかという仕掛け。
ある意味、マニアというかヲタク的興味。
0214１３２人目の素数さん
2005/09/29(木) 17:53:48有用さ＞＞＞厳密性
基礎論屋は、死ね！
0215１３２人目の素数さん
2005/09/29(木) 17:54:48死ぬべきなのは君だと思うな
0216１３２人目の素数さん
2005/09/29(木) 17:54:51私見では置換群が鍵のように見えるんですが…
0217１３２人目の素数さん
2005/09/29(木) 17:57:39ヒルベルトがつきぬけてるのは、文字面だけ考えればイイ！
というところに気づいた点。
ただ、こういう発想は数学者にはとっても嫌われる。
美女も骸骨だけみりゃいいみたいな感じにとられるわけだ（ｗ
0218１３２人目の素数さん
2005/09/29(木) 18:00:11マツシン先生いますか？
いたら返事をしてください
0219１３２人目の素数さん
2005/09/29(木) 18:02:11計算機でチェックするとは言ってないでしょ。大体、
当時はコンピュータがなかったんだから
ヒルベルトは２段構え
１．定理の客観性を確保するために、形式体系内で証明を行う
２．当該の形式体系が少なくとも全く無意味であることを保障
するためには、（有限の立場で？）無矛盾性を確認する
２はゲーデルによって（一応の）否定を見たわけだけど、１は
なんら否定を受けていないからさ
一応、形式的に証明されれば客観的な訳で、もちろん矛盾した
体系ならば、すべての命題が正しいから意味はないけど。その
場合であったとしても正しいということ自体は客観的ではある
0220１３２人目の素数さん
2005/09/29(木) 18:02:22いまどきの集合論屋は数学者です。
彼らを、基礎論屋とかロジシャンとか呼ぶとたいてい蹴られます。
0221１３２人目の素数さん
2005/09/29(木) 18:04:19＞２．当該の形式体系が少なくとも全く無意味であることを保障
＞ するためには、（有限の立場で？）無矛盾性を確認する
すまん、書き間違えたよん。
２．当該の形式体系が少なくとも「全くの無意味」ではないことを
保障するためには、（有限の立場で？）無矛盾性を確認する。
0222The_Knight_of_Mathematics ◆uGlSZOV4Kc
2005/09/29(木) 18:04:38コンピューティングによる証明を否定するゆえはない
例えば ピタゴラスの定理の証明の一つなどで辺に接続する図形を移動することで証明とする場合を
否定するようなものだ
俺ってキングとは逆に幾何学大好きだから目で見てわかる証明のほうが美しいと感じる
0223１３２人目の素数さん
2005/09/29(木) 18:09:24別に客観性なんてヒルベルトの関心にはなかった筈。
＞一応、形式的に証明されれば客観的な訳で
しかし実際には、形式的証明は激しく読みにくい。
したがって「機械は正しいといってるがオレにはチンプンカンプン」
という状況がおきる可能性大。客観的というより「無観的」といった
ほうがいい。
0224１３２人目の素数さん
2005/09/29(木) 18:12:27>１．定理の客観性を確保するために、形式体系内で証明を行う
これ普通に数学者がやってることなんじゃないの？ ただ記号論理でやらないだけで。
0225１３２人目の素数さん
2005/09/29(木) 18:12:44だから別に読まなくてもいいんだって、
それはコンピュータに読ませるための
証明なんだからさ
ユークリッド幾何を勉強するのに幾何
学基礎論を読まなくてもいいでしょ
勉強をして感覚を養うのと、正しさを
厳密に確認するのは、違う作業だって
ことはよく知ってるでしょ
0226１３２人目の素数さん
2005/09/29(木) 18:13:26いや、全然やっていない。
0227１３２人目の素数さん
2005/09/29(木) 18:16:14もっと詳しく
0228１３２人目の素数さん
2005/09/29(木) 18:16:59＞別に客観性なんてヒルベルトの関心にはなかった筈。
集合論のパラドックスに端を発して、
数学（的定理？）の正しさを保障する
方法が必要であると考えたのが、常識
として「ヒルベルトの動機」だったと
いうことになってるよ
0229The_Knight_of_Mathematics ◆uGlSZOV4Kc
2005/09/29(木) 18:17:00http://image.blog.livedoor.jp/thinkdeep/imgs/3/4/341da381.jpg
図形動かして証明するほうが早いんだよ
四色問題の証明もこの証明も
これと似たようなことしてるだけだろ
数理的な証明も不可能ではないけど
複雑な命題になるにつれて
そうした証明を読み解いて理解できるやつが少なくなる
0230１３２人目の素数さん
2005/09/29(木) 18:20:42だから、フェルマーの定理だってペアノ公理系から
（その肯定も否定も）導けるか、どうかは分かって
ないよ。数学者が証明したということと公理系から
形式的に導けるということは別物なの。
これが分かってないと、中村教授の「完全証明」と
いう言葉で誤解をしてしまう素人さんの一人に入る。
0231１３２人目の素数さん
2005/09/29(木) 18:21:11＞だから別に読まなくてもいいんだって、
＞それはコンピュータに読ませるための
＞証明なんだからさ
コンピュータを信頼する根拠は？
＞ユークリッド幾何を勉強するのに
＞幾何学基礎論を読まなくてもいいでしょ
それはむしろ君の主張を否定するもののような希ガス
＞勉強をして感覚を養うのと、正しさを厳密に確認するのは、
＞違う作業だってことはよく知ってるでしょ
理解せずに正しさを確認できるという発想は
どこか精神を患っている希ガス
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＞そこは問題にしない、というのが形式主義だろ？
重大な間違いだな。誰もそんな馬鹿げたことはいっていない。
＞しかし、それだとどこにも客観性はないが。
君が間違ってる。むしろ問題にしないほうが客観性がない。
そういう立場は君だけの主観的なものだな。他人には通用しない。
君の同類には通用するかもしれないが、具体的な事例になると
君と君の同類の見解はことごとく相違し、了解がとれなくなるだろう。
要するにコミュニケーションを否定した独我論に陥ってるわけだ。
プライドばかり強いとそういう馬鹿げたことになる。
■ このスレッドは過去ログ倉庫に格納されています