ジョルダンの曲線定理が完全証明される
レス数が1000を超えています。これ以上書き込みはできません。
0001132人目の素数さん
2005/09/28(水) 02:15:26・フランスの数学者カミーユ・ジョルダンが1887年に概念を確立し、その後多くの
数学者らが完全証明に挑んできた「ジョルダンの曲線定理」について、信州大
工学部の中村八束(やつか)教授(62)が27日、ポーランドの数学者ら16人との
約14年間にわたる共同作業で、完全証明に成功したと発表した。数式上の誤り
などを確認するコンピューターシステムのチェックを経て、約20万行にわたる証明が
完成。中村教授らは「完全証明したのは世界初」としている。
「ジョルダンの曲線定理」は「平面上の閉じた曲線は、平面を曲線の内と外に分ける」
というもの。直感的には明らかだが、数学的な証明は難しいとされてきた。
中村教授によると、人間が行った数学的な証明をチェックする「プルーフ・チェッカー」
というコンピューターシステムのうち、今回はポーランド・ビアリストーク大のアンジェイ・
トリブレッツ博士(64)らが開発した「MIZAR(ミザール)」と呼ばれるシステムを使用
したという。中村教授は「同様のシステムでコンピュータープログラムにミスがない
ことを確認するなど、今回の成果は実社会にも応用できる可能性がある」と話している。
http://www.mainichi-msn.co.jp/shakai/wadai/news/20050928k0000m040137000c.html
0002132人目の素数さん
2005/09/28(水) 02:20:12ヘボい企業の人が営業で言いそうな台詞だ。
0003132人目の素数さん
2005/09/28(水) 02:27:120004132人目の素数さん
2005/09/28(水) 02:47:440005132人目の素数さん
2005/09/28(水) 02:49:570006132人目の素数さん
2005/09/28(水) 02:56:290007132人目の素数さん
2005/09/28(水) 02:59:59【研究】「実社会にも応用可」 "ジョルダンの曲線定理"、世界初の完全証明…信州大教授ら
ttp://news19.2ch.net/test/read.cgi/newsplus/1127835258/
0008132人目の素数さん
2005/09/28(水) 03:00:57もっともそんなの見る気にもならんが
0009132人目の素数さん
2005/09/28(水) 03:16:29たぶん、それが「証明」じゃなくて「完全証明」の意味だろうね。
中村さんのサイト
ttp://e-learn.mine.nu/mizar/jordancurve.htm
には、最初に証明したのは「Oswald Vebren」と書いてあるけど、
「Veblen」のミススペルだから、ここ見てたら直してね。
0010132人目の素数さん
2005/09/28(水) 07:36:34ftp://mizar.uwb.edu.pl/pub/version/mml/jordan.miz
ftp://mizar.uwb.edu.pl/pub/version/abstr/jordan.abs
http://e-learn.mine.nu/mizar/jordancurve.htm に
>Oswald Vebren が 1905年に一応の証明をしたと言われていますが、前提
>となる知識の到るところに直感が使われ、完全証明とは言いがたいものでした。
とあるけど、「直感が使われ」ていたのは具体的に証明のどの部分なのだろう?
0011132人目の素数さん
2005/09/28(水) 07:51:59証明の長さ的にもギネス級でわ?
0012132人目の素数さん
2005/09/28(水) 07:55:41ごジョルダンでしょ?
0013132人目の素数さん
2005/09/28(水) 08:15:430014132人目の素数さん
2005/09/28(水) 09:11:46「数学者は役たたず.自分の縄張りの問題も解決できない
やっぱり工学は偉い」
みたいなレトリックに転嫁されそうですね
数学プロパのみなさん
曲線定理の経緯とこの信州大の人の仕事の意義を
詳しく説明してください
0015132人目の素数さん
2005/09/28(水) 09:56:414 名前:132人目の素数さん[] 投稿日:2005/09/28(水) 02:47:44
プルーフチェッカーのデモの一つとして、曲線定理をやってみただけでは?
・ 曲線定理の経緯と
10 名前:132人目の素数さん[sage] 投稿日:2005/09/28(水) 07:36:34
>Oswald Vebren が 1905年に一応の証明をしたと言われていますが、前提
>となる知識の到るところに直感が使われ、完全証明とは言いがたいものでした。
とあるけど、「直感が使われ」ていたのは具体的に証明のどの部分なのだろう?
13 名前:132人目の素数さん[sage] 投稿日:2005/09/28(水) 08:15:43
>>10 公理からダイレクトに出してない,くらいの意味だとおも
0016132人目の素数さん
2005/09/28(水) 09:58:42もうちょっとツッコんだ分析をお願いします
0017132人目の素数さん
2005/09/28(水) 10:25:48できたのが最大の成果ではないかな。ミザール言語からTeXへ、
TeXからミザール言語へ変換するようなスクリプトやエディタ
があると、今後は普及していくかも知らん。
0018132人目の素数さん
2005/09/28(水) 10:33:41出来てない、というか、してない有名定理は五萬とある訳で
プルーフチェックが今後、簡便化されていけば、将来的に実用もあるん
じゃないかねえ?自分で書いた証明をチェッカーに掛けて検証するとか
0019132人目の素数さん
2005/09/28(水) 10:52:22自動証明を応用することはありえるのでしょうか?
0020132人目の素数さん
2005/09/28(水) 10:56:33当分はないんじゃない?これは既にある証明の構文チェックをするものなので、
証明をするのとは次元が違うとおもわれ。教科書の証明をどんどんミザール言語に
翻訳したり、ライブラリを作ったりするのが今後の発展方向では?
0021132人目の素数さん
2005/09/28(水) 10:58:08未解決問題を証明することはできないでしょうか?
0022のりお
2005/09/28(水) 11:11:200023132人目の素数さん
2005/09/28(水) 11:12:22既に自動証明と言うジャンルはある。任意の命題を一階述語論理の範囲で
真か偽か判定するものなので、その過程は証明であると言えば言える。
しかしその種のプログラムは一般に、有限時間の範囲で真または偽という
判定がでるとは限らない。囲碁や将棋では、この手は損だと思ったら
適当な基準で考えるのを止めていいんだが、証明はそうでないという
点が最も異なる。とはいえ未解決問題や証明のギャップを、有限時間
考えてみるというプログラムが登場してくる可能性はありうる。
それだって、(ミザール言語による)数式のライブラリがある程度
充実していないとなかなか機能しないと考えられるが。
0024132人目の素数さん
2005/09/28(水) 11:16:27これか?
http://pya.cc/pyaimg/pimg.php?imgid=18276
0025132人目の素数さん
2005/09/28(水) 11:23:36「厳密さは時代の関数」と言った偉い数学者がいたと思ったよ。
完全証明と言うのは、完全に厳密な証明のことであろう。気にスンナ。
>>24
Mizar言語の概要
http://markun.cs.shinshu-u.ac.jp/kiso/projects/proofchecker/mizar/Mizar-J/Miz-ch2.htm
0026132人目の素数さん
2005/09/28(水) 11:27:43>>287
黒木のように、直観力がなく、客観に頼ろうとする人間には
数学は無理だったんだよ。結局
0027132人目の素数さん
2005/09/28(水) 11:32:48が載ってる本教えて。なるべく手に入りやすいのが有難い
0028132人目の素数さん
2005/09/28(水) 11:35:14Jordan, Cours d'Analyze de l'Ecole Polytechnique (1887)
0029132人目の素数さん
2005/09/28(水) 11:40:20トポロジー入門
0030132人目の素数さん
2005/09/28(水) 13:51:59夫馬です。
「客観的な証明は20万行」も掛かるんだってさ。こんなの
やってられないよね。普通の証明は、「直感」的なんだよね。
客観的ではないのよ。分かりましたか
0031132人目の素数さん
2005/09/28(水) 14:49:53>将来的に実用もあるんじゃないかねえ?
そのためには、人間にとっては直観的に明らかな命題を
自動証明する"行間を埋める"機能が必要だね。
0032132人目の素数さん
2005/09/28(水) 15:29:18約14年間にわたる共同作業の大部分は、人間にとって間を埋められるのが
わかりきっている部分を、計算機に手取り足取り教えるのに費されたのでは
ないかと。
0033132人目の素数さん
2005/09/28(水) 15:41:29もし黒木が査読者だったら、んなことせにゃならんのか?
0034132人目の素数さん
2005/09/28(水) 15:44:010035132人目の素数さん
2005/09/28(水) 15:44:27それは最初にクレームしただけで、間違っている。Veblen の1905年論文は
ぐぐるとヒットするはず。シェーンフリース1906やL.ブラウワ1909(不動点定理
のほう、有限群のほうはR.ブラウワ)の論文もある。
Jordanよりも四色問題やケプラー問題のプルーフチェックをしてくれると
助かるね。
0036132人目の素数さん
2005/09/28(水) 15:45:59って事は結局、自動証明が実用的なものにならない限り、
人手も時間も掛かりすぎて駄目っぽいな
0037132人目の素数さん
2005/09/28(水) 15:51:18通常、「自動証明」というのは人間にとっても意味のある定理を
証明することを目標にする
この場合は、人間にとって自明な命題を証明できればいい
厳密には区別できないが、そいうことだ
0038132人目の素数さん
2005/09/28(水) 15:56:19人間にとっては自明な命題の自動証明
この間にある間隙はいかほどのものだろう
0039132人目の素数さん
2005/09/28(水) 16:01:17「人間にとって自明」ってのは、「良く知られた事実」と「良く知られた論法」の中から
「その場面において適切なものを選び出」せば、わずかな手順で証明が探索出来るって事だよね。
数学的事実とか論法のデータベース化と、
それらをどんな場面でどうやって組み合わせるのが適切か、という知識のデータベース化が進めば、
人間にとって自明な命題が証明出来るようになるのかな。
0040132人目の素数さん
2005/09/28(水) 16:04:10既存の証明をMizar言語に翻訳して、Mizarに食わせて、
受理されるかどうかを確かめるってハナシでしょ。
しろうとの勘違いだったらスマン。
0041132人目の素数さん
2005/09/28(水) 16:06:54>受理されるかどうかを確かめる
それで済むなら、既に実用段階に近いということだね。
どっちが正しいのかは知らないが
0042132人目の素数さん
2005/09/28(水) 16:07:44それより、表題の件は証明チェッカーを通すために人間が
証明を機械にわかる形に書いたのが20万行ってことだろうな。
このステップ数をなんとか数千行くらいまで落とせれば実用になるだろう。
0043132人目の素数さん
2005/09/28(水) 16:09:50このプロジェクトの目的は数学の論文のチェックのシステムを作ることです.
http://markun.cs.shinshu-u.ac.jp/kiso/projects/proofchecker/mizar/Mizar-J/Miz-ch1.htm
0044132人目の素数さん
2005/09/28(水) 16:11:340045132人目の素数さん
2005/09/28(水) 16:13:51食わせた、ということか?
0046132人目の素数さん
2005/09/28(水) 16:21:28>いますが、前提となる知識の到るところに直感が使われ、
>完全証明とは言いがたいものでした。
数学の定理のほとんどは、そうなのだが…
直感なしの証明が与えられている定理なんて、ほとんどない
0047The_Knight_of_Mathematics ◆uGlSZOV4Kc
2005/09/28(水) 16:23:11・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・
・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・
・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・
・・・・・・・・・・・・
これが証明すべきものであった.
0048132人目の素数さん
2005/09/28(水) 16:26:15実用には耐えられないわな。せめて1千行〜1万行でないと。
>このプロジェクトの目的は数学の論文のチェックのシステムを作ることです.
http://markun.cs.shinshu-u.ac.jp/kiso/projects/proofchecker/mizar/Mizar-J/Miz-ch1.htm
0049132人目の素数さん
2005/09/28(水) 16:29:22自動変換するシステムが必要になるな。
0050The_Knight_of_Mathematics ◆uGlSZOV4Kc
2005/09/28(水) 16:29:39そのためにPDが職を得るのSA
教授の原案をもとに数十人がかりでNA
世の中うまくまわるようになっるYO
0051132人目の素数さん
2005/09/28(水) 16:30:37だからって、その概念があいまいで信用出来ないってことはない。
ある意味、直感ほど正確で信用おけるものはない。
程度によるけど。だから程度問題。
0052132人目の素数さん
2005/09/28(水) 16:30:38自動証明はやったのか?やらなかったのか?それが問題だ!
0054The_Knight_of_Mathematics ◆uGlSZOV4Kc
2005/09/28(水) 16:34:440055132人目の素数さん
2005/09/28(水) 16:34:56人間にとっては自明な命題の自動証明
この間にある間隙はいかほどのものだろう
0056132人目の素数さん
2005/09/28(水) 16:37:08実用化の必要十分条件
0057The_Knight_of_Mathematics ◆uGlSZOV4Kc
2005/09/28(水) 16:38:26MIZARによるものはその次によい
- ウィリアム・メークピース・サッカリ(イギリスの小説家)
0058132人目の素数さん
2005/09/28(水) 16:40:560059132人目の素数さん
2005/09/28(水) 16:50:010060132人目の素数さん
2005/09/28(水) 17:15:23ユークリッド幾何をMIZARが食えるように書き直すってのは
まあ面白いかもね。
今回は、ジョルダンという「自明のようだが証明はわかりにくい」定理の
プルーフチェックを計算機で行ったという着眼点がよかった。
ピタゴラスの定理だったら、さほど評価されないね。
四色問題なら14年ですまないw
フェルマーは人間がチェックするほうがはるかに早い。
論文の TeX ソースを MIZAR に変換する自動プログラムなんて、
当分無理だしね。
0061132人目の素数さん
2005/09/28(水) 17:26:46だろうな。検証対象の証明文を書くにしてもライブラリに登録する文章を書くにしても、
完全に行間を埋めなきゃいけなかったら、大変すぎて非実用的。
自明な行間くらいはコンピュータが自分で補ってくれないと。
「組み合わせ的に考察すれば明らか」とか「定数項に着目すれば明らか」とかを
詳しく書いてられない。
0062132人目の素数さん
2005/09/28(水) 17:31:060063132人目の素数さん
2005/09/28(水) 17:33:40コンピューターによる定理の自動証明
http://science4.2ch.net/test/read.cgi/math/1126017312/
0064132人目の素数さん
2005/09/28(水) 17:36:39フェルマー予想もな。
で、ほとんどの証明されてる定理には、まだ完全証明は
与えられていない。
ここ200年の間の数学的成果で完全証明の与えられて
いる定理の割合は1%も行かないんじゃない
0065132人目の素数さん
2005/09/28(水) 17:38:01完全証明⊂証明だろうけど
0066132人目の素数さん
2005/09/28(水) 17:39:14それはproof checkerが実用的な(人手も時間も
掛からない)ものになる可能性を否定するも同然かと。
0067132人目の素数さん
2005/09/28(水) 17:39:25プルーフチェックの実用化は無理だよん。諦めなwww
0068132人目の素数さん
2005/09/28(水) 17:40:280069132人目の素数さん
2005/09/28(水) 17:47:33proof checkerと自動証明はまったく別ものだろう。
難度から言ったら自動証明のほうがはるかに、というより可能と
不可能の違い。
0070132人目の素数さん
2005/09/28(水) 17:52:01proof checker の実用化=自明な命題の自動証明
自動証明=意味の有る定理の自動証明
という意味でなら、違うなあ
0071132人目の素数さん
2005/09/28(水) 17:53:54つまり、自明な命題の自動証明は可能、
意味の有る定理の自動証明は不可能と
いうことですかい
0072132人目の素数さん
2005/09/28(水) 17:56:320073132人目の素数さん
2005/09/28(水) 17:57:28人間がすべての行間を埋めなければならない
それは人間が「定理の証明図」を書かないと
いけない、というのと同じ
これでは、プルーフチェックは全く実用的で
ない
0074132人目の素数さん
2005/09/28(水) 18:00:21「禿 藁 to appear 論文」の自明を
自動証明ができるレベルじゃなきゃ
ダメだろw
0075132人目の素数さん
2005/09/28(水) 18:02:52それが出来たら、禿ちゃんの数学者としての名誉も完全回復だね♪
0076132人目の素数さん
2005/09/28(水) 18:04:37それは「自明」ではなく「間違い」。百歩譲って「ギャップ」。
本人による手動証明もできるレベルでないwww
0077132人目の素数さん
2005/09/28(水) 18:05:26禿ちゃん、病院のベッドの上でMIZARを必死に勉強中らすい
0078132人目の素数さん
2005/09/28(水) 18:07:35いや、Ann. Math. の査読者が間違っているんだよ。
正しいのは分科会だった、ということまで自動的に
証明できるよ♪
0079132人目の素数さん
2005/09/28(水) 18:08:53一定時間内に埋められなかった行間は自己申告して人間に埋めて貰う。
んでその埋められなかった行間が多すぎなければ実用的と言えるかと。
>>74-78
巣に帰れ。他スレにまで迷惑掛けるな。
0080132人目の素数さん
2005/09/28(水) 18:10:28そうでしょうなあ。
0081132人目の素数さん
2005/09/28(水) 18:13:370082132人目の素数さん
2005/09/28(水) 18:15:57ただ、今回のは「行間を埋める」じゃなくて、何が仮定されてるのか
よくわからんから証明をチェックしてみました〜って話だから、
「自明をコンピュータで埋める」とは違うかと。
論文の自明は「ルーティンだけどめんどくさい」が多いので、
さまざまなルーティンを全部プログラムにぶち込むのは今のところは
不可能。今回は、ジョルダンに特化してるわけで、何にでも使える
わけではない。
0083132人目の素数さん
2005/09/28(水) 18:16:32数学基礎論(とくに証明論)の初歩の初歩をどうぞ
0084132人目の素数さん
2005/09/28(水) 18:20:21このプロジェクトの目的は数学の論文のチェックのシステムを作ることです.
http://markun.cs.shinshu-u.ac.jp/kiso/projects/proofchecker/mizar/Mizar-J/Miz-ch1.htm
0085132人目の素数さん
2005/09/28(水) 18:42:27「完全証明は史上初」という売り文句は素人相手に有効だよね。
完全証明ということばで、今までの証明は数学的に不十分だったと
思わせられるから。
0086132人目の素数さん
2005/09/28(水) 18:49:07そうすると、現在までに証明されているほとんどの定理には
数学的に完全な証明はないことになるんだけどね。
0087132人目の素数さん
2005/09/28(水) 19:18:04S_nのアレキサンダー双対とかいうので証明したスレがあったとおもうんだけど
あれどこだっけ?おぼえてるひといまつ?
0088海援隊
2005/09/28(水) 19:22:080089132人目の素数さん
2005/09/28(水) 19:35:080090132人目の素数さん
2005/09/28(水) 19:48:000091GiantLeaves ◆zkraGArAss
2005/09/28(水) 19:53:490092132人目の素数さん
2005/09/28(水) 19:57:140093132人目の素数さん
2005/09/28(水) 20:27:55----------------------------------------------
9月28日(水)
------------------------------------------------------------------------
ジョルダンの曲線定理 信大教授ら「完全証明」
------------------------------------------------------------------------
信大工学部の中村八束教授(62)=長野市青木島、数理情報学=が28日
までに、約120年間、数学的に完全に証明されなかった「ジョルダンの曲線
定理」を、ポーランドの数学者らと共同で初めて完全証明した−と同教授が管
理するホームページ上で発表した。
ジョルダン曲線定理は、「閉じた曲線は、平面を内と外に分ける」というも
の。1887年、フランスの数学者カミーユ・ジョルダンが発表した。中村教
授は「直感的には当然だが、誰も数学的に完全な証明ができなかった」として
いる。
中村教授は1991年、ポーランドのワルシャワ大学ビアリストーク分校に
勤務する数学者とともに証明に取り組み始めた。同国の数学者らが管理する、
数学の証明をチェックするコンピューターシステム「ミザール」を用い、両国
の計16人の数学者が分担、14年かけて証明を終えた。
中村教授は「ジョルダン曲線定理を前提にしていた多くの証明がある。今回
の証明で、そうした別の証明にも根拠を与えることができる意義は大きい」と
している。
東工大大学院情報理工学研究科の小島定吉教授(位相幾何学)は「基本的に
は証明された定理だと考えているが、数学者にとっては、どこまで証明すれば
完全かという問題がある。ミザールを使い、完全に証明できたという点に意味
があるのではないか」としている。
0094132人目の素数さん
2005/09/28(水) 20:30:150095132人目の素数さん
2005/09/28(水) 21:27:24見方によっては、実はあいまいな直観にたよった証明だった
という事実に衝撃
数学側からみて物理の人の使う数学が
「いい加減なことやってんな」
と思うのに似てるのか?
0096132人目の素数さん
2005/09/28(水) 21:49:45互換性のある別の処理系を作って追試するしかないんじゃないか。
0097132人目の素数さん
2005/09/28(水) 21:55:54でもそれで満足しなかった人が数学的に証明したりして。
それでも満足しなかった人が計算機にチェックさせたと。
それでもなお満足しない人はチェッカが正しいことを何らかの方法で確かめて、
その方法が正しいことを確かめて(以下無限ループ)
になるんだろうかねえ
0098132人目の素数さん
2005/09/28(水) 21:59:48それでも満足しない人は
公理系の妥当性を疑う
そしてノイローゼになる
0099132人目の素数さん
2005/09/28(水) 22:23:51ワロスwww
でも実際、数学はそういう公理の元、つまりある程度人間の空想であるもの、
これの上で成り立っているものだから、
「数学的な証明」っていうのはどうなってくるんだろうなぁ。。。
0100132人目の素数さん
2005/09/28(水) 22:38:23人によっては、人間の存在とは全く別個に数学的現象の実在を信じ、
実在する数学的現象を人間が記述する事が数学である、と思ってる人もいる。
そういう人にとっては、公理ってのは人間が後から取ってきた一つの言語に過ぎないし、
ZFCか型の理論かそれら以外かとかもどうでもいい事。
ゼータの実在を信じてる人も。
010199
2005/09/28(水) 22:49:31マジレスありがとうございます。
そういう捉え方もありましたか。。。
何か数学について人間について考えさせられました。本当にありがとうございます。
数学って物理的な部分を持つ反面、何かと哲学っぽいですね。
0102132人目の素数さん
2005/09/28(水) 22:52:30数学徒は鉄柱にだけはなってはいけない
0103132人目の素数さん
2005/09/28(水) 23:31:130104132人目の素数さん
2005/09/28(水) 23:41:46嫌基礎論厨
0105132人目の素数さん
2005/09/29(木) 00:47:460106132人目の素数さん
2005/09/29(木) 00:59:26それはむしろ閉曲面バーションっぽいな。
3次元ユークリッド空間の場合も「証明」済みなんかな?
0107132人目の素数さん
2005/09/29(木) 01:07:041次元以上なら何次元でも成り立つ(0次元球面は2点空間)。
0108132人目の素数さん
2005/09/29(木) 05:51:39直観を使うにせよ、せめて直観を論理で埋めることが
可能なことくらい確認するはず
>>56
まあ永田雅宜先生にとって自明な命題≠普通の数学者にとって自明な命題
だけどなwww
0109132人目の素数さん
2005/09/29(木) 05:53:15小島先生も相変わらず言葉を濁してるねwww
>>95
似てないよ
0110132人目の素数さん
2005/09/29(木) 09:06:14行っただけだろ。なにもジョルダンの定理の証明が不完全だから機械にかけて
完全な証明を行ったわけじゃない。お前等のポイントがずれてるんだよ。
つまり勘違い。あの20万行の内容を具体的にみればわかるだろうけど、
あれは既存の証明を機械にわかる形に書いただけのもんだろ。
0111132人目の素数さん
2005/09/29(木) 09:17:13半分以上の人間はそんなこと分かってると思うが
0112132人目の素数さん
2005/09/29(木) 09:18:37Euclid の有名な証明あるよね?
あれを Mizar 言語で
だれか書いてくんない?
Mizar の感じをつかみたい
0113132人目の素数さん
2005/09/29(木) 10:19:35矛盾してるな。
20万行を数千行に圧縮するには、
圧縮された証明の行間を埋められる
程度に賢い自動証明が不可欠。
述語論理の充足可能性の非決定性の壁を
突破しろなんて誰もいっちゃあいない。
0114132人目の素数さん
2005/09/29(木) 10:27:39>今回のは「行間を埋める」じゃなくて、何が仮定されてるのか
>よくわからんから証明をチェックしてみました〜って話だから、
>「自明をコンピュータで埋める」とは違うかと。
一口に「自明」といっても奥が深い。
単純に論理学的に少ないステップで証明できるものとは言えない。
直観的には人間は理解できるが、機械がチェックできるような
形式的な理論が構築されていない場合は多々ある。
ただ、こういう話は、昔AIで議論されたフレーム問題にも関わる。
AIが記号主義からコネクショニズムにパラダイムシフトした
最大の理由は、いちいち言葉で書くのが面倒くさいので、
機械が勝手に学習してくれればいいなと思ったから。
0115132人目の素数さん
2005/09/29(木) 10:27:57>矛盾してるな。
何が?
0116132人目の素数さん
2005/09/29(木) 10:32:03一方で、自動証明はダメといいつつ、
もう一方で、行数を少なくしろといってること。
行数を少なくすれば、行間が広くなる。
そこは、単純に推論規則に当てはまってるかどうか
だけではチェックできない。行間を埋められるような
推論規則の組み合わせが存在するかどうかを確かめる
必要がある。それはまごうことなき「自動証明」だ
0117132人目の素数さん
2005/09/29(木) 10:35:02>基本的には証明された定理だと考えているが、
(本音)同じ分野の連中は皆納得してるって
>数学者にとっては、どこまで証明すれば完全かという問題がある。
(本音)ただ、畑違いの連中が「わかんねー」
なんていうからめんどくせーんだよ。
>ミザールを使い、完全に証明できたという点に意味があるのではないか
(本音)ま、そういう連中が納得できるんなら、いいんじゃねーの?
0118132人目の素数さん
2005/09/29(木) 10:35:12読みすぎというか。20世紀における科学技術の進歩に幻惑されて
るんだろうな。
0119132人目の素数さん
2005/09/29(木) 10:39:47>一方で、自動証明はダメといいつつ、
>もう一方で、行数を少なくしろといってること。
行数を少なくしろなんて言ってないだろ。
実用になるには行数が多くては駄目という当然のことを言ってる。
自動証明が駄目という意味は、non-trivialな定理の証明が駄目って
いうこと。すこしは、意を汲んだらどうだ、コンピュータじゃあるまいし。
0120132人目の素数さん
2005/09/29(木) 10:45:58「楽観過ぎる」というのはその通りだな。
もっとも、誰にも迷惑はかけていないと思うが(w
0121132人目の素数さん
2005/09/29(木) 10:48:55>もっとも、誰にも迷惑はかけていないと思うが(w
税金使ってないか?
0122132人目の素数さん
2005/09/29(木) 10:56:55使ってるだろうけど、それがなくなると
貴様のところにいったいいくら戻ってくるか
一度でもマジメに計算したことあるのか?
0123132人目の素数さん
2005/09/29(木) 10:59:43>小島先生も相変わらず言葉を濁してるねwww
数学者の間で証明されたと認められている定理でも
完全証明のないものは非常に多い。例えばワイルズ
により証明されたフェルマーの最終予想もその一つ
でしょう。この研究は、それらの定理に完全証明が
与えられるようになる第一歩となるのではないかと
期待できる
とでも言っておけば…
0124132人目の素数さん
2005/09/29(木) 11:14:16そう開き直られてもな。第5世代コンピュータ開発計画
(つまりAI)というのが鳴り物入りで始められたことがあったよな。
あのプロジェクトにいくら使われたのか。数億程度なわけないだろ。
で結局失敗。その責任を取ったやつっているのかよ。
誰もいないから、まだ懲りずにAIやって飯食える。甘い世の中だよな。
0125132人目の素数さん
2005/09/29(木) 11:18:04完全証明のないものは、ジュルダンの閉曲線定理以外にも
非常に多い。例えばワイルズにより証明されたフェルマの
最終予想もその一つでしょう。この研究はそれらの定理に
完全証明が与えられるようになる第一歩となるのではない
か、と期待できる
0126132人目の素数さん
2005/09/29(木) 11:37:07それを言うならピタゴラスの定理だって完全証明はないんじゃないの?
完全証明なんていらないってのがほとんどの数学者の意見だろう。
まあ、ケアレスミスのチェックにあれば便利というくらいで。
ただし、20万行も書かなきゃなんないのなら論外。
0127132人目の素数さん
2005/09/29(木) 11:40:40証明工学的なアプローチが必要なんだよな
20万行だと一寸本職の数学者が使う気にはならないな
プログラマにとって見れば大したこと無いんだろうけど
(WindowsのOSが2000万行くらいだったっけ?オーダーはあってるはず)
0128132人目の素数さん
2005/09/29(木) 11:47:46そうだけど。そこまで言ってしまうと角が立つから、
大人の対応としての発言として、こんなのどう?、と
いう提案だ。
0129132人目の素数さん
2005/09/29(木) 12:03:13>第5世代コンピュータ開発計画
これの残党でちゃっかり数学教授におさまってるのが
R命館にいるな
指導者の淵も大学におさまちゃってるが
責任とらずに
0130132人目の素数さん
2005/09/29(木) 12:08:43>(つまりAI)
AIは第五世代コンピュータ開発計画の一部だよ
似たような例として、第五世代=シグマという勘違いをしてる人もよく見掛けるね
0131132人目の素数さん
2005/09/29(木) 12:35:08AIはあのプロジェクトの主要な部分だからな。だからなに?
0132132人目の素数さん
2005/09/29(木) 13:48:51TRONもΣもなんだって批判できるよなぁ、程度の意味です
0133132人目の素数さん
2005/09/29(木) 13:59:47違うだろ。能天気すぎるんだよ。AIやってる連中は。
SFの読み過ぎだって。映画「2001年宇宙の旅」の見すぎ。
あの映画は2001年を舞台にしたものでHALというAIコンピュータ
が活躍するな。で2005年の現実はっていうと、あんなものは影も形もない。
あの原作者のクラークは通信衛星なんかを予言して、わりと先見性があるけど
AIに関してはまるで大はずれ。彼はSF作家だから、はずれても問題ないけどな。
0134132人目の素数さん
2005/09/29(木) 14:02:17HAL は中に人がいる設定だったけどな
その意味じゃはずれてない
0135132人目の素数さん
2005/09/29(木) 14:15:50君はそんなにAIに期待を持っていたのかね
なるほどそれでボクの心を裏切ったんだと
シンジ君宜しく発狂寸前な訳ですな( ´,_ゝ`)
0136132人目の素数さん
2005/09/29(木) 14:20:25出来っこないとバカにしていたよ。まあ、おとぎ話として、
映画は映画として見たが。
0137132人目の素数さん
2005/09/29(木) 14:27:27第五世代=AIというのはいくらなんでも無知すぎるな。
AI以前の理論計算機科学のところが大きいんだが。
>結局失敗
そりゃ君が勝手に高望みしてるからじゃないか?
少なくとも日本で理論計算機科学で博士取得者を
沢山生産できたのは成功だよ。まあ、高山さんとか
数学に逃げられてしまったが(笑
0138132人目の素数さん
2005/09/29(木) 14:33:04あれは、暗にこの世界がおおむねユークリッド空間であることに
全面的に依存してる。
もしこの世界が例えば双曲的非ユークリッド空間だったら失敗する。
0139132人目の素数さん
2005/09/29(木) 14:33:26今のAI研究も同じようなもんだろ。AIとは名ばかり。
>そりゃ君が勝手に高望みしてるからじゃないか?
第5世代コンピュータって出来てないだろ。
これが失敗でなくて何?
0140132人目の素数さん
2005/09/29(木) 14:34:33釣りだよな?
0141132人目の素数さん
2005/09/29(木) 14:35:10>数億程度なわけないだろ。
日本の人口を一億として、十億なら十円、百億なら百円。
まあ、百円戻ってくるならジュース一本くらい買えるかな。
職場内の自販機だと百円で買えるし(w
0142132人目の素数さん
2005/09/29(木) 14:38:25マジですが、何か(w
0143132人目の素数さん
2005/09/29(木) 14:40:56失敗したとは気づかれない。
それは、非常に遅い速度では相対性理論を
必要としないのと同じようなものである。
0144132人目の素数さん
2005/09/29(木) 14:43:02何も日本人全員に割り振るなよ。まともに税金納めてる人間は
30%くらいだろ。そうすると、300円か。
俺だったら100円でもドブに捨てたくないね。
0145132人目の素数さん
2005/09/29(木) 14:43:33「第五世代なんちゃらは、投下した税金に見合った成果が得られていない、
プロジェクトとして見通しが甘すぎた」
って言いたいんじゃないの?
0146132人目の素数さん
2005/09/29(木) 14:43:49シンジはまだ幸せ。
ODの心境はさながらアスカのようなもの。
0147132人目の素数さん
2005/09/29(木) 14:47:01一見もっともらしいが、じゃあいったいどういう成果を
期待していたんだと聞くと、実に妄想モード全開みたいな
回答がバカバカでてきて、呆れ果てる。
0148132人目の素数さん
2005/09/29(木) 14:49:18漏れは君が使うほうがドブに金を捨てた気分になるが(w
0149132人目の素数さん
2005/09/29(木) 14:51:24世界が非ユークリッドだとユークリッド幾何学の定理が証明出来ないのか?
そんなことはないだろ。幾何学というのは、我々の住む世界だけを
扱うわけではない。
0150132人目の素数さん
2005/09/29(木) 14:55:23基礎論ヲタの人教えて。
0151132人目の素数さん
2005/09/29(木) 14:56:18>世界が非ユークリッドだとユークリッド幾何学の定理が証明出来ないのか?
図形を切った貼ったする証明に関してはそう。
0152132人目の素数さん
2005/09/29(木) 14:59:33「ユークリッド空間ではピタゴラスの定理が成り立ちますよ」
という実証でしかない。
0153132人目の素数さん
2005/09/29(木) 15:02:22非常に好意的に無理矢理解釈すれば、まぁ間違いではないか。
0154132人目の素数さん
2005/09/29(木) 15:04:01切った貼ったって三角形の合同だろ。そんなものは、ユークリッドの公理
から出るだろ。
0155132人目の素数さん
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.
を恣意的に誤訳して作り上げた単語だと思う。
0156132人目の素数さん
2005/09/29(木) 15:13:53何を当たり前なことを。
誰も非ユークリッド空間でピタゴラスの定理が成立つとは言ってないよ。
トンデモは除いてだが。
0157132人目の素数さん
2005/09/29(木) 15:17:45まあ、誤解をまねく用語なことは確か。
形式的証明でもちょっとおかしいけどね。
0158132人目の素数さん
2005/09/29(木) 15:32:00くらいにしときゃ誤解も無いんだろうけどな
0159132人目の素数さん
2005/09/29(木) 15:33:20数学者の間では既に証明されたと認められている定理でも
形式的証明はなされていないものは、ジュルダンの閉曲線
定理以外にも非常に多い。例えば、ワイルズにより証明が
なされたフェルマーの最終予想もその一つでしょう。この
研究はそれらの定理にも形式的な証明が与えられるように
なる第一歩となるのでないか、と期待できる
そうすると素直に読めるなwww
0160132人目の素数さん
2005/09/29(木) 15:36:27>>301
ポモ的なのに叩かないのは、そういう理由だったんだね!
土建屋=宇沢=長谷川=黒木 ← 隠れポモ野郎
禿藁=U健爾 ← 隠れポモ野郎
あほ鴨=中村 ← 隠れポモ野郎
303 :132人目の素数さん :2005/09/29(木) 15:26:53
>>302 >>295
こいつらって、結局
ポモと同じでしょ。
>そして、別の場所で、極端なことを言っているのではないかと非難された場合には、
>3 (a) に近い穏健だが当たり前の主張を述べて批判をかわします。
http://www.math.tohoku.ac.jp/~kuroki/FN/relativism.htm
0161132人目の素数さん
2005/09/29(木) 16:00:27したがってワイルズの証明は間違っているとやった人が
アメリカに居たねw
0162132人目の素数さん
2005/09/29(木) 16:04:15No
単に証明の計算機による検証のことを
信州大の教授が完全証明と称しているだけ
0163132人目の素数さん
2005/09/29(木) 16:19:35数理論理では、記号論理による数学の定理の証明のことをさす
用語があるんじゃないの? 形式証明でいいのかな?
0164132人目の素数さん
2005/09/29(木) 16:32:59もちろん、メタ論理のレベルでの、たとえば不完全性定理の「証明」とかとは
意味が違う訳ですが、文脈から言って誤解する可能性はほとんど無いですし
まあ、形式的証明とか形式証明とか言っとけば
言いたいことは通じるんじゃ無いでしょうか
0165132人目の素数さん
2005/09/29(木) 16:33:38> 形式証明でいいのかな?
他にも、証明図という呼び方をする場合もある。
面倒なので単に「証明」と呼んで、通常の証明を「非形式的証明」と言ったりもする。
0166132人目の素数さん
2005/09/29(木) 16:34:16「証明図」とか「証明木」とかは見た事がある。単に「証明」って言う事が多い。
「完全証明」と名付けてるのは見た事がない。
あと「形式証明」って言ったら、
普通は「証明する対象がメタでない」という事の強調として捉えると思う。
0167132人目の素数さん
2005/09/29(木) 16:35:30この世界は概ねユークリッド空間だから
非ユークリッド空間で成立するとされている全ての定理は
証明に失敗しているわけですね。
てゆうか1次元や2次元で成立する定理も全部ダメですね。
この世界は概ね3次元なんですから。
自然数もダメ。あれ無限だし。この世界にあるのは自然数の
有限部分集合だけだもんね。数学は窮屈な学問だね。
0168132人目の素数さん
2005/09/29(木) 16:36:31一つここに書いてくれないかね。
0169132人目の素数さん
2005/09/29(木) 16:41:530170132人目の素数さん
2005/09/29(木) 16:43:38計算機でチェックできる形式に書き下してくれ
0171132人目の素数さん
2005/09/29(木) 16:43:55そう。
>そんなものは、ユークリッドの公理から出るだろ。
物理的に切った貼ったするならユークリッドの公理に従うとは限らない(w
つまり、そこが盲点というわけだ。
0172132人目の素数さん
2005/09/29(木) 16:46:12勧違いしてしまいそうだから
数学会として公式見解を出しておく
必要がありそうですね
Up野先生,こういうときこそ
その指導力を善用してください
若手いじめではなく
0173132人目の素数さん
2005/09/29(木) 16:51:51原理的に計算機でチェックできるくらい厳密じゃないのかな
(実数論の公理を一寸手直しする必要があるかもしれない)
もっとも、この本は全く直観を排して書かれていることで有名だけども、
それでもとある「明らかだが証明が難しい」定理が、
"困難も無く"得られることになっているのだがw
0174132人目の素数さん
2005/09/29(木) 16:52:22そもそも証明が完全に公表されて無いんじゃなかったっけ
0175132人目の素数さん
2005/09/29(木) 16:55:35そのヒルベルトの幾何学基礎論による証明かい?
すり替えはよくないね。学問を否定する悪行だよ。
0176132人目の素数さん
2005/09/29(木) 16:57:30いや公表はされてるんだけど
あまりに膨大で入りくんでいるため
確認がとれない
最近の Aschbaher らの仕事で
あやしかった部分が克服されて
ようやく完成したと見ていいでは(?)
という話
0177132人目の素数さん
2005/09/29(木) 16:59:17中村八束氏の仕事の先駆といってもよいものだ。
つまり、ヒルベルトの証明と通常の作図による証明の差を理解すれば
形式的証明と通常の証明(あるいは説明)の差を理解できるはずである。
0178132人目の素数さん
2005/09/29(木) 17:03:01では、公式見解の叩き台を考えましょう。
数学者の間では既に証明されたと認められている定理ではあっても
形式主義的に満足できる証明がなされているものは、非常に少ない。
例えば、ワイルズによって証明がなされたフェルマーの最終予想も
形式的証明までは、まだ遠いようである。今回の中村氏らの研究は
それらの定理にも、形式的な証明が与えられるようになる第一歩と
なるのではないか、と大きな期待を抱かせるものである。
0179132人目の素数さん
2005/09/29(木) 17:05:12別にそんなこと一言も主張してないが
初めて習うときに多分に直観的な証明がされて何が悪い?
0180132人目の素数さん
2005/09/29(木) 17:08:29数学者の間では既に証明されたと認められている定理ではあっても
形式主義的に満足できる証明がなされているものは、非常に少ない。
例えば、ワイルズによって証明がなされたフェルマーの最終予想も
形式的証明までは、まだ遠いようである。今回の中村氏らの研究は
それらの定理にも、形式的な証明が与えられるようになる第一歩と
なるのではないかと我々数学者に大きな期待を抱かせるものである。
最後の行に「我々数学者に」を入れてみたけど
0181132人目の素数さん
2005/09/29(木) 17:08:47計算機によって証明が検証された!とか言っても
今度は計算機とそのプログラムの信頼性の問題が出てくるわけで
往々にして健全な直観の方が信頼が置けたりするわけで
まあ、たとえJordan曲線定理にしか適用できないようなモノだったにせよ、
それまで殆ど計算機科学者の机上の空論だった証明チェッカが
初めて実際に実際の数学の定理の証明をチェックした、
という意味で意義の有る仕事だとは思うけどね
0182132人目の素数さん
2005/09/29(木) 17:11:47形式的証明以外はすべてただの説明である、証明に非ず
って暗に言ってるような感じで一寸違和感があるな、、
直観が混じった証明か、原理的に論理規則と公理だけからできる証明かは
数学者だったら簡単に区別くらいつけられる
0183132人目の素数さん
2005/09/29(木) 17:13:51だから形式証明なんかほとんどの数学者は必要としてないんだって。
手軽に出来るならケアレスミスのチェック用に便利っていうだけ。
だけど手軽になんか出来ないだろ。
0184132人目の素数さん
2005/09/29(木) 17:14:12>初めて習うときに多分に直観的な証明がされて何が悪い?
問題は、その直観が隠れた前提を持っているかどうか。
例えば作図の場合、たいていの人は作図による合同と
物理的な「切った貼った」の違いに気づかない。
しかし、非ユークリッド幾何学のクラインモデルや
ポアンカレモデルを理解するにはこの違いに気づく必要がある。
0185132人目の素数さん
2005/09/29(木) 17:15:18>往々にして健全な直観の方が信頼が置けたりするわけで
それは今のところね。しかも、健全な直観を獲得するのは
ごく専門領域に限ったとしても大きな労力を要することは
君もよく知っているはずだよね
だから、コンピュータによる自動化が今後なされることは、
それなりに意味のあることだろう。まだ実用段階にはない
だろうけど。特に数学の証明問題の自習に役立つと思うし、
数学者だって自分の証明のチェックに使えるだろう
0186132人目の素数さん
2005/09/29(木) 17:17:51「必要ない」なんていったら、角が立つだろう。
これは政治的な話でもあるんだよ。素人の誤解を
解きつつ、見解は相手を立てる言い方にしないと
0187132人目の素数さん
2005/09/29(木) 17:19:19新聞記者が勝手に都合の良い所だけ切り取ってきた、という可能性もあるがな
0189132人目の素数さん
2005/09/29(木) 17:20:25>往々にして健全な直観の方が信頼が置けたりするわけで
プログラムのミスも人間のミス(w
それも含めて人間がミスしやすいのは明らか。
>>182
そう読むのは間違っている。
> 直観が混じった証明か、原理的に論理規則と公理だけから
>できる証明かは数学者だったら簡単に区別くらいつけられる
これは大嘘。数学者は無意識に直観を混入させている。
その直観が論理規則と公理で正当化できるかどうかなど
数学者にはさしたる関心はない。時間の無駄だからだ。
0190132人目の素数さん
2005/09/29(木) 17:21:41そんなに手軽に証明チェックが出来るようになるものかな?
普通証明する場合は同様に、で済ませるようなところだって
機械はそれじゃ理解してくれないし
0191132人目の素数さん
2005/09/29(木) 17:23:36当時の現実的可能性の少なさに負けたとも言える
その可能性を追求している人達を無碍に否定する
必要もなかろうて
0192132人目の素数さん
2005/09/29(木) 17:26:58いや、必要ないと思ってるならはっきりそういうべきだろ。
喧嘩が怖いチキンは真っ先に食われる。
0193132人目の素数さん
2005/09/29(木) 17:27:11>機械はそれじゃ理解してくれないし
だから、今はね。今後の可能性を否定
しなくてもいいでしょ。そういうこと
やってる人の研究を、部外者が見解を
出すに当たっては気の利いたリップ・
サービスをしてこうぜ
2chで誹謗中傷は、大いに結構だがw
0194132人目の素数さん
2005/09/29(木) 17:29:10・オレが理解できたらその定理は正しい
(ただしオレ自身が証明した定理を除く)
0195132人目の素数さん
2005/09/29(木) 17:30:04やれやれ批判と誹謗中傷と区別できない馬鹿がここにもいたか。
0196132人目の素数さん
2005/09/29(木) 17:31:22必要ないのは、多くの数学者の感覚に過ぎないだろ。
大体、数学会には「基礎論屋」だっているんだから
基礎論屋なんて追い出せ、という教条主義を掲げる
決意をこれからは持つというならそれもありかもな
そいつらは必要だと思ってやっているわけだから、
それに合わせてやれ
0197132人目の素数さん
2005/09/29(木) 17:32:18・オレが理解できないのに機械が検証したなんて認めない!
0198132人目の素数さん
2005/09/29(木) 17:34:34>ヒルベルトは「必要」という立場だったわけでさ
根拠は?
0199132人目の素数さん
2005/09/29(木) 17:35:02>それなりに意味のあることだろう。まだ実用段階にはない
>だろうけど。特に数学の証明問題の自習に役立つと思うし、
>数学者だって自分の証明のチェックに使えるだろう
実用化されれば、役立つじゃんか。まあ、実用化されるのに
どれだけ時間が掛かるのは分からんがなw
0200132人目の素数さん
2005/09/29(木) 17:35:31いまや、ロジシャンなんてソフトウェア科学会とか
科学哲学会あたりに亡命しちまったと思ったが(w
数学屋の嫌論理なんてのはヨーロッパの反ユダヤ主義
くらい根深いもんだろ。
0201132人目の素数さん
2005/09/29(木) 17:36:39一般に流布している常識を知らない?まあ、
常識が正しいという確証はないわけだが…
0202132人目の素数さん
2005/09/29(木) 17:39:06数学屋のプラトニズムという信仰の虚妄を明らかに
するものだからだろう。
数学的プラトニズムが極右なら
論理的フォーマリズムは極左
0203132人目の素数さん
2005/09/29(木) 17:40:24別に基礎論屋がこういう証明を支持するかというと
また微妙かもしれないけどね
>>200
50年前にこういうふいんきは無かったはず
というか、日本特有じゃないのかな、基礎論異端視がこんなに激しいのは
0204132人目の素数さん
2005/09/29(木) 17:41:370205132人目の素数さん
2005/09/29(木) 17:42:52常識なら根拠くらい挙げられるだろう。
0206132人目の素数さん
2005/09/29(木) 17:44:53>別に基礎論屋がこういう証明を支持するかというと
>また微妙かもしれないけどね
彼らは専門家だから、より慎重でしょう。
ただ、こういう方向性の研究自体には、普通の数学者
よりも親近感を持つ人が多いでしょう。中には、近親
憎悪的過剰反応を示す香具師もいるかも試練が。
0207132人目の素数さん
2005/09/29(木) 17:45:07>するものだからだろう。
どう明らかにするんだよ。
0208132人目の素数さん
2005/09/29(木) 17:46:28「ヒルベルトは形式主義の提唱者」という常識
0209132人目の素数さん
2005/09/29(木) 17:47:28いや、世界的傾向だね。
ロジックは結局言葉の学問だからね。
たいていの日本人は、ロジックが存在する意味すら理解できていない。
だから、極少数の理解者は、さながら隠れキリシタンのようなもの。
0210132人目の素数さん
2005/09/29(木) 17:50:15どっかの研究科みたいに、教条主義を掲げて別分野をパージしますか?w
0211132人目の素数さん
2005/09/29(木) 17:52:44『面白さ&有用さ』にあるからね。
0212132人目の素数さん
2005/09/29(木) 17:53:03俺は205じゃないけども
ヒルベルトの形式主義は別に計算機で証明をチェックすれば
厳密性が確保できる、とか言うことじゃなくて
証明を形式的に書き下せば自然数論なり実数論なり、
特定の形式的数学の無矛盾性が証明できるから、(りゃ
という思想だったはず
もちろん俺はヒルベルトの後継者だ!とか自負するのは勝手だけど
一寸ヒルベルトの考えに対する勝手な憶測が入りすぎかと
0213132人目の素数さん
2005/09/29(木) 17:53:03ロジシャンは興味を持つだろうね。
ただ、ロジシャンは素人のようにロジックに絶対的信頼は置いてない。
だから、フォーマルだから正しいとは言わない。
彼らが興味を持つというのは、正しいかどうかよりも、どういう
フォーマリズムによってそれが証明されるのかという仕掛け。
ある意味、マニアというかヲタク的興味。
0214132人目の素数さん
2005/09/29(木) 17:53:48有用さ>>>厳密性
基礎論屋は、死ね!
0215132人目の素数さん
2005/09/29(木) 17:54:48死ぬべきなのは君だと思うな
0216132人目の素数さん
2005/09/29(木) 17:54:51私見では置換群が鍵のように見えるんですが…
0217132人目の素数さん
2005/09/29(木) 17:57:39ヒルベルトがつきぬけてるのは、文字面だけ考えればイイ!
というところに気づいた点。
ただ、こういう発想は数学者にはとっても嫌われる。
美女も骸骨だけみりゃいいみたいな感じにとられるわけだ(w
0218132人目の素数さん
2005/09/29(木) 18:00:11マツシン先生いますか?
いたら返事をしてください
0219132人目の素数さん
2005/09/29(木) 18:02:11計算機でチェックするとは言ってないでしょ。大体、
当時はコンピュータがなかったんだから
ヒルベルトは2段構え
1.定理の客観性を確保するために、形式体系内で証明を行う
2.当該の形式体系が少なくとも全く無意味であることを保障
するためには、(有限の立場で?)無矛盾性を確認する
2はゲーデルによって(一応の)否定を見たわけだけど、1は
なんら否定を受けていないからさ
一応、形式的に証明されれば客観的な訳で、もちろん矛盾した
体系ならば、すべての命題が正しいから意味はないけど。その
場合であったとしても正しいということ自体は客観的ではある
0220132人目の素数さん
2005/09/29(木) 18:02:22いまどきの集合論屋は数学者です。
彼らを、基礎論屋とかロジシャンとか呼ぶとたいてい蹴られます。
0221132人目の素数さん
2005/09/29(木) 18:04:19>2.当該の形式体系が少なくとも全く無意味であることを保障
> するためには、(有限の立場で?)無矛盾性を確認する
すまん、書き間違えたよん。
2.当該の形式体系が少なくとも「全くの無意味」ではないことを
保障するためには、(有限の立場で?)無矛盾性を確認する。
0222The_Knight_of_Mathematics ◆uGlSZOV4Kc
2005/09/29(木) 18:04:38コンピューティングによる証明を否定するゆえはない
例えば ピタゴラスの定理の証明の一つなどで辺に接続する図形を移動することで証明とする場合を
否定するようなものだ
俺ってキングとは逆に幾何学大好きだから目で見てわかる証明のほうが美しいと感じる
0223132人目の素数さん
2005/09/29(木) 18:09:24別に客観性なんてヒルベルトの関心にはなかった筈。
>一応、形式的に証明されれば客観的な訳で
しかし実際には、形式的証明は激しく読みにくい。
したがって「機械は正しいといってるがオレにはチンプンカンプン」
という状況がおきる可能性大。客観的というより「無観的」といった
ほうがいい。
0224132人目の素数さん
2005/09/29(木) 18:12:27>1.定理の客観性を確保するために、形式体系内で証明を行う
これ普通に数学者がやってることなんじゃないの? ただ記号論理でやらないだけで。
0225132人目の素数さん
2005/09/29(木) 18:12:44だから別に読まなくてもいいんだって、
それはコンピュータに読ませるための
証明なんだからさ
ユークリッド幾何を勉強するのに幾何
学基礎論を読まなくてもいいでしょ
勉強をして感覚を養うのと、正しさを
厳密に確認するのは、違う作業だって
ことはよく知ってるでしょ
0226132人目の素数さん
2005/09/29(木) 18:13:26いや、全然やっていない。
0227132人目の素数さん
2005/09/29(木) 18:16:14もっと詳しく
0228132人目の素数さん
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
図形動かして証明するほうが早いんだよ
四色問題の証明もこの証明も
これと似たようなことしてるだけだろ
数理的な証明も不可能ではないけど
複雑な命題になるにつれて
そうした証明を読み解いて理解できるやつが少なくなる
0230132人目の素数さん
2005/09/29(木) 18:20:42だから、フェルマーの定理だってペアノ公理系から
(その肯定も否定も)導けるか、どうかは分かって
ないよ。数学者が証明したということと公理系から
形式的に導けるということは別物なの。
これが分かってないと、中村教授の「完全証明」と
いう言葉で誤解をしてしまう素人さんの一人に入る。
0231132人目の素数さん
2005/09/29(木) 18:21:11>だから別に読まなくてもいいんだって、
>それはコンピュータに読ませるための
>証明なんだからさ
コンピュータを信頼する根拠は?
>ユークリッド幾何を勉強するのに
>幾何学基礎論を読まなくてもいいでしょ
それはむしろ君の主張を否定するもののような希ガス
>勉強をして感覚を養うのと、正しさを厳密に確認するのは、
>違う作業だってことはよく知ってるでしょ
理解せずに正しさを確認できるという発想は
どこか精神を患っている希ガス
0232The_Knight_of_Mathematics ◆uGlSZOV4Kc
2005/09/29(木) 18:23:30パズルが噛み合うから証明できたよーんっていうようなものだろ
ほら見ろよ 噛み合ってんじゃん!って
その証明を否定しようにもスパコンひっぱってこなきゃならんし
20万行読まなきゃならんしで大変・・・
今後はこういう証明が台頭する状況になっていくかと
0233132人目の素数さん
2005/09/29(木) 18:25:17>ペアノ公理系から
なんでペアノ公理系からなの?
集合論の公理系でいいじゃない。
そこからフェルマーは証明されてんでしょ。
0234132人目の素数さん
2005/09/29(木) 18:28:43ああ、いろいろ使ってるからなあ。
しかし、素人の誤解とかいう時点で
君も玄人の誤解に陥ってるな(w
0235132人目の素数さん
2005/09/29(木) 18:30:13>理解せずに正しさを確認できるという発想は
>どこか精神を患っている希ガス
別に理解しなくても。「正しさだけなら確認」
できる。というのが、ヒルベルトの形式主義。
もちろん、それに対して貴方がどう思うかは、
自由だよ。
ま、単に「正しい」という言葉で意味しいてる
事が違うだけと思うが
ただ、「君の考える正しさ」は、主観的にのみ
確認できるものだと思うけど。それはプラトニ
ズムだな。もちろん、そういう立場もあるよね
0236132人目の素数さん
2005/09/29(木) 18:31:26>集合論の公理系でいいじゃない。
それも分かってないけど
0237132人目の素数さん
2005/09/29(木) 18:33:30はあ? それじゃ証明されてないんじゃない。
0238132人目の素数さん
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俺にはもうついてけんよ
0240132人目の素数さん
2005/09/29(木) 18:36:04だから、「基礎論の初歩」を知っている数学の先生に
聞いてみな、ね
この「中村氏の完全証明」と「普通の証明」の違いが
分からないんですけど、どういうことですか?、って
結論から言えば、「普通の数学者の証明」は形式的に
証明できるということとは違うんだ、って答えになる
0241132人目の素数さん
2005/09/29(木) 18:40:15>別に理解しなくても「正しさだけなら確認」できる。
>というのが、ヒルベルトの形式主義。
違うなあ。「理解しなくても」「確認できる」なんていうのは
君が勝手にそう思ってるだけのこと。
実際には数学の理屈は文字の操作に完全に還元できるという発想。
まあ、唯名論だな。
しかしこれは大きな落とし穴がある。
つまりそもそも文字操作として表した形式化が正しいかどうかは
分からんってこと。だから実は理解ぬきには客観性なんかないって
ことさ。論理マンセーの素人が必ず陥る初歩的な穴だな。
0242132人目の素数さん
2005/09/29(木) 18:40:19だから、中村氏の発言になるんでしょ?
ジョルダンの曲線定理は、数学者の言う普通の意味では
証明はできていたけど、形式的証明はできていなかった。
今回、我々はそれに成功したぜ
って言っているの。
0243132人目の素数さん
2005/09/29(木) 18:43:05君はもしかしてワイルズの証明はどこかで
公理に拠らない直観を使用しているかもしれないから
計算機で確認するまで証明されたとは認めないつもりかな
おかしな人だなあ、というのが普通の数学の人の反応な訳だけど
0244132人目の素数さん
2005/09/29(木) 18:43:58たとえ証明の途中で集合論的な選択公理を援用したにせよ、
原理的には証明からそのような除去できる、って定理があったから
かなり弱い公理から導けると思って間違いないかと
0245132人目の素数さん
2005/09/29(木) 18:44:05いまどき、基礎論なんて古臭い言葉を繰り返す奴は
ロジックの初歩も知らんというのが相場。
こっちは、ロジシャンから聞いたこと書いてるんだよ。
0246132人目の素数さん
2005/09/29(木) 18:45:50>結論から言えば、「普通の数学者の証明」は形式的に
>証明できるということとは違うんだ、って答えになる
それは程度問題じゃないの。本質的違いじゃなくて。
だから今回みたいに数学者の証明を書き下していけば機械に通るわけで。
0247132人目の素数さん
2005/09/29(木) 18:46:08マジックの初歩も知らんというのが相場。
こっちは、マジシャンから聞いたこと書いてるんだよ。
0248132人目の素数さん
2005/09/29(木) 18:46:30あのねえ、普通の数学者は、原理的には時間をかければ
計算機で検証可能なレベルで、厳密に定理を証明できるだけの能力は持ってるよ
(まあ幾何学者とか一部あまり厳密で無い人も居るけど)
単に時間が無駄だからそうしないだけでね
0249132人目の素数さん
2005/09/29(木) 18:46:45そこは問題にしない、というのが形式主義だろ?
君がその考えは取りたくないというのは勝手だよ
しかし、それだとどこにも客観性はないが。別に
そういう立場はありだ、と思うよ。でも、それは
貴方の考えで。いろんな考え方があるの。
形式主義の考え方ならこうなるよ、って言ってる。
で、中村の完全証明っていうのは、そう言う話だ。
それに価値があるか、どうかは人それぞれの価値
観だ。俺も「ジョルダンの曲線定理の形式証明」
自体にそんなに価値がある、とは思ってないけど。
これは俺の個人的価値観だから。
0250The_Knight_of_Mathematics ◆uGlSZOV4Kc
2005/09/29(木) 18:46:58平面上の閉じた曲線は、
↓
○
↑
平面を曲線の内と外に分ける
これが「ジョルダンの曲線定理」だっ!!!
生徒→ ('A`)「・・・・」
0251132人目の素数さん
2005/09/29(木) 18:49:13激しく勘違い。もう君は駄目だ。「基礎論の初歩」を知ってる
普通の(基礎論でない)数学者に聞いてみろよ。直接
やっぱり公式見解が必要かな。こういう勘違い君がいるとこを
見ると。どうにかしてくれって感じだが
0252132人目の素数さん
2005/09/29(木) 18:50:23>そこは問題にしない、というのが形式主義だろ?
重大な間違いだな。誰もそんな馬鹿げたことはいっていない。
>しかし、それだとどこにも客観性はないが。
君が間違ってる。むしろ問題にしないほうが客観性がない。
そういう立場は君だけの主観的なものだな。他人には通用しない。
君の同類には通用するかもしれないが、具体的な事例になると
君と君の同類の見解はことごとく相違し、了解がとれなくなるだろう。
要するにコミュニケーションを否定した独我論に陥ってるわけだ。
プライドばかり強いとそういう馬鹿げたことになる。
0253132人目の素数さん
2005/09/29(木) 18:52:44だから、君のいう「基礎論の初歩」は間違いだよ。
まったく素人に限って勝手に自分の中に似非専門家を
つくるから困ったもんだ。素人が即座に専門家に
なれるわけがないだろ。
0254132人目の素数さん
2005/09/29(木) 18:55:36何だか、数学の話じゃなくなってるんですが…
何だか、君は哲学的見解を主張されてるようで
数学者は「数学者同士で」、ある程度、共通の
主観を持っているから高度な数学の話が通じる。
実際、俺はそう感じているよ
0255132人目の素数さん
2005/09/29(木) 18:57:41はあ?初歩なんだから、専門家じゃなくても分かっていても
可笑しくないだろ。
数学の専門家じゃなくても、数学の初歩を知ってる人はいる
よね。
0256132人目の素数さん
2005/09/29(木) 18:58:350257132人目の素数さん
2005/09/29(木) 18:59:10>>249の「そこは問題にしない」というのは数学じゃないよ。
>数学者は「数学者同士で」、ある程度、共通の主観を
>持っているから高度な数学の話が通じる。
>実際、俺はそう感じているよ
共通かどうかはともかくとして、実際には数学者自身の理解と
相互の了解が、数学の定理の正しさを根拠づけているという
主張は私自身がここでしてきたことで、いまさら君の主張だと
言い張られても迷惑なんだが。
0258132人目の素数さん
2005/09/29(木) 19:01:22いや、初歩だから、素人が誤解しても可笑しくないんだよ。
見当違いのことをいう人は、たいてい初歩からダメだよね。
君がそう。どうせ独学だろ?だから誤解したまま気づかないんだ。
独学は結局自慰だからな。
0259132人目の素数さん
2005/09/29(木) 19:03:00勘違いしてるのは君だよ
俺は別に数学の普通の論文がどれくらい論理的に緻密に
書かれてるか、なんてことは主張して無い
ただ書こうと思ったら書けるよ、と言ったまでのこと
0260132人目の素数さん
2005/09/29(木) 19:04:04>相互の了解が、数学の定理の正しさを根拠づけているという
>主張は私自身がここでしてきたことで、いまさら君の主張だと
>言い張られても迷惑なんだが。
だから、それが数学者が普通の意味で言う証明です。
それと、「形式的証明」は違いますよ、って言う話
なんだがなあ。それは分かるでしょ。
俺は、普段、形式的証明なぞ全くしないし、貴方の
定理は(かくかくしかじかの形式体系で)証明でき
ますか?と聞かれたら、「全く分かりません。どう
なんでしょう?」としか、答えようがないよ。
0261132人目の素数さん
2005/09/29(木) 19:05:390262132人目の素数さん
2005/09/29(木) 19:10:17普通はしない。それに普通の証明したからって、
それで形式的に証明できるのか、どうかなんて、
全然、分からないよ
で、今回、中村は形式的に証明できましたって
話でしょ。
もし、今までの数学者の証明=形式的証明なら
中村の「初めて」って話は嘘になるけど、俺は
嘘だと別に思わないな
0263132人目の素数さん
2005/09/29(木) 19:12:30一階の述語論理が人間の推論様式を全般に渡って記述しうるというのは
十分な検証を要する一種のドグマである。」 by 某W先生
「一階の述語論理」の部分を「NBG集合論」にしてみたり、
「人間の推論様式」の部分を「数学者の推論様式」にしてみると、
>書こうと思ったら書けるよ
ってのは楽観的すぎかなとも思う。
0264132人目の素数さん
2005/09/29(木) 19:14:23ホモロジーって結局何なの?
ttp://cheese.2ch.net/math/kako/1009/10092/1009270205.html
0265132人目の素数さん
2005/09/29(木) 19:15:40まあ初めて「形式的に証明」できました、じゃ無くて
初めて「完全証明」できました、なんて言っちゃってるけどな
>>263
まあそりゃそうだね
0266132人目の素数さん
2005/09/29(木) 19:19:22しかし、「形式的証明」は今回、初めて我々の手によって与えら
れましたって言うんだから
結局、ジュルダンの定理の「普通の証明」と「形式的な証明」は
違うわけで
0267The_Knight_of_Mathematics ◆uGlSZOV4Kc
2005/09/29(木) 19:28:29ジョルダンの曲線定理とジュルダンの定理はどう違うんだ?
0268132人目の素数さん
2005/09/29(木) 19:32:02ジェルダンの曲線定理の「普通の証明」なら、とっくに
あった、でFA。
0269132人目の素数さん
2005/09/29(木) 19:33:30>結局、ジュルダンの定理の「普通の証明」と「形式的な証明」は
>違うわけで
誰も同じとは思ってないだろ。
だけど、これは量の問題であって質の問題じゃないだろ。
他の証明、例えばフェルマーの定理の証明だって時間と手間を
かければ形式証明が出来るだろう。そんなことは昔からわかってることだろう。
0270132人目の素数さん
2005/09/29(木) 19:35:57>ポーランドの数学者ら16人との約14年間にわたる共同作業
って14年間も何してたんだろ
0271132人目の素数さん
2005/09/29(木) 19:43:06>かければ形式証明が出来るだろう。
その肯定が形式体系から証明できるか、どうかは
分かりません。
ただし、その手の専門家によれば、今までの経験
から予想するに証明できる公算が高いのではない
か、という噂なら聞いたよ
「時間と手間を掛ければ、形式的証明ができる」
ことが分かってるなら形式式証明ができてるのと
同じことじゃないか?
でも、少なくともジョルダンの曲線定理は、そう
じゃなかったよね。ということは「数学者の言う
証明」は「形式的証明」では必ずしもないという
ことだ。
で、ワイルズのフェルマーの定理の証明が形式的
証明だと言う根拠は何なの?
数学者が「形式的証明」であると言ってたかな?
0272132人目の素数さん
2005/09/29(木) 19:46:15形式的に証明できるか、どうかは分からない
よね
形式的にも証明できそうだ、という「予想」
することは何ら問題ではないけどね
0273132人目の素数さん
2005/09/29(木) 19:49:29>かければ形式証明が出来るだろう。そんなことは、
>昔からわかってることだろう。
何が分かってるの?フェルマーが証明されたのは最近。
今もまだ形式的な証明ができるかどうかは分からない。
基礎論の専門家の間では、できるのではないか?、と
予想されているという噂は聞いたよ。
0274132人目の素数さん
2005/09/29(木) 19:52:04誰もWilesの200ページ弱の証明がそのまま形式的証明だなんて言ってないだろ?
そんな勘違いをしてるのは君だけ
>でも、少なくともジョルダンの曲線定理は、そうじゃなかったよね。
実際に形式的な証明が出来ただろ?
「直感的には当然だが、誰も数学的に完全な証明ができなかった」
なんていってるのは中村教授とそのお仲間だけで
平地健吾だって小島定吉だって、オリジナリティの低い低レベルな結果だ、と
内心考えてると思うよ
0275132人目の素数さん
2005/09/29(木) 19:54:54>そんなことは昔からわかってることだろう。
分かってる、ということは
仮定:数学者が(数学者じゃなくてもいいが)こうこうこう言う風に証明
⇒
結論:その定理は形式的に証明可能
という定理でもあるのかい?そんなのがあったら
教えて欲しいなあ。で、ワイルズの証明が、その
定理の仮定を満たしてる事も確認できてるのかな
0276132人目の素数さん
2005/09/29(木) 20:00:02>実際に形式的な証明が出来ただろ?
ジョルダンの場合はね。他の定理もそうだ、というのは
どうして分かるんだい?
分かるというなら『「普通の証明」⇒「形式的証明」』
という定理が成り立つんだよねえ。
つか、その前に「普通の証明」というのを数学的に定義
しなきゃならんがwww
0277132人目の素数さん
2005/09/29(木) 20:01:46単に、必要があれば、充分形式的なレベルまで証明を緻密にする
自信がある、というだけだろ
証明の形式化のどの部分がそんなに難しいと考えてるのかな?
少なくともZFCの公理から、必要な諸概念を定義して、
完全に形式的に証明するのは、述語論理の基礎を理解している数学者には
簡単なことだと思うがな
今回14年掛かったことだって、単に能力が欠けていた、としか思われない
0278132人目の素数さん
2005/09/29(木) 20:06:18ほとんどは「形式的にも証明できる」だろう、という予想でしょ。
よく考えたらゲーデルの第二不完全性定理があるじゃん。
「無矛盾性を意味する(とある)命題」が正しいけれども、
それは形式体系では証明できないって定理だね。
0279132人目の素数さん
2005/09/29(木) 20:07:16他の場合も出来るはずだ、という強い確信があるだけだよ
もちろん確実な根拠なんて無いわけだが、
それは、集合論の公理系は矛盾しているかもしれないのに、
実際には現今の数学者は、そんな可能性微塵も考えずに、
無矛盾に決まっている、その無矛盾な集合論で基礎付けできる現在の数学も
無矛盾だろう、と判断して研究を進めるのと同じことでしょ?
それを、無駄に不安を煽るのは、昔杞の国の人が、
天が崩れて落ちてきたらどうしようと憂いて夜も眠れなかった、という故事と一緒で
単なる無駄な取り越し苦労だと考えるべきかと
0280132人目の素数さん
2005/09/29(木) 20:11:23>自信がある、というだけだろ
何だ、自信の話ですか。それは「かくかくしかじかの定理」は
形式的にも証明できると私は予想しています、って話だね。
予想することと、確認することは別だよね。
0281132人目の素数さん
2005/09/29(木) 20:12:41他の場合って、どの場合よ。現に出来ないものを
ゲーデルは見つけたでしょ?
0282132人目の素数さん
2005/09/29(木) 20:13:04それがどうしたの?
もしかしてそれが
>「数学者によって証明されている定理」の
>ほとんどは「形式的にも証明できる」だろう、という予想
に対する反例になると考えているのかな?
君はゲーデルの第二不完全性定理を理解していませんね
そもそもその文脈で挙げるのは第一不完全性定理で充分なはずだけど
0283132人目の素数さん
2005/09/29(木) 20:15:30そりゃ手でやりゃあ 14 年もかからずできるさ
問題はどうやって数学的概念を計算機に理解させるか.
俺らが何気なく定義するようなものも,直感(というよりも常識)が多分に入るから,
それを計算機に理解させるためにたくさん手続きが必要になる.
だいぶ基本的な定義が出来上がった後でも,「領域が有界」であることを定義するために
120個も条件連ねなきゃならんのだから,全部証明するのに苦労するかは押して知るべし.
0284132人目の素数さん
2005/09/29(木) 20:19:22別に「形式的証明」がなくても不安じゃありませんけど。
というか、形式的証明ができない事が分かったとしても
不安じゃないよ
無矛盾性の証明は形式的に証明できないね。でも、不安
じゃありません。自分の定理が、仮に「形式的に証明」
できなかったとしても不安ではありませんね。
その否定が形式的に証明されたのなら、俺って馬鹿、と
思うだろうけど。そんなことをする暇人はいないから、
気にしてないけどね
0285132人目の素数さん
2005/09/29(木) 20:23:07>ほとんどは「形式的にも証明できる」だろう、という予想
に対する反例になると考えているのかな?
はあ?反例って、予想って書いたけどさ、これは
数学的な定理じゃないよね。
「ほとんど」ってあるよね。これって、数学的な
定義になってないじゃんか?
だから、この予想って書いたけど、これはただの
感想だから。反例も証明もあるわけない。人それ
ぞれの感想だからさ
0286132人目の素数さん
2005/09/29(木) 20:23:56(無矛盾で、再帰的に公理化可能ならば、)
その体系の無矛盾性とメタレベルで同値になる、従って直観的には真となるはずの
命題ConTが、【その体系内では】証明できない、という定理でしょ?
だからその体系内でその定理がたとえ証明できなくても、
適当に公理を付け加えた体系T'では普通に証明できて何も困らない
だから計算機で検証不可能な定理の存在を示していることにはならないよね
だから
>現に出来ないものをゲーデルは見つけたでしょ?
これは君の明らかな勘違い
0287132人目の素数さん
2005/09/29(木) 20:25:15>「数学者によって証明されている定理」の
>ほとんどは「形式的にも証明できる」だろう
と言ったとしても、これはその人の感想を述べただけね
0288132人目の素数さん
2005/09/29(木) 20:26:24予想に反する例、「ほとんど」に当てはまらない例、と言わないと分かって貰えないかな
0289132人目の素数さん
2005/09/29(木) 20:27:32>適当に公理を付け加えた体系T'では普通に証明できて何も困らない
それは分かってる、ってば。
でもさ、「証明したい定理を公理に加えた体系T'」では、その定理は
証明できるよねwww
0290132人目の素数さん
2005/09/29(木) 20:29:20そうだよ
だからどうしたの?
じゃあ>>281の>現に出来ないもの
って何のことだよ?言ってみてくれよ
0291132人目の素数さん
2005/09/29(木) 20:31:05当てはまるか、当てはまらないか、はどうやって決めるの?
>予想に反する
予想に反してないか、どうか、は?
ただの感想ですか?
0292132人目の素数さん
2005/09/29(木) 20:35:14どうやら、終わったみたいだね。
だから、「無矛盾性を意味する(とある)命題」が
その形式体系では証明できないってこと。
「無矛盾性を意味する」というのは、ここでの話し
ではあまり関係ないがな。
0293132人目の素数さん
2005/09/29(木) 20:38:49形式的に証明できれば当てはまるし、予想に反しない、
形式的に証明できないものは当てはまらないし、予想に反する
それくらい文脈から明らかだろうに
>>281によると
>現に出来ないものをゲーデルは見つけたでしょ?
だそうだから、その「現に出来ないもの」が予想に反するんじゃないかな
それと、数学的なstatement以外を全て「感想」で片付けるのは
止めてくれないかな
別にこのスレはひたすら数学的な定理と証明を書き込むスレじゃないんだからさ
0294132人目の素数さん
2005/09/29(木) 20:42:18>ある定理を正しいと認めた数学者が、
>その定理が成り立つ適当な公理系が
>何であるか?についてまで分かって
>いるとは限らないよ。
もちろん、適当でなければ、いくら
でも思いつくよ。例えばその定理を
定理を含んだ公理系とかね。www
0295132人目の素数さん
2005/09/29(木) 20:43:24頼むから名前欄に仮のハンドルをつけてくれ
0296132人目の素数さん
2005/09/29(木) 20:48:25>その定理が成り立つ適当な公理系が
>何であるか?についてまで分かって
>いるとは限らないよ。
で、ジョルダンについては、ごくごく常識的な
公理系で形式的に証明できました、ということ
でしょう
もちろん、これも感想だけどさ。何か異論ある
感想を否定はしてない。感想は感想に過ぎない
というだけのことだよ。
0297132人目の素数さん
2005/09/29(木) 20:51:060298132人目の素数さん
2005/09/29(木) 20:51:34>定理は(かくかくしかじかの形式体系で)証明でき
>ますか?と聞かれたら、「全く分かりません。どう
>なんでしょう?」としか、答えようがないよ。
これも結論だね。感想だけどさ。
0299132人目の素数さん
2005/09/29(木) 20:55:03普通の数学をやっているから。
で、自分が証明した定理が成立する適当な「形式
体系」なぞさっぱり分からないね。それで不安に
なったりはしないよ
これも感想だ
0300132人目の素数さん
2005/09/29(木) 20:55:380301132人目の素数さん
2005/09/29(木) 20:58:37証明できる、というのは大昔に数学者が確認したことなんだよ
今回の「完全証明」とやらの意義は、Jordan曲線定理を証明するのに
必要な公理の強さを確定したとか言うことじゃなくて、
proof checkerが、実用化に近づいた、ということだろ
0302132人目の素数さん
2005/09/29(木) 21:00:28>証明できる、というのは大昔に数学者が確認した
>ことなんだよ
じゃあ、その体系で形式的に証明されてたんだね。
ホント?
0303132人目の素数さん
2005/09/29(木) 21:02:32>その定理が成り立つ適当な公理系が
>何であるか?についてまで分かって
>いるとは限らない
しかし、集合論的な一部の数学を除けば、ZFCの範囲で大体事足りる
事足りない場合でも、基本的には、ZFCから独立かどうかを判定する
ための一般論は確立されている、というのが
常識的な数学者の所信(君の言う「感想」w)だと思うがな
そう思わないとしたら、基本的に感覚がずれている
0304132人目の素数さん
2005/09/29(木) 21:04:05何が「じゃあ」なのか分からないが
まだ形式的な証明と、普通の数学者の証明の区別も付かないのかなあ、、
もう説明する気無いよ
0305132人目の素数さん
2005/09/29(木) 21:04:10俺は自分の証明して、論文に発表した定理が、
「適当な公理系から形式的に証明できること」
なんて全く確認してない。他人の論文を読む
ときもね。
形式的に証明できることなんて、普通の数学
者は全然、確認しないと思うが?
0306132人目の素数さん
2005/09/29(木) 21:06:26だから、違うんでしょ。違うなら
普通に証明したからって、形式的に証明できるか
どうかは、分からないよね
0307132人目の素数さん
2005/09/29(木) 21:07:10>普通に証明したからって、形式的に証明できるか
>どうかは、分からない
0308132人目の素数さん
2005/09/29(木) 21:07:10とりあえず http://mizar.org/fm/ と20万行目に目を通したんだけど,ほとんど全てが
定式化のための定式化で冗長としか思えんかった.
知識蓄積する以外になんかこのあたり簡単にできんかな?
0309132人目の素数さん
2005/09/29(木) 21:07:31多少論理学の知識があれば、形式的に証明するのは簡単そうだ、
と分かるはずだから問題ないよ
0310132人目の素数さん
2005/09/29(木) 21:08:37PCにWebブラウザのクッキー情報が残ると、なんか不都合なことでもあるの?
0311132人目の素数さん
2005/09/29(木) 21:09:23>どうかは、分からない
ジョルダンの定理は普通に証明されていたが、今回、
形式的に証明がなされた、ということでいい訳だね
0312132人目の素数さん
2005/09/29(木) 21:12:12Goedelがある論文の中で
これこれのformal proofは、まともに書くと長くなるが、
これこれメカニズムを入れれば、短縮できる、みたいな
証明工学なことにも触れているのは流石だ、と言って
林晋が褒めてたかと
もうそのページ消されたのでInternet Archive探さないと残ってないっぽいけど
0313132人目の素数さん
2005/09/29(木) 21:15:30全然、思わないがな。それに「公理系」と「定理」の
採用の仕方によるね。普通の数学者は、どんな形式的
体系で、どんな命題に置き換えるかなんて、意識して
ないと思うが。
だから、お前らの言っていることは、多くの場合には
数学者の証明を見ると適当な公理系と定理に対応する
適当な命題を思いつく自信があるよということでしょ。
君の感想だよね。別に、否定するつもりはないけどね。
0314132人目の素数さん
2005/09/29(木) 21:17:50http://www.shayashi.jp/HistorySociology/HistoryOfFOM/Books/books.html かな?
>この本では技術的には一貫して計算機科学的視点からゲーデルの定理を見ています。
>その方が自然なのです。例えば,ゲーデル数を素因数分解で定義しますと、
>実際にやるとトンでもないことになりますが、普通の文字列のコード化と同じにすれば
>スイスイです。また、対角線論法も、コンピュータでは、例えば、lisp を使えば、
>本当に実行して遊ぶことができます。
0315132人目の素数さん
2005/09/29(木) 21:18:360316132人目の素数さん
2005/09/29(木) 21:21:25もう一度、書いておく。
>自分が証明するときに形式的に証明されるか、どうか、なんて
>気にしちゃいねーよ。だから、形式的に証明できるか、どうか
>なんて分からないし、仮に形式的に証明ができないものだった
>としても、気にしないね。普通に証明できればOKだ。
0317132人目の素数さん
2005/09/29(木) 21:21:57>しかし、さすがゲーデルというか、そういう定義を完全に展開してしまうと
>扱っている論理式が非常に大きくなるだろうとか、Principia Mathematica のよう、
>定義のメカニズムが入っていれば、短くなるが、などの証明工学的な話もちゃんと議論しています。
>前原先生がイオタ記号を使われたのは、ここら変を曖昧にしておくのが嫌だったからでしょう。
ここらへんのことです
論理式の長さ、でしたね、失礼
まあ証明の長さにも同じことは言えると思いますが
0318132人目の素数さん
2005/09/29(木) 21:23:39だから>仮に形式的に証明ができないものだった
そんなものがあるかもしれないと信じてる数学者は殆どいねえっていうのに
>>306-307を見てレスする気力がなくなったけどね
0319132人目の素数さん
2005/09/29(木) 21:31:43具体的に「定理と公理系」を特定しなければ、
形式的に証明できるとか、できないとかが、
意味を持たないだろう。
ということは、「そういうものがある」という
のもただの感想だし、「そういうものがない」
というのもただの感想にしか過ぎないね。
君は感想を言ってるんだ。俺もだがな。自覚し
ようぜ
0320132人目の素数さん
2005/09/29(木) 21:33:03その定理は形式的に証明できるからな。
0321132人目の素数さん
2005/09/29(木) 21:34:14Principia Mathematica のようなメカニズムって,数々の省略記号のことかな?
だとしたら相当楽観的な判断に思えるんだがなあ.
0322132人目の素数さん
2005/09/29(木) 21:36:48少なとも、俺はあると思うぜ。
ない、と思う奴もいるだろう。
いずれにしても、どちらも間違ってない訳だ。
ということは「意識調査」の問題だな。
各国の数学者に「意識調査」をして見るのも
いいかもしれないね。時代とか、国によって
どう変わるかとかね。ちょっと見てみたい。
0323132人目の素数さん
2005/09/29(木) 21:42:572.「普通に証明できてるものは『適当な』公理系で形式証明可能」
いや、「できないものもある」
→ どちらを考えるにしても、ただの感想。正しい、間違って
いるの問題ではない。因みに、俺は「できない派」だけどね。
0324132人目の素数さん
2005/09/29(木) 21:44:28『適当な』という部分が個人の主観だからね。
0325132人目の素数さん
2005/09/29(木) 21:48:48だから「確信、所信」を「感想」に変えないでくれないかな
意味が違う言葉だからさ
>>323
具体的にはどういう定理がそうなると思うのかな?
まさか具体例は無い、なんてことは無いだろうけど
0326132人目の素数さん
2005/09/29(木) 21:50:37証明ができない定理がある
と俺は思う。もちろん、これはただの感想。『適当な』というのが
個人的主観だから
0327132人目の素数さん
2005/09/29(木) 21:53:19>だから「確信、所信」を「感想」に変えないでくれないかな
>意味が違う言葉だからさ
意味が分からないな。だって、普通の意味で反証可能命題では
ないじゃない。ということは、感想だろが?
確信という言葉は、反証可能な命題でなければ意味ないぜ
0328132人目の素数さん
2005/09/29(木) 22:04:290329132人目の素数さん
2005/09/29(木) 22:05:34>証明可能
これは感想とか、意見の類でしかないよね。ご自由にどうぞ
俺の意見は、「証明不可能なものもある!」だ。というか、実は
どっちでもいいんだけどね。
俺が本当に言いたいことは、「それって、どちらにしても、結局
意見にしか過ぎない!」ということ
0330132人目の素数さん
2005/09/29(木) 22:09:52確信って、「正しいか、間違ってるかが決まる」ことに対して
言うんでしょ。決まらないことに言うのは、ただの意見だよ。
というか、どちらも正しい訳だから矛盾が許容される世界での
「おしゃべり」だね。それも、結構だと思うよ
0331132人目の素数さん
2005/09/29(木) 22:12:05あんたは不可能なものがあると信じる根拠を挙げなきゃ意見未満だよ
あと確信ってのは正しいと信じていること。決まるかどうかとは無関係。
さらに言えばあんたの立場では決まらないかどうかもわかんないでしょ?
0332132人目の素数さん
2005/09/29(木) 22:16:25意味が分からない。だって、「適当な」って言うのが
完全な個人の主観じゃない。
決まらないよ。何度も言うように「適当な」ってのが
主観だからね。
ここをどうするのよ。もちろん、そこを定義すれば、
決まるかもね。
実は、定義があるのかな?www
0333132人目の素数さん
2005/09/29(木) 22:19:15工房でしょうか
スルーが吉かと
0334132人目の素数さん
2005/09/29(木) 22:19:25「適当な」ってままじゃ、何を言っても意見だよ。
君の経験に基づく感想だ。
だから、「意識調査」でもしようぜ、な
0335132人目の素数さん
2005/09/29(木) 22:22:38一方的に使ってる言葉だよ
よく読んだほうがいいよ
0336132人目の素数さん
2005/09/29(木) 22:23:58あれ?今、数学のことを話てるんだよね。
数学で「適当な」というだけで、定義が
なければ、それはまだ意見でしょ。もち
ろん、今後、定義がなされて定理になる
可能性を秘めた意見もある。でも、
>普通に証明できてる定理は、『適当な』公理系で形式主義的に
>証明可能
なんての、上手く定理に出来るもんかね?
0337132人目の素数さん
2005/09/29(木) 22:25:07何学的にですか?
0338132人目の素数さん
2005/09/29(木) 22:27:00んなこたーない.論文とかで「適当な仮定の下で」ってj表現見たこと無い?
数学で「適当」って言ったら,妥当な条件が共通知識としてあるものだよ?
0339132人目の素数さん
2005/09/29(木) 22:27:59>その定理を公理として含む公理系を考えれば
>その定理は形式的に証明可能である
正しいねえ。
0340132人目の素数さん
2005/09/29(木) 22:32:07うんうん、あるね。それは、「条件」を明確に
あげることが出来る場合だよね。じゃあ、頑張って
>普通に証明できてる定理は、『適当な』公理系で形式主義的に
>証明可能
の「適当な」も明確な条件に置き換えてみてよ。もしも出来たら
いい仕事じゃないの?うんうん、すごいねwww
0341132人目の素数さん
2005/09/29(木) 22:44:34数学をすることと数学について話すことの区別も付かないのかなあ
しかもお前が言い出した良くわかんない命題を
なんでうまく定理にしないといけないのか
>>323のできない例って具体的にどういう場合を想定してるのか
いい加減教えてくれよ
0342132人目の素数さん
2005/09/29(木) 22:45:570343132人目の素数さん
2005/09/29(木) 22:51:43だから、命題じゃないんでしょ。じゃあ、
意見でしょ。自分で認めたのね。
いや、それとも何か別の命題があるのかな
別に数学的な命題じゃなくてもいいけど。
物理的命題もあれば、医学的命題もある。
いずれにしても、命題は正しいか、正しく
ないかが決まるものだけどね。
0344132人目の素数さん
2005/09/29(木) 22:52:450345132人目の素数さん
2005/09/29(木) 22:58:25>いい加減教えてくれよ
「たくさん、あるんだから、その中にはあるんじゃね」って
感じの話だ。感想だけどね。
喩えて言えば「宇宙は広いから地球以外に生命体がいても、
いいんじゃね」というような感想。この場合、まだ、生命体
とかに一応の定義ができそうだから、まだ命題っぽいけど。
それに比べても、
>普通に証明できてる定理は、『適当な』公理系で形式主義的に
>証明可能
こっちは、全く命題になってないから、どうしようもない。どう
あがいても、感想だ。
もしも君が感想以上のことを言いたいなら、どうぞ言って下さい
よ。
0346132人目の素数さん
2005/09/29(木) 23:00:25>いいんじゃね」
今数学の話してたんじゃ無かったのか?
物理や生命科学が、形式的に証明できると思ってるのか?
0347132人目の素数さん
2005/09/29(木) 23:01:26なんてことは、思ってないよ。
だから、「意識調査」を見てみたい気もするんだよね。
0348132人目の素数さん
2005/09/29(木) 23:04:38>普通に証明できてる定理は、『適当な』公理系で形式主義的に
>証明可能
は,あなたが >>329 で引用として持ち出したわけですけど,その原文は
どこにも無いわけですよ.あなたが勝手に妄想で持ち出した引用文なわけですよ.
勝手に人の主張を捏造しないでもらえますか?
0349132人目の素数さん
2005/09/29(木) 23:04:40「感想」の一言で片付ける
自分はというと都合が悪くなったら突然
数学の話をそらして宇宙の生命体の話をしだす
こいつ頭が悪すぎる
駄目だ
0350132人目の素数さん
2005/09/29(木) 23:05:06形式的に証明できなくても、数学的に証明できなくても
科学的命題というのはあるよね。分からないかな?
>「宇宙は広いから地球以外に生命体がいても、
>いいんじゃね」
これは、宇宙とか生命体があやふやだから、命題と
して不十分だと思うよ
0351132人目の素数さん
2005/09/29(木) 23:06:25だから、さっきから言ってるでしょ。
貴方の感想でない主張はどこにあるの?聞かせて
0352132人目の素数さん
2005/09/29(木) 23:06:38適当な、という言葉を二重括弧で括って
自分勝手な意味で使ってますよ、ということをアピールしてたから
誰もその発言には突っ込んでない訳なんだけどな
0353132人目の素数さん
2005/09/29(木) 23:09:350354132人目の素数さん
2005/09/29(木) 23:09:59>「感想」の一言で片付ける
すべてではないよ。たまたま、ここでは感想以外のものが
見当たらないだけ。
0356132人目の素数さん
2005/09/29(木) 23:12:24書いてみて
0357132人目の素数さん
2005/09/29(木) 23:13:55>>343 で
>命題じゃないんでしょ。じゃあ、 意見でしょ。
とあるのであんたの中では 「not 命題 ≡ 意見」 と判断されても仕方が無いわけだが
ところで意見と感想は同じ?
0358132人目の素数さん
2005/09/29(木) 23:18:13「誰々さんのこれこれというタイトルの論文は
いいね」
これは感想だね。正しいとも、決まらないし、
間違ってるとも、決まらない。
でも、こうした感想には意味がある事もある。
また、それぞれの意見を持つ事は、自由だね。
対立する意見があったからと言ってどちらかが
間違っているという訳でもない。
0359132人目の素数さん
2005/09/29(木) 23:19:15うん、同じ意味で使ってる。
0360132人目の素数さん
2005/09/29(木) 23:20:22not「命題 ≡ 意見」
これは当然です。
0361132人目の素数さん
2005/09/29(木) 23:25:50「普通に証明できてるものは『適当な』公理系で形式証明可能」
いや、「できないものもある」
→ どちらを考えるにしても、ただの感想。正しい、間違って
いるの問題ではない。因みに、俺は「できない派」だけどね。
0362132人目の素数さん
2005/09/29(木) 23:27:59対立した感想を持っているに過ぎず。どちらが
正しいとか、間違ってるとか、そういう話では
ないということ。分かるかな?
これに関する「意識調査」って、ないのかな?
0363132人目の素数さん
2005/09/29(木) 23:30:41>「普通に証明できてるものは『適当な』公理系で形式証明可能」
を言ったのはお前だろ?
>どちらを考えるにしても
も何も,そんなの考えてるのはお前だけ.
0364132人目の素数さん
2005/09/29(木) 23:33:45じゃあ、貴方は何が言いたかったの?感想でも、命題でも
いいから聞かせてよ、ね♪
俺は「できない派」だよ!ちゃんと、見てくれてるかな?
0365132人目の素数さん
2005/09/29(木) 23:35:14>因みに、俺は「できない派」だけどね。
ってあるよね。
0366132人目の素数さん
2005/09/29(木) 23:36:16>「普通に証明できてるものは『適当な』公理系で形式証明可能」
>いや、「できないものもある」
> → どちらを考えるにしても、ただの感想。正しい、間違って
>いるの問題ではない。
0367132人目の素数さん
2005/09/29(木) 23:41:22おめでとう!あなたの勝ちです。よかったね!
というわけでここからは本題に戻ってプルーフチェッカーの話をしましょう。
0368132人目の素数さん
2005/09/29(木) 23:43:55いや〜、嬉しいな。w
0369132人目の素数さん
2005/09/29(木) 23:45:240370132人目の素数さん
2005/09/29(木) 23:47:130371132人目の素数さん
2005/09/29(木) 23:50:23そうだったのか。。!
プログラミングに関してはHello Worldに毛が生えたような知識なもんで。。
0372132人目の素数さん
2005/09/29(木) 23:52:460373132人目の素数さん
2005/09/29(木) 23:56:20有用さ>>>厳密性
基礎論の豚どもは、死ね!
0374132人目の素数さん
2005/09/29(木) 23:56:52http://www.google.co.jp/search?hl=ja&q=Windows+%E4%B8%87%E8%A1%8C&btnG=Google+%E6%A4%9C%E7%B4%A2&lr=
0375132人目の素数さん
2005/09/29(木) 23:59:42基礎論屋は、居なくていいよwww
0376132人目の素数さん
2005/09/30(金) 00:00:360377132人目の素数さん
2005/09/30(金) 00:01:520378132人目の素数さん
2005/09/30(金) 00:04:05ハハハハハハ
0379132人目の素数さん
2005/09/30(金) 00:05:250380132人目の素数さん
2005/09/30(金) 00:06:010381132人目の素数さん
2005/09/30(金) 00:20:59>いや、「できないものもある」
> → どちらを考えるにしても、ただの感想。正しい、間違って
>いるの問題ではない。
どんな定理でも形式証明は可能なのだよ。いや、
どんな命題でも形式的証明は可能なのさ。なぜ
なら、その命題を公理として含む形式的体系を
考えればいいから
君はこんな簡単なことも知らなかったのかいw
形式証明は必ず出来るのさ!
0382132人目の素数さん
2005/09/30(金) 00:22:43出来ない、というのは「ただの間違い」だから。分かった?
0383132人目の素数さん
2005/09/30(金) 00:23:30君は基礎論の入門書でも読んだときに随分そこで引っ掛かったんですねえ
0384132人目の素数さん
2005/09/30(金) 00:25:18証明しなくてもいいのだ。すべての命題は証明できる
0385132人目の素数さん
2005/09/30(金) 00:28:20¬(1+1=2) :証明可能
すべては証明可能。だから、証明なんかしなくていいんだよ
0386132人目の素数さん
2005/09/30(金) 00:29:120387132人目の素数さん
2005/09/30(金) 00:41:23証明は無意味だ!
0388132人目の素数さん
2005/09/30(金) 00:42:01数学的証明=無意味
0389132人目の素数さん
2005/09/30(金) 01:11:22MIZ→Tex(pdfだったかな?)は、あるよ。
それを論文の一部として出してたりしてたからね。
0390132人目の素数さん
2005/09/30(金) 01:12:28どちらでも全く不安ではありません。
「適当な」というのに正確な意味がないけどねw
つーかさ、ある形式体系で証明可能であったとしても、その
形式体系が無矛盾か、どうかは結局、数学者の主観に永遠に
留まるしかない。もちろん、その妥当性を検証し続ける事は
可能だが、いつまで立っても完全に肯定的結論は得られない。
主観的信念が強まるだけだ。そのような事が無意味だ、とは
言わないけど
もっと言えば、当該の「形式的体系の価値」が主観的、相対
的なものに過ぎないから決着は永遠にありえない。あくまで
「一つの試み」だが「こんなもんで十分なんじゃないの」と
言う感想に留まるのみなのだ
リップサービスとして、「初めて」の形式的証明である、と
言うのは良いことだよ。これは政治的価値判断の問題だけど
0391132人目の素数さん
2005/09/30(金) 01:13:54pdfとtex、全然違うが???一体、何なの???
0392132人目の素数さん
2005/09/30(金) 01:16:39MIZを、英語で書かれた数学論文(pdf)に自動変換します。
優れものです。w
0393132人目の素数さん
2005/09/30(金) 01:16:420394132人目の素数さん
2005/09/30(金) 01:17:31優れものです。w
0395132人目の素数さん
2005/09/30(金) 01:18:31じゃあ、pdfは関係ないじゃんw
0396132人目の素数さん
2005/09/30(金) 01:19:59自分達がやってることも理解できてないみたいだね。
0397132人目の素数さん
2005/09/30(金) 01:26:13どうか知らんが)、証明問題の自習用とか、数学者が自分の証明の
チェックに使えて便利だと思うね。でも別にプルーフ・チェックが
通らなかったからと言って証明に穴があるとは思わない。穴がある
可能性があると思うだけだ
0398132人目の素数さん
2005/09/30(金) 01:28:31部分の証明には自信がある、という状態はなかなか気持ちが
いいと思うね。
0399132人目の素数さん
2005/09/30(金) 01:30:170400132人目の素数さん
2005/09/30(金) 01:32:090401132人目の素数さん
2005/09/30(金) 01:33:420402132人目の素数さん
2005/09/30(金) 01:37:04いや、俺が単純に覚えてないだけ。
MIZ→TeX→PDFだったのか、MIZ→PDFだったのか、、。
最終的に、PDFになってたのだけは覚えてる。
オレの研究と全く関係ないのに、俺もやらされたよMIZAR。
ゼンゼンわからんかったけどね。工学の人間なんでオレ。
中村さんは、確か理学博士だったような、、、。
0403132人目の素数さん
2005/09/30(金) 01:39:09見づらかったのだけは良く覚えてるわwww
0404132人目の素数さん
2005/09/30(金) 01:39:41聞きたいのは、それって「普通の証明」に変換されるの?
それとも証明図とかになって出てくるの?
「普通の証明」になって出てくるなら、俺は面白いと思う
0405132人目の素数さん
2005/09/30(金) 01:41:02普通の証明だったと思うよ。
多分Webのどっかに落ちてるから、探してみるよ。変換例。
0406132人目の素数さん
2005/09/30(金) 01:42:43「普通の証明→形式証明」に変換する以上に難しいと
思う。
0407132人目の素数さん
2005/09/30(金) 01:45:15ほんとに?と言っても、「普通の証明」というのが
実は主観でしかないから
でも、よろしく頼むよ。それをいろいろな数学者に
見せて、感想を聞いてみるのは面白い、と俺は思う
0408132人目の素数さん
2005/09/30(金) 01:46:10まずAIを作らなきゃ駄目なんじゃ
まだ、検索エンジンで無理矢理翻訳したみたいな
自然言語での証明を生成する方が楽かと
0409132人目の素数さん
2005/09/30(金) 01:46:53簡単な例と、
http://markun.cs.shinshu-u.ac.jp/mirror/mizar/JFM/Reqmnts/boole.html
の、BOOLEってリンクの先がMIZAR記述で、Contents (PDF format)が、自動生成されるPDF。
http://markun.cs.shinshu-u.ac.jp/mirror/mizar/JFM/mmlident.html
にこれまで証明された全てがあると思われ(自信なし)。
昔無理やりやらされた俺のファイルもあるかなwww.。
>>406
あー、オレ「普通の証明」の意味多分わかってないわ。↑が着たい違いだったらスマソ。
0410132人目の素数さん
2005/09/30(金) 01:48:06もし、そうならプルーフ・チェックも実用化も
そんなに絵空事でないような気もするね。
0411132人目の素数さん
2005/09/30(金) 01:56:02サンクス。
>BOOLEってリンクの先がMIZAR記述で、Contents (PDF format)
うん。普通の形式証明(普通の証明でなく)の記号の部分を、
普通の英単語に機械的に置き換えた感じがするね。ちょっと
見ただけだから確証はない。
0412132人目の素数さん
2005/09/30(金) 02:01:57ポイントになるところをイメージ喚起
的に説明するのは、非常に難しいよ。
俺はこれは得意じゃない。厳密にしこ
しこ証明を書くほうがルーチン的で、
体力を使うが気は楽。厳密といっても
形式的証明では、もちろんないけど。
0413132人目の素数さん
2005/09/30(金) 02:55:450414132人目の素数さん
2005/09/30(金) 03:58:250415132人目の素数さん
2005/09/30(金) 07:48:30>平地健吾だって小島定吉だって、
>オリジナリティの低い低レベルな結果だ、と
>内心考えてると思うよ
それ以前に、
「数学の話じゃないだろ」
と思ってるだろ。
そしてそれは正しい。
0416132人目の素数さん
2005/09/30(金) 07:54:44>証明の形式化のどの部分がそんなに難しいと考えてるのかな?
>少なくともZFCの公理から、必要な諸概念を定義して、
>完全に形式的に証明するのは、述語論理の基礎を
>理解している数学者には簡単なことだと思うがな
まず、数学者は述語論理もZFCも正確に理解してるわけではない
次に、理解していたとしても、自分たちが直観で扱ってきた概念を
完全に記号操作として書ききるのは実は箆棒に困難な作業である。
最後に、上記の「翻訳」の作業で、多くのミスが発生し形式化された
理論が、直観的概念に照らし合わせて妥当かどうかチェックする
必要がいたるところで発生する。
プログラムのデバッグをやったことがある人にとっては明らかなこと。
0417132人目の素数さん
2005/09/30(金) 08:05:03>別に「形式的証明」がなくても不安じゃありませんけど。
ごもっとも。
数学の証明はプログラム検証とは違う。
数学は読んだ人が理解できればそれでよい。
ギャップは読者にとって自明でないから問題になるのであって
多くの専門家が「自明」と判断すればそれはギャップでなくなる。
「玄人の誤解」とは、数学が実は数学者の頭の中の世界における
共同の了解事項であるにすぎないにもかかわらず、あたかも
自分たちとは全く独立なる真偽の根拠があると信じていること。
そしてそれが嘘であることを暴くのが形式的証明。
なぜなら、誰一人了解しない機械的検証を、数学者はまったく
信頼しないからである。
0418132人目の素数さん
2005/09/30(金) 08:11:25>とりあえず http://mizar.org/fm/ と20万行目に目を通したんだけど,
>ほとんど全てが 定式化のための定式化で冗長としか思えんかった.
主語をはっきり書こう。論理的であるということはそういうこと。
さて、あなた(もっと広く人間サマ)にとって冗長であるからといって
機械にとっても同じとは限らない。機械は記号処理しかできない石頭
であるということを忘れてはならない。
>知識蓄積する以外になんかこのあたり簡単にできんかな?
簡単にしたために、形式化自体を否定する結果になるかもしれん。
0419132人目の素数さん
2005/09/30(金) 08:29:030420132人目の素数さん
2005/09/30(金) 09:17:04>つーかさ、ある形式体系で証明可能であったとしても、その
>形式体系が無矛盾か、どうかは結局、数学者の主観に永遠に
>留まるしかない。
集合論の公理系に矛盾が発見されない限りそうだな。
だから表題のジョルダンの定理の証明も、元になってる公理
(集合論だろう?)に矛盾がないと証明されてないわけだから
客観的な意味で正しいかどうかはわからない。
結局、形式主義は自己矛盾で行き詰まることになってる。
形式主義の最大の問題は意味を無視していること。
定理の意味こそ重要なのにな。
0421132人目の素数さん
2005/09/30(金) 09:30:04当時は理解できるひとがほんど少なくてなあ
んでもんで後年追試されていったけんよ
ほなこの証明もなんだかんだでアルゴリズムになってよ
CGとかいろんなプログラムに応用されるようになったらな
ああこれこれってなるくらいになって認められるんべいよ
でかい目でみんれば技術投資なんだべよなキタコレ
0422132人目の素数さん
2005/09/30(金) 09:36:35>「玄人の誤解」とは、数学が実は数学者の頭の中の世界における
>共同の了解事項であるにすぎないにもかかわらず、あたかも
>自分たちとは全く独立なる真偽の根拠があると信じていること。
「共同の了解事項であるにすぎない」のすぎないに引っかかるな。
なぜそう言い切れる? つまり実在論が嘘だと何故言い切れる?
>そしてそれが嘘であることを暴くのが形式的証明。
>なぜなら、誰一人了解しない機械的検証を、数学者はまったく
>信頼しないからである。
この「なぜなら」がまったく分からない。
もっと詳しく説明してもらいたい。
0423132人目の素数さん
2005/09/30(金) 09:43:24>「普通に証明できてるものは『適当な』公理系で形式証明可能」
>いや、「できないものもある」
極論をいえば、公理や推論規則を適当に追加すれば
名目上「形式的証明」にはできる(w
ただし実際にはぎりぎりまで絞った公理と推論規則だけを
用いた形式的証明ができるかどうかを問題にしている。
「できると信じたいが、もしかしたらできないかもしれない。」
これが率直な気持ちだろう。
0424132人目の素数さん
2005/09/30(金) 09:45:16俺も人間が検証できるに越したことはないと思ってはいるがな。
0425132人目の素数さん
2005/09/30(金) 09:49:44嘘だとはいっていないよ。
ただ、本音はそうじゃないってこと。
いざというときに、自分の理解してないことは認めない。
それが本音。そもそも数学者は理解するために数学しているんで
自分が理解できない定理なんて数学者には不愉快なだけでしょ(w
0426132人目の素数さん
2005/09/30(金) 09:53:06ビル・サーストンは信用してないみたいだけど。
0427132人目の素数さん
2005/09/30(金) 09:53:07はあ?信用なんて出来ないよ。この場合はな。20万行の中身を
見ないことには。さらにはMizarとかいうソフトのコードも調べないことには。
0428132人目の素数さん
2005/09/30(金) 09:57:41しかし帰納法抜きのロビンソン算術では証明できない。
ロビンソン算術は弱いといわれるが、普通の自然数の計算は
ちゃんとやるから、直観的には証明できそうに思える。
しかし、実際には「想定外の反例」がある。
つまりロビンソン算術では自然数を十分に定義できていない。
形式化の穴はいたるところにある。
0429132人目の素数さん
2005/09/30(金) 10:01:57「証明不可能」だったらまだいいかな。
でも、NBG集合論からは「否定が証明可能」で、
多くの数学者にとって正しいと思われてる命題って具体的にある?
0430132人目の素数さん
2005/09/30(金) 10:02:03交換法則を証明すると、直観との乖離に気づく。
加法の形式的な定義はそもそも不自由である。
上記の証明は、パズル的な面白さは感じられるが
それは当たり前のことを面倒な状況で示すだけのことで
これで正しさが保証されるという感じはしない。
0431132人目の素数さん
2005/09/30(金) 10:03:14>いざというときに、自分の理解してないことは認めない。
誰のことを言ってる?一からげにしなさんな。
それに文意もはっきりしない。自分の理解してなことは、認めるも
認めないもノーコメントが普通の態度だろ。
>そもそも数学者は理解するために数学しているんで
だから、一からげにしなさんな。
0432132人目の素数さん
2005/09/30(金) 10:05:53>NBG集合論からは「否定が証明可能」で、
>多くの数学者にとって正しいと思われてる
>命題って具体的にある?
なぜZFCでなくNBG?
もしかして、クラスを考えないと
「証明されてるが受け入れられない定理」
があるのかな?(例えば集合の全体が存在しない、とか)
0433132人目の素数さん
2005/09/30(金) 10:09:03>一からげにしなさんな。
十巴一からげとはいうが、一からげとはいわない。
>自分の理解してなことは、認めるも認めないも
>ノーコメントが普通の態度だろ。
それが「認めない」ということ。
0434132人目の素数さん
2005/09/30(金) 10:10:01圏論とかはクラスで考える方が自然じゃない?
ZFCで出来なくはないだろうけど。
0435132人目の素数さん
2005/09/30(金) 10:13:36>圏論とかはクラスで考える方が自然じゃない?
じゃ、集合の圏では成り立たないが
別の圏で成り立つ命題があるかどうか
探して見ればいいのでは?
あってもおかしくはない希ガス。
0436424
2005/09/30(金) 10:16:55>>機械的検証を信用しない数学者なんてもういないだろ。
>
>ビル・サーストンは信用してないみたいだけど。
勝手なことを言わないように。サーストンはコンピューター大好き人間だし、
機械を使った証明検証に対する彼の好意的な意見は
ttp://arxiv.org/abs/math.HO/9404236
に述べられているから読んでおくように。
0437132人目の素数さん
2005/09/30(金) 10:18:11>十巴一からげとはいうが、一からげとはいわない。
口語では一からげで十分通じるし、そう言う言い方もありなの。
そちらの地方では言わないかもしれないけどな。
>それが「認めない」ということ。
ノーコメントがなんで認めないになるんだよ。
分からないってだけだろ。
0438132人目の素数さん
2005/09/30(金) 10:21:40それは形式化大好きということとは違う。
>機械を使った証明検証に対する彼の好意的な意見は
>http://arxiv.org/abs/math.HO/9404236
>に述べられているから読んでおくように。
君こそちゃんと読んだほうがいい。
彼がフォーマリズムを信頼してないことが分かる。
0439132人目の素数さん
2005/09/30(金) 10:24:06口語では「一緒」というよな。
一からげなんてちょっとわざとらしくて不自然
そのくせ省略してるところがハンパ。
>ノーコメントがなんで認めないになるんだよ。
>分からないってだけだろ。
分からないなら認めないってこと。
0440132人目の素数さん
2005/09/30(金) 10:25:28幾つかの分野にまたがる研究していたら、使っている定理が
正しいかどうかなんて個人ではチェックしきれないからね。
安全のために、その分野のエキスパートに確認する程度だよ。
だから自動プルーフ・チェッカーがあって正しい定理を認定して
くれるってんなら、そりゃ便利だわな。
0441132人目の素数さん
2005/09/30(金) 10:31:28それは他人の理解を信頼してるからであって、
形式的証明への信頼とは異なる話だな。
>自動プルーフ・チェッカーがあって正しい定理を認定してくれる
>ってんなら、そりゃ便利だわな。
チェッカーが便利なのは、正しさを認定するからじゃないよ。
どこにバグがあるかを判定してくれるから。
証明がチェックを通ったから正しいとはいえない。
形式化自体が間違っている可能性は多々ある。
0442132人目の素数さん
2005/09/30(金) 10:35:40>一からげなんてちょっとわざとらしくて不自然
全然不自然ではないよ、だけどスレと関係ないからな。
>分からないなら認めないってこと。
違うだろ。面倒だから、仮にそうだとしてそれがいけないのか?
つまり、分からないことに対しては、ノーコメントじゃいけないのか?
0443424
2005/09/30(金) 10:38:26サーストンは2ページの八行目辺りから、四色問題の機械証明が起こした騒動に触れて、
I interpret the controversy as having little to do with
doubt people had
as to the veracity of the theorem or
the correctness of the proof.
Rather, it reflected
a continuing desire for *human understanding* of
a proof, in addition to knowledge that the theorem is true.
と言ってるね。彼が機械検証の正しさを疑っていないことは明らかだな。
それに君は、>>426では
>>機械的検証を信用しない数学者なんてもういないだろ。
>
>ビル・サーストンは信用してないみたいだけど。
と言ってたのに>>438では
>彼がフォーマリズムを信頼してないことが分かる。
とビミョーに意見をずらしたね。
0444132人目の素数さん
2005/09/30(金) 10:40:50>>一からげなんてちょっとわざとらしくて不自然
>全然不自然ではないよ
君が、一緒のことを一からげとかいう実に辺鄙な田舎で
子供時代をすごしたという「特殊な人」なら仕方がない。
別に何県何郡何村大字何某字何某なんて聞かないから
安心したまえ。書いたらどこの誰だか分かっちゃうだろ?(w
>面倒だから、仮にそうだとしてそれがいけないのか?
>つまり、分からないことに対しては、ノーコメントじゃいけないのか?
だから、君の「認める」という言葉の理解が間違ってる。
0445132人目の素数さん
2005/09/30(金) 10:45:01>ビミョーに意見をずらしたね。
いや、私はもともと*human understanding*が重要だといってるんで
それ抜きに形式的だから正しいということにはならないといってるわけ。
サーストンの文章を正しく読めば、彼が「機械が検証すれば、
人間の理解ぬきに正しい」とはいっていないことがわかる。
0446132人目の素数さん
2005/09/30(金) 10:45:58おれは生まれも育ちも東京だよ、環状線の中。
ごちゃごちゃ言わなくていいから、これに答えてくれ。
>つまり、分からないことに対しては、ノーコメントじゃいけないのか?
0447424
2005/09/30(金) 10:48:33>>426では機械検証を信用してない数学者の例として
サーストンを挙げたんじゃなかったのか?
彼はどこでそんなことを言ってる?
0448132人目の素数さん
2005/09/30(金) 10:49:45じゃ、両親が田舎の人か。最近は珍しくない。
悪いがおれは祖父母の代から東京市内。
ごちゃごちゃ弁解するな。お前の日本語が間違ってるんだ。直せ。
0449132人目の素数さん
2005/09/30(金) 10:54:14>彼はどこでそんなことを言ってる?
サーストンに対するインタビュー記事で
彼が一時期直観主義に傾倒していて、
形式的証明がそれゆえに正しいという
考え方に対して疑念を抱いているという
文章を読んだ。
0450132人目の素数さん
2005/09/30(金) 10:55:17>十巴一からげとはいうが、一からげとはいわない。
何このどうでもいい突っ込み。ここ本当に数学板?
0451424
2005/09/30(金) 10:59:53はいはい。ソースはないわけね。
それに、二十年前に機械検証を信用しなかった数学者ならいくらでもいるしな。
>426 名前:132人目の素数さん[] 投稿日:2005/09/30(金) 09:53:06
>>機械的検証を信用しない数学者なんてもういないだろ。
>
>ビル・サーストンは信用してないみたいだけど。
0452132人目の素数さん
2005/09/30(金) 11:03:38>はいはい。ソースはないわけね。
残念だが、君の期待ははずれだ。
数学人群像―プロフィルとインタビュー
D.J. アルバース (編集), G.L. アレクサンダーソン (編集), 一松 信 (翻訳)
>それに、二十年前に機械検証を信用しなかった
>数学者ならいくらでもいるしな。
機械検証をしたことがある人なら、今でも
形式化の誤りが深刻だというのは常識だがな。
0453424
2005/09/30(金) 11:09:43ちゃんと該当部分を引用してくれないかな。
サーストンは先に挙げた文献の中(9ページ中頃)で、
The standard of correctness and completeness
necessary to get a computer program to work at all
is a couple of orders of magnitude higher than the
mathematical community's standard of valid proofs.
とも言ってる。機械で検証する方が人間がやるより厳密だってわけだ。
まあ、その後に長いプログラムにつきもののバグを心配しはいるが。
0454132人目の素数さん
2005/09/30(金) 11:15:03今残念ながら手元にない。図書館ででも探してくれ。
>機械で検証する方が人間がやるより厳密だってわけだ。
>まあ、その後に長いプログラムにつきもののバグを心配しはいるが。
プルーフチェッカーのバグの可能性は確かにあるが、
それはまだなんとかなるほうだ。問題は、形式化する
理論自体がどうしたって長大になるから、そこに
バグが混入する可能性が避けられないってことだ。
それは前提だから、チェッカでは検証できない。
0455132人目の素数さん
2005/09/30(金) 11:27:49設定した公理系は無矛盾であったが、実は考えていたものとは違っていた。
しかし、定理の形式的証明ができたので、万事OKと考えた。
その後、実は当初の公理系では強すぎて、排除したいものまで
証明できてしまうことがわかったので、公理系を変えたところ
証明ができなくなった。実際後で反例がみつかった。
0456132人目の素数さん
2005/09/30(金) 11:33:22AIの研究者以外では数学の出来ないやつだけだろ。
自分の代わりに機械にやってもらおうと。そんなの何の意味があるか
知らないけど。宿題やってもらうとかかw
0457132人目の素数さん
2005/09/30(金) 11:50:45>自動証明に期待をもつってのは・・・数学の出来ないやつだけだろ。
>自分の代わりに機械にやってもらおうと。
>そんなの何の意味があるか知らないけど。
全然ないとはいわない。証明を読んで理解したなら
それはそれで当人には意味がある。
ただ、不勉強な奴はきっと証明なんて読まないだろうけど。
0458132人目の素数さん
2005/09/30(金) 12:29:06>設定した公理系は無矛盾であったが、
無矛盾の公理系からでる定理なんてつまらないものか、
マイナーな分野、例えば組み合わせ論とかの定理じゃないの。
重要な定理って大抵、実数体や選択公理などを使うでしょ。
0459132人目の素数さん
2005/09/30(金) 12:30:38小島はサーストンを恐らく敬愛しているだろうから、
どう思うだろうね。
結局、「意識調査」の問題だけどさ
0460132人目の素数さん
2005/09/30(金) 12:33:33価値の低いどうでもいい結果なのに
一般メディアに大きく報道されて
誤解が誤解を生んでめちゃくちゃになる
しょせん大衆は馬鹿だから
0461132人目の素数さん
2005/09/30(金) 12:35:08>自動証明に期待をもつってのは・・・数学の出来ないやつだけだろ。
そんなことはない。頭の悪い奴に自分の証明を見せても
分からないときに、「貴方は分からないのかもしれない
けど、このプルーフ・チェッカーでは通ってるよ」、と
言える。(主張の正しさについての)肯定的な査読者が
増えたようなもの
0462132人目の素数さん
2005/09/30(金) 12:36:20>一般メディアに大きく報道されて
じゃあ、価値のある結果をアピールしようぜ!
0463132人目の素数さん
2005/09/30(金) 12:37:39止めましょう。ここは2chだからいい
けど
0464132人目の素数さん
2005/09/30(金) 12:38:32プルーフ・チェッカーと自動証明はちがうんだけど。
0465132人目の素数さん
2005/09/30(金) 12:43:06これなんか、どう思うの?
>受賞者 西田孝明
>受賞理由 微分方程式の解の大域構造の数学解析に,計算機援用証明の方法を
>本質的かつ本格的に用いたところにある.
>自明解からの定常分岐やホップ分岐の存在,臨界パラメータでの自明解の不安
>定化等について計算機支援による数学的証明を次々と成し遂げた.
>同氏の業績は解析学賞にふさわしい.
http://www.math.kobe-u.ac.jp/a-prize/jusho3-3.html
0466132人目の素数さん
2005/09/30(金) 12:47:30俺の言うプルーフ・チェックは「実用的なそれ」だからな…
こう言えばいいか、「自明な」命題の自動証明のこと。
「自動証明」って言葉は紛らわしいな
逆側の極が「まだ予想もされていない価値のある定理の
自動発見(+証明)」か
0467132人目の素数さん
2005/09/30(金) 12:53:18「まだ予想もされていない価値の
ある定理の自動発見」ができれば
意味あるね
>>465 に計算機を使ってる証明が
あるけど無意味だとは感じないな。
自動証明ではないけど。部分的に
何かを計算機で証明しているんだ
けどね
0468132人目の素数さん
2005/09/30(金) 13:02:11>証明されてないわけだから客観的な意味で正しいか
>どうかはわからない。
いや、違う。「その公理系では全ての命題が客観的に
正しい」だけだ。形式化しなければ、主観に過ぎない。
但し、多くの数学者は客観性に価値をそれほど置いて
いないと思うね。だから、主観でもいいじゃない、と
言うこと
ある公理系が無矛盾だろうというのも主観だし、その
公理系に意味があるというのも主観だから。ただし、
その公理系からかくかくしかじかの命題が、形式的に
証明できるのは客観だ。それに、どのくらいの価値が
あるか、と思うのかは、主観だね
0469132人目の素数さん
2005/09/30(金) 13:05:06>無矛盾の公理系からでる定理なんてつまらないものか、
>マイナーな分野、例えば組み合わせ論とかの定理じゃないの。
をひをひ、無矛盾でない公理系は何でも証明可能だから無意味だぞ(w
>重要な定理って大抵、実数体や選択公理などを使うでしょ。
あのなぁ、無矛盾性が証明できない=矛盾してる、ってことじゃないぞ(w
0470132人目の素数さん
2005/09/30(金) 13:07:51いっとくけど、「形式化すれば客観的」とかいうのも主観だぞ。
どこまでいっても主観を排除できない。できると思うのは妄想だ。
0471132人目の素数さん
2005/09/30(金) 13:13:58それじゃあ、客観はないことになるよ。とすれば、
すべてが主観なのだから、「主観と客観」という
区別自体が無効化するが…
0472132人目の素数さん
2005/09/30(金) 13:15:39>それじゃあ、客観はないことになるよ。
ないと困るのか?
0473132人目の素数さん
2005/09/30(金) 13:16:44ZFCの無矛盾性=主観
かくかくしかじかの形式的命題がZFCで証明可能=客観
という区別ね。こういう区別をする、というのはあくまで
俺の意見だけど
0474132人目の素数さん
2005/09/30(金) 13:16:48>すべてが主観なのだから、
>「主観と客観」という区別自体が
>無効化するが…
効果があると思ってたのか?
0475132人目の素数さん
2005/09/30(金) 13:18:20要するに
有限=客観
無限=主観
ってことかな?(w
0476132人目の素数さん
2005/09/30(金) 13:21:24全てが主観だったら、「それは主観である」という
主張には何の意味もなくなるよ
わざわざ矛盾した体系を使ってたら、全てが正しい
命題なんだから、「この命題は正しい」というのが
無意味になるようなもの
0477132人目の素数さん
2005/09/30(金) 13:23:07> 全てが主観だったら、
>「それは主観である」という主張には
>何の意味もなくなるよ
意味があると思ってたのか?
0478132人目の素数さん
2005/09/30(金) 13:25:16「自分が間違ってるかもしれない」
という不安を解消するための阿片
0479132人目の素数さん
2005/09/30(金) 13:27:28「自分が間違ってるかもしれない」
という不安を分割して無害な程度に
小さくするためのもの
0480132人目の素数さん
2005/09/30(金) 13:29:58だから、それが君の言葉使いにおける客観性だとしたら、
「君の言う客観性(=自分は間違ってるかもしれないと
いう不安を解消するための阿片)」が世の中にあるじゃ
ない
要は言葉使いの違いだよ。
0481132人目の素数さん
2005/09/30(金) 13:30:57無矛盾の公理系っていうのは、引用元の言葉をそのまま使ったもの。
つまり、無矛盾と分かっている公理系という意味。
少しはスレを追えよ。
>あのなぁ、無矛盾性が証明できない=矛盾してる、ってことじゃないぞ(w
俺はそんなこと言ってないよ。勝手に見当違いな解釈すんじゃない。
0482132人目の素数さん
2005/09/30(金) 13:31:05阿片中毒患者の開き直りか?(w
0483132人目の素数さん
2005/09/30(金) 13:32:19無矛盾な公理系は無矛盾と証明されている公理系という意味じゃない。
少しは日本語をマジメに勉強しろ。
0484132人目の素数さん
2005/09/30(金) 13:32:42という感想を持った奴はいないのか?
0485132人目の素数さん
2005/09/30(金) 13:33:13君は、君なりに客観性という言葉を使っていて、
そういう物(=客観性)は現に存在するわけだ。
0486132人目の素数さん
2005/09/30(金) 13:34:14普通の数学なら100行もいらない
0487132人目の素数さん
2005/09/30(金) 13:35:08君は、ユニコーンという言葉があるから
ユニコーンが存在するんだというのかい?
それとも、阿片の吸いすぎで幻覚を見たか?(w
0488132人目の素数さん
2005/09/30(金) 13:38:01俺は違う意味で、客観性という言葉を使っているだけだ。
いずれにしても、区別をしている以上はあるんだよ。
どういう意味なのかは、完全には明確にはならないけど。
「この料理は旨い」と言えば、旨いものと不味いものが
ある。但し、当然ながら「完全に正確な意味」は分から
ない。
0489132人目の素数さん
2005/09/30(金) 13:38:20一ページ40行として、5000ページか。
数学書何冊分に当たるか考えたくもない。
0490132人目の素数さん
2005/09/30(金) 13:39:07その場合でも、幻覚の中にあると思うが…
0491132人目の素数さん
2005/09/30(金) 13:40:19無責任な臆病者の自己弁護は醜いものだ。
0492132人目の素数さん
2005/09/30(金) 13:40:55そういう証明を一般的に可能と考えられている方法で行間を埋めようとすると、
20 万行ではとてもきかないと思うのだが。
0493132人目の素数さん
2005/09/30(金) 13:42:03その意味での「在る」は幻覚を見る君の主観
ほら客観が消滅しただろ。
♪
これも主観
あれも主観
たぶん主観
きっと主観
0494132人目の素数さん
2005/09/30(金) 13:42:52不安を解消するための阿片」があるでしょ。それとも、ないのかい?
(少なくとも)俺の中で「旨い」「不味い」の区別があるようにね。
0495132人目の素数さん
2005/09/30(金) 13:44:33自分の中の「旨い」「不味い」の区別が主観であるように、
自分の中の「主観」「客観」の区別は主観でしかない。
0496132人目の素数さん
2005/09/30(金) 13:45:17だから、言い方を変えれば消滅するよね。言ってることが
違うんだからさ。それだけのことだ。君は勝手に言い方を
変えて「人の感想」を否定し、「自分の感想」を押し付け
ようとしてるだけだ。
0497132人目の素数さん
2005/09/30(金) 13:45:56最終的には自分自身の信念が根拠。
死ねない者はそもそも生きていない。
0498132人目の素数さん
2005/09/30(金) 13:47:16>自分の中の「主観」「客観」の区別は主観でしかない。
もちろん、そうだ。だから、主観的区別として、主観と
客観があるのよね。
0499132人目の素数さん
2005/09/30(金) 13:47:50いや、目を開くと消滅するのだ。
君は目をつぶって自分の妄想を語り
それが妄想に過ぎないという忠告に
耳をふさいでいるだけだ。
0500132人目の素数さん
2005/09/30(金) 13:49:40どうやら、君の方が妄想的になってるねw
0501132人目の素数さん
2005/09/30(金) 13:50:24>主観的区別として、主観と客観があるのよね。
それは君が間違っているから。
主観的だから間違いがないということにはならない。
0502132人目の素数さん
2005/09/30(金) 13:50:40数学板随一のスピードだ
0503132人目の素数さん
2005/09/30(金) 13:51:21>どうやら、君の方が妄想的になってるねw
いや、それは妄想だ(w
0504132人目の素数さん
2005/09/30(金) 13:51:39書いてるのは2人か3人です
0505132人目の素数さん
2005/09/30(金) 13:53:09>主観的だから間違いがないということにはならない。
じゃ、「間違ってる」という状態が客観的にあるんだ。
0506132人目の素数さん
2005/09/30(金) 13:53:48じゃあ、二人だ。
なぜなら、議論してる二人と独立の人物なら
自分が三人目だとわかるから。
0507132人目の素数さん
2005/09/30(金) 13:53:590508132人目の素数さん
2005/09/30(金) 13:55:09>>主観的だから間違いがないということにはならない。
>じゃ、「間違ってる」という状態が客観的にあるんだ。
それが間違いだ。主観的であっても矛盾からは免れない。
0509132人目の素数さん
2005/09/30(金) 13:56:13>結局、言葉使いの違いだろ。それだけ
ネットでは、私が間違ってましたという言葉は
このように言い直される(w
0510132人目の素数さん
2005/09/30(金) 13:57:42ただ、「単に感想レベルの話」でも、他人との対立や矛盾を
許容したくないだけでは?
0511132人目の素数さん
2005/09/30(金) 13:58:41>東京市内
東京市内東京市内東京市内東京市内東京市内東京市内東京市内東京市内東京市内
東京市内東京市内東京市内東京市内東京市内東京市内東京市内東京市内東京市内
東京市内東京市内東京市内東京市内東京市内東京市内東京市内東京市内東京市内
東京市内東京市内東京市内東京市内東京市内東京市内東京市内東京市内東京市内
東京市内東京市内東京市内東京市内東京市内東京市内東京市内東京市内東京市内
東京市内東京市内東京市内東京市内東京市内東京市内東京市内東京市内東京市内
0512132人目の素数さん
2005/09/30(金) 13:58:45>「完全に正確な意味」
自分とは独立に「正しい意味」があると思うのは
単に自分の存在を忘れたからだろう。
0513132人目の素数さん
2005/09/30(金) 14:00:06だけど、この言葉には意味が含まれている
0514132人目の素数さん
2005/09/30(金) 14:00:34別に間違ってない。戦前は東京市だ。
しかも35区の頃ではなく15区の頃からだ。
0515132人目の素数さん
2005/09/30(金) 14:01:59状況による。
旨いと思って言ったならそれは正しいが
お世辞で嘘をついたならそれは間違いだ。
もっとも、世の中は正しければよいというものではない(w
0516132人目の素数さん
2005/09/30(金) 14:04:24意味を否定した覚えはない。
自分とは独立だというのが間違ってるといったまでだ。
0517132人目の素数さん
2005/09/30(金) 14:09:03>お世辞で嘘をついたならそれは間違いだ。
じゃあ、君はそういう人の発言を「間違いだ」と
表現するんだね。
結局、ここに戻る気がするねえ。
>ただ、「単に感想レベルの話」でも、他人との対立や矛盾を
>許容したくないだけでは?
0518132人目の素数さん
2005/09/30(金) 14:12:19>君はそういう人の発言を「間違いだ」と表現するんだね。
口にだすとは限らないな。
しかし、今ここで君にお世辞をいうことで
私や君が何らかの利益を得るとは考えない。
>結局、ここに戻る気がするねえ。
戻りたがってるのは君だろう。
0519132人目の素数さん
2005/09/30(金) 14:13:39「この料理は旨い」って感想は自分と独立ではない、ってのは
普通のことだろ?どうして、そんなこと盛んに言うのかなあ。
0520132人目の素数さん
2005/09/30(金) 14:14:21「単に感想を述べただけ」(ここでレベルというのはおかしい)
といって、他者との対立や自己の発言の矛盾を避けるのは、
君自身が卑怯だからだろう。
0521132人目の素数さん
2005/09/30(金) 14:14:36もちろん、そうだが?
0522132人目の素数さん
2005/09/30(金) 14:15:43>ってのは普通のことだろ?
それなら「「完全に正確な意味」は知らない」という言い方はおかしい。
まさに君自身が旨いと感じたときが「完全に正確な意味」だからだ。
0523132人目の素数さん
2005/09/30(金) 14:18:25文字で表したものが、本来の正しい意味だと言い張るところ。
0524132人目の素数さん
2005/09/30(金) 14:18:26やっぱり、そうみたいだね。君はそれを卑怯と表現するのか。ふ〜ん
A:俺は不味いと思う。
B:いや、俺は俺は旨いと思うけど。
これで、終わって別の話題に移るのもよし。
「どうして〜?」と互いの感想を話題にし
続けるのもよし。
0525132人目の素数さん
2005/09/30(金) 14:19:310526132人目の素数さん
2005/09/30(金) 14:21:34やっぱり君は分かっていないな
私がいってるのは例えば
TV番組の「食わず嫌い」のコーナー
のような状況。
君は自分がいってることの矛盾を認めていないから
間違っているといっているのだよ。
0527132人目の素数さん
2005/09/30(金) 14:22:48まあ、そうだなw
0528132人目の素数さん
2005/09/30(金) 14:24:17>>互いの感想を押し付け合うとこのスレみたいになるのか......
>まあ、そうだなw
二人とも馬鹿だなw
0529132人目の素数さん
2005/09/30(金) 14:25:50>無矛盾な公理系は無矛盾と証明されている公理系という意味じゃない。
文脈からそういう意味で使ってるんだよ。
そう解釈しないと、俺の言ったことの意味が通らないだろ。
0530132人目の素数さん
2005/09/30(金) 14:27:35>文脈からそういう意味で使ってるんだよ。
勝手にそう思い込んだだけだろ。
>そう解釈しないと、俺の言ったことの意味が通らないだろ。
君が馬鹿なだけだ。自業自得だ。
0531132人目の素数さん
2005/09/30(金) 14:29:53A:お前は間違っている!
B:感想なんだから、間違ってるも何もないでしょ。
それに自分は素直に感想を述べてるつもりだし。
A:それでも、お前は間違っている!
B:他人の感想ぐらいは、認めたら?
の繰り返しですw
0532132人目の素数さん
2005/09/30(金) 14:31:27許容したくないだけでは?
0533132人目の素数さん
2005/09/30(金) 14:33:31なんだ、やっぱりあちこちの基礎論系のスレでいつも同じこと書いてる人か
これが言いたいがために、話を無理矢理引っ張って誘導するんだよね
はいはい、啓蒙活動おつかれさんです
0534132人目の素数さん
2005/09/30(金) 14:35:50そっか、その感想を皆に披露したかったんだね
披露できて、良かったね
0535132人目の素数さん
2005/09/30(金) 14:53:51勘違いしたお前が悪い。文意を考えれば勘違いするはずないんだよ、普通はな。
0536132人目の素数さん
2005/09/30(金) 14:59:51これなんか、どう思うの?
>受賞者 西田孝明
>受賞理由 微分方程式の解の大域構造の数学解析に,計算機援用証明の方法を
>本質的かつ本格的に用いたところにある.
>自明解からの定常分岐やホップ分岐の存在,臨界パラメータでの自明解の不安
>定化等について計算機支援による数学的証明を次々と成し遂げた.
>同氏の業績は解析学賞にふさわしい.
http://www.math.kobe-u.ac.jp/a-prize/jusho3-3.html
0537132人目の素数さん
2005/09/30(金) 15:06:08これほどまでに主観的で曖昧な表現が飛び交うのか。
それと他人に意見を伝える気があるのなら、
レス番号でもいいので、せめて名前欄くらい埋めてから投稿して欲しい。
傍観者としても読む気が起きない。
0538132人目の素数さん
2005/09/30(金) 15:13:03>これほどまでに主観的で曖昧な表現が飛び交うのか。
ここで行われてたのは「自分の価値観の表明」だから、
それは当然だと思うよ
0539132人目の素数さん
2005/09/30(金) 15:26:38>>534のようなレスを返すだけの
無意味なキャラに成り果てました
0540132人目の素数さん
2005/09/30(金) 15:47:320541132人目の素数さん
2005/09/30(金) 16:13:55まあ、いいんじゃないかな。さすがに、他人から自分が
『人の感想を否定して自分の感想を押し付ける人』だと
見られていることは、分かったんじゃないの。
自分の感想を言ったり、他人の感想を聞いたりするのは、
よくあることだけどね。
0542132人目の素数さん
2005/09/30(金) 16:16:02どっかに「意識調査」はないのかなあ?
0543132人目の素数さん
2005/09/30(金) 17:10:23それを自分のナイーブな感覚とまぜくって
偉そうにしゃべって、つっこまれるとやれ
感想だ、オレの言葉だと馬鹿丸出しなこと
いって結局自爆するいつもの馬鹿がいるね。
いい加減、もうその芸は見飽きたよ。
ちっとは新しいこと学んで違うネタみせろ
0544132人目の素数さん
2005/09/30(金) 17:13:05>これほどまでに主観的で曖昧な表現が飛び交うのか。
そもそも形式化のプロセスは客観的でもなんでもないからさ。
そのことに気づかない素人が勝手に自分の主観的な「客観性」
をわめきちらしてしかもそれがいかに主観的で身勝手なものか
絶対に認めようとしないからみっともないことになる。
ちなみに、曖昧とかいう前に無意味だね。無意味。
0545132人目の素数さん
2005/09/30(金) 17:16:13>レス番号でもいいので、せめて名前欄くらい
>埋めてから投稿して欲しい。
ん?漏れは誰がいってるかトレースできたよ。
書いてること読めばわかるじゃん。
>傍観者としても読む気が起きない。
自分の意見ももてない傍観者は読んではいかんな。
馬鹿には無理なんだよ。考えない君のような馬鹿にはね。
0546132人目の素数さん
2005/09/30(金) 17:22:17二人いるね。
・必ず基礎論という言葉を用いて、実に陳腐な
形式的=客観的という主張を「基礎論の初歩」
とほざくアホ
・ロジックという言葉を用いて、上記のような
陳腐な主張に必ず突っ込みを入れたがる、
玄人ぶったウザイ奴
で、だいたい前者の一見もっともらしい主張が
後者の狡猾極まりないレトリックに押されて
耐えられなくなった前者がブチ切れて終わる
といういつものパターン。もう何度みたか。
0547132人目の素数さん
2005/09/30(金) 17:41:11おもしろくないとか ためにならないとか 価値観がどうのこうのいうやつがそう
数学やってるやつはただ本を読むのでも演習を自分でやって解く能動的な仕事を伴う
だから考え方が実践的で他人の発言をよいか悪いかでは見ない
単純に正しいか間違っているかで見るし そこにはすごくシビアだ
哲厨は哲学書を自分の好き勝手に読むだけだから好き嫌いで批評する癖がついている
そして大学でまともにやってるやつらじゃないから論文を書く手法も知らない
ただ自分の視点からあれこれ文句をつけるだけ
数学とはその点が相容れない
数学は演習なしでは絶対に身につかねえ
初等数学でも真面目にやってるやつのほうが哲厨よりはるかに話せる
価値観なんてどうでもいいんだよ ぼけが
高度な数学的証明やってのけたやつだけがかっこいい
そいつの哲学など知ったことかってのが本来の数学者のスタンスだろ
哲厨は藤原きどりかよw
0548132人目の素数さん
2005/09/30(金) 17:52:49好き嫌いは、哲学ですらないんだが(w
で、
> 単純に正しいか間違っているかで見る
問題は、何をもって正しいというか、だ。
それを意識したくない人は哲学が嫌い。
哲学とは自己批判なんだよ。
0549132人目の素数さん
2005/09/30(金) 17:53:440550132人目の素数さん
2005/09/30(金) 17:54:450551132人目の素数さん
2005/09/30(金) 17:57:020552132人目の素数さん
2005/09/30(金) 18:03:40javaとかでは無理?
0553132人目の素数さん
2005/09/30(金) 18:09:10Javaでも出来るけど、プログラミングと計算時間含めて数万年かかると思う。
0554132人目の素数さん
2005/09/30(金) 18:11:45今後はプルチェキってよぼうぜ
0555132人目の素数さん
2005/09/30(金) 18:14:53なんか微妙。。
でも確かに略したいかも。アイディアはいい。
0556132人目の素数さん
2005/09/30(金) 18:31:26数学って価値観だろ。美意識に近いものが重要。
このあたりプロなら言うのもヤボなくらい先刻承知のこと。
0557132人目の素数さん
2005/09/30(金) 18:48:31Mizarってのは「IBM-PC上で動作する」とされているぞ。
ソースコードが公開されているかは知らんが、スパコン云々というものではないようだ。
0558132人目の素数さん
2005/09/30(金) 19:28:08正しくてもヘボいのは全然ダメ
だから主観が重要
因みに形式化のプロセスが主観的なのは当たり前。その後が客観的。
多くの数学者にとって前者の方が、重要なのも当たり前
0559558
2005/09/30(金) 19:31:100561132人目の素数さん
2005/09/30(金) 19:38:25形式体系=客観
形式体系に関する解釈=主観
0562132人目の素数さん
2005/09/30(金) 19:41:22できない奴が一名、紛れ込んでいるみたい
0563132人目の素数さん
2005/09/30(金) 20:05:20形式体系→客観
形式体系に対する解釈→主観
実在主義
数学的対象→客観
数学的対象に対する解釈→主観
0564132人目の素数さん
2005/09/30(金) 20:10:450565132人目の素数さん
2005/09/30(金) 20:15:48イデオロギー闘争に他ならない。という訳でこの闘争にはあまり意味がない。
0566132人目の素数さん
2005/09/30(金) 20:45:12ルネ・トムや佐藤幹夫の論文に書いてあることをきちんと証明した
というので立派な論文になるわけだからね。
岡潔の論文の中身を定式化するためには大理論が必要になった。
意味合いがちがうことだけど、
有限単純群の分類が完成したという宣言が出たが
細かいギャップがたくさんあるそうだ。
0567132人目の素数さん
2005/09/30(金) 20:51:270568132人目の素数さん
2005/09/30(金) 22:15:52気違い以外は、両方の価値を認めている。その上で後者に、より価値を置く数学者が多い
それだけのことだ
0569132人目の素数さん
2005/09/30(金) 22:18:47形式的証明→形式体系→客観
実在主義
証明→数学的対象に対する解釈→主観
0570132人目の素数さん
2005/09/30(金) 23:19:35形式的証明 ⊂ 形式体系
実在主義
証明 ⊂ 数学的対象に対する解釈
0571132人目の素数さん
2005/10/01(土) 00:06:500572132人目の素数さん
2005/10/01(土) 00:21:110573132人目の素数さん
2005/10/01(土) 00:46:25形式体系→客体
その解釈←主体
実在主義
数学対象→客体
その解釈←主体
0574132人目の素数さん
2005/10/01(土) 00:47:430575132人目の素数さん
2005/10/01(土) 00:57:06だから高度な数学は理解できない
0576132人目の素数さん
2005/10/01(土) 07:35:51適当な作業ディレクトリにjordan.miz, jordan.absをコピーして
名前の衝突を避けるためにjordan_test.miz, jordan_test.absにリネームしたのち
Cygwinで以下のように実行。
work$ ls
jordan_test.abs* jordan_test.miz*
work$ ../accom.exe jordan_test.miz
Accommodator, Mizar Ver. 7.5.01 (Win32/FPC)
Copyright (c) 1990,2005 Association of Mizar Users
Processing: jordan_test.miz
-Parsing-Vocabularies-Constructors-Registrations-Notations
-Definitions-Theorems-Schemes
work$ ../verifier.exe jordan_test.miz
Verifier, Mizar Ver. 7.5.01 (Win32/FPC)
Copyright (c) 1990,2005 Association of Mizar Users
Processing: jordan_test.miz
Parser [6801 *317] 0:02
Analyzer [6801 *339] 0:10
Checker [6801 *347] 0:23
Time of mizaring: 0:34
work$
これでうまく証明できてるのかな?
0577132人目の素数さん
2005/10/01(土) 07:38:00「無矛盾と分かっている」の「分かっている」は飽くまでお前が
勝手に付け加えただけだと思うぞ
>>458を読む限り、無矛盾性が証明されている、
という意味で「分かっている」という言葉を使っているんだろうけど
一番初めの
>設定した公理系は無矛盾であったが
は、別に無矛盾である、ということが「分かっている」必要は無い
無矛盾かどうかは天のみぞ知る、ただし、実際には、誰一人人間には
証明できないにせよ、無矛盾であった、という状況で充分
0578132人目の素数さん
2005/10/01(土) 07:40:17A:お前は間違っている!
B:数学的な命題以外はすべてただの感想でしょ。
早く数学的な命題を述べてよ、はやくはやく。
A:こいつは莫迦だ、退散しよう。
の繰り返しだと思うぞ。
0579576
2005/10/01(土) 07:43:15ただ、mizarに含まれているライブラリ(Mizar Mathematical Library)のファイルの
行数を数えてみると、183万行もある。(C:\mizar\mml\*.mizの行数を合計)
このライブラリ内の定理を jordan.miz で利用しているようなので、
その部分を考慮すると20万行になるということなのでしょう。
0580132人目の素数さん
2005/10/01(土) 07:44:284次元kissing numberの論文とかあるじゃん
0581576
2005/10/01(土) 07:46:22それにしても、このライブラリを記述した人達の労力を考えると、絶句・・・ですね。
0582132人目の素数さん
2005/10/01(土) 08:33:24形式体系についての解釈(主観)
この区別がついてない馬鹿が紛れ込んでただけ
0583132人目の素数さん
2005/10/01(土) 08:40:17しかもまだその話題引っ張ってんのか?
過去ログ読んだけど>>417の
>そしてそれが嘘であることを暴くのが形式的証明。
は全く独り善がりだと思うがな
まあ個人的意見だというのなら敢えて否定はしないけど
それなら、普通は私見だが、とか一言書くものだけどな
0584132人目の素数さん
2005/10/01(土) 09:04:10お前さえ我慢すれば全てがまるく収まることに気づけ
0585132人目の素数さん
2005/10/01(土) 09:04:57無矛盾性を意味すると解釈される命題で、証明図のない物がある。
実は、一方で
無矛盾性を意味すると解釈される命題で、証明図のある物がある。(ゲーデルの世界p141)
まずは形式体系とその解釈の区別をつけましょう
0586132人目の素数さん
2005/10/01(土) 09:05:55>区別が できない奴が一名、紛れ込んでいるみたい
それをいうなら、真偽の判定は前者ではなく
後者の問題だってことが分からない阿呆が
一名いるな。
0587132人目の素数さん
2005/10/01(土) 09:12:28上記の場合、証明図の二つの形式的定義
(カット入りとカット無し)によって、
証明可能な定理の全体が等しくなるかどうか
が問題となる。
これは自然数論では証明ができない。
つまり、自然数論の形式体系に合致する解釈において
反例が存在する。しかし、このような「反例」は
そもそも想定されていたものではない。
0588132人目の素数さん
2005/10/01(土) 09:20:34「そもそも語りたかったこと」
を語っているかどうかはもっとも
重要なポイント。
0589132人目の素数さん
2005/10/01(土) 09:31:52>気違い以外は、両方の価値を認めている。
本当に狂ってるのは、
「俺は客観(=価値中立)的立場に立っている」
と叫んで、自分自身を消去しようとしてる奴。
こういう奴が自殺する。
0590132人目の素数さん
2005/10/01(土) 09:33:14現在の論理体系ではあのバナハ・タルスキーのパラドクスが
OKとなるがいいのだろうか
0591132人目の素数さん
2005/10/01(土) 09:50:06カットって何のこといってるの?
LKとかLJの話してるわけじゃないはずだが
0592132人目の素数さん
2005/10/01(土) 09:50:45何が困るの?
論理体系の話じゃなくて公理系の話じゃないの?
0593132人目の素数さん
2005/10/01(土) 10:23:25だが、客体が存在する事に変わりはない
それとは別に真偽判定(数学的な物に限らない)の対象にならない表現行為、という物もある
例えば「これ旨いね」
人間が行う発言の内で、真偽判定の対象になる物は非常に少ない。この少ないという発言自体がな(w
0594132人目の素数さん
2005/10/01(土) 10:33:40客体(客観)は存在し、証明図は客体である
多くの発言は真偽判定の対象ではない。普通に証明できれば「適当な」形式体系で証明がある、とかもその一つ
0595132人目の素数さん
2005/10/01(土) 10:36:390596132人目の素数さん
2005/10/01(土) 11:32:31証明図がある(客観)
に必ず間隙が存在する事をゲーデルは証明した。
だからと言って、証明図(客体)が消える訳じゃない。当たり前だがな(w
0597132人目の素数さん
2005/10/01(土) 11:37:03まあそれは兎も角
このスレはJordanの曲線定理の「完全証明」について話すスレじゃないのか?
0598132人目の素数さん
2005/10/01(土) 13:11:10普通はない
もちろん、別の形式体系をもってきて「形式的な真」を定義することもある。「普通の真」が「形式的な真」に対応するか、
どうかが主観的な判断である以上、「普通の真」は永遠に主観的なままだ。とは言え
形式的真は普通の真の補強材料くらいにはなるから、それなりに意味はあると思うよ
0599132人目の素数さん
2005/10/01(土) 13:29:44こうやってただのオウム返しを繰り返しながら(本人は鋭い切り返しだと思ってるようだがw)
強引に自分が説教したい方向にスレの内容を引っ張っていくんだよね。
基礎論のスレっていつもこのパターン
0600132人目の素数さん
2005/10/01(土) 13:31:11形式的真により、別体系でより多くの命題が真であることが証明可能になることはある。
しかし、当たり前の事だが、全ての命題が、別体系で決定可能になる訳ではない
0601132人目の素数さん
2005/10/01(土) 13:33:41↑こっちのスレにも書いてくださいよ
http://academy4.2ch.net/test/read.cgi/philo/1127033882/108 さーんw
0602132人目の素数さん
2005/10/01(土) 13:42:57しかも・・・
頼むから帰ってくれ
0603 ◆0wCTzeasu2
2005/10/01(土) 14:05:18西川青季「幾何学」でジョルダン閉曲線定理の勉強中
証明の概略を書いていきたいと思います。
0604132人目の素数さん
2005/10/01(土) 14:50:23形式的証明にこだわるのは変だとは思うし、597の「真」の定義というのは所詮
数学的定義だから、いわゆる「真」ではない。しかし、チミはなにがいいたい
わけ。ご高説を滔々と述べられたらいかがですか。
0605132人目の素数さん
2005/10/01(土) 15:17:07>カットって何のこといってるの?
おお、先走った。
ロッサーの方法による無矛盾性と、
カット抜きの証明の定義による無矛盾性は
別物だったな。
とはいえ、ここでは無矛盾性のようなものにも
異なる形式化が考えられ、しかもそれは体系に
よっては異なる意味をもつ場合があると考えられる
わけであるから、単純に形式化以降の話をチェック
したって「真偽判定」については無意味だってこと。
0606132人目の素数さん
2005/10/01(土) 15:23:10>真偽判定(数学的な物に限らない)の
>対象にならない表現行為、という物もある
>例えば「これ旨いね」
レイ・スマリヤンの「認識論的悪夢」って話を知ってるかい?
「これは何色か?」という質問に、
「僕には赤く見えます」と答えた人が
「違う!」と反駁されてそこから延々と
議論が始まるわけだ。
そこでのもっとも重要なポイントは
「「僕には赤く見える」という発言が間違ってるなんて
他人に言えるわけがない」という発言が間違ってること。
ちなみに、上記の質問で提示された色は・・・赤!
0607132人目の素数さん
2005/10/01(土) 15:31:27これを発表した中村教授は今度大学院を
設立する。その話題作りの一つだ。まだ、
気が付かないのか。
0608132人目の素数さん
2005/10/01(土) 15:32:46君の間違いは、真偽判定=証明探索だと思ってること。
でも実は違うんだ。つまり「これ旨いね」という発言に
何の証明がなくとも、君が旨いねと思ってそういったなら
それは真実なんだよ。
0609132人目の素数さん
2005/10/01(土) 15:41:14>ある命題が真である、ということには
>ちゃんと数学的な定義があるんだけどな
それには二階論理を使う。実は二階論理は形式化できない。
ただ、数学的=形式的ではない。
>>598
>普通はない
君のいう"普通"が形式的体系でのことならその意味では正しい。
しかし、普通=形式的ではない
0610132人目の素数さん
2005/10/01(土) 15:46:02追伸
>597の「真」の定義というのは所詮数学的定義だから、
>いわゆる「真」ではない。
597の定義を、無理矢理形式化してしまった
モデル理論の中で考えるならそうだろう。
しかし、数学的定義=形式的定義
だと考えるほうが実はおかしい。
0611132人目の素数さん
2005/10/01(土) 16:48:090612598
2005/10/01(土) 17:25:26>モデル理論の中で考えるならそうだろう。
「形式的な真」の定義ということは、そういうことだ。
それと、「普通の意味での真」は別物だろ
もちろん、関連していると主観的に思えるように形式
化するけどな。
0613598
2005/10/01(土) 17:27:46>>610
> 597の定義を、無理矢理形式化してしまった
>モデル理論の中で考えるならそうだろう。
「形式的な真」の定義ということは、そういうことだ。
それと、「普通の意味での真」は別物だろ
もちろん、関連していると主観的に思えるように形式
化するけどな。
>>604
君と同じことが言いたかったんだと思われ
0614598
2005/10/01(土) 17:41:00ただ、数学的対象物に対する主張が正しいことを真と言い、
間違っていれば偽と言うだけだから
まあ、こんなものでも数学的定義と呼びたければ、それも
ありだと思うよ。結局、言葉の選択問題に過ぎないけどな
>>608
>君の間違いは、真偽判定=証明探索だと思ってること。
>でも実は違うんだ。つまり「これ旨いね」という発言に
>何の証明がなくとも、君が旨いねと思ってそういったなら
>それは真実なんだよ。
あーあ、やっちゃいましたか?うんうん。
君は
感想が本心であれば、正しい
感想が本心でなければ、間違っている
というように表現するんだね。俺はそんな言葉使いは
控えたいね。ところで、俺は本心から「これ旨いね」
は真偽判定の対象ではないと思っているわけだから、
俺は正しいよ。おっと、つい使ってしまったw
0615598
2005/10/01(土) 17:46:06形式体系では真を定義できない。
しかし、そのモデル理論を形式化することにより
真が形式的に定義される。
0616598
2005/10/01(土) 17:47:120617598
2005/10/01(土) 17:54:20形式体系を対象とした普通の実在主義数学。
しかし、そのモデル理論を形式化したもの
こそが考察されるべき客体だ、と考えれば
また形式主義が復活する。
形式主義は、永遠のいたちごっこ。しかし、
それが無意味だと思わない。ま、俺は普通
数学しか、やらないけどね。
0618132人目の素数さん
2005/10/01(土) 17:56:49> 普通の(形式化されてない)モデル理論は、
> 形式体系を対象とした普通の実在主義数学。
完全性定理が好例か
0619132人目の素数さん
2005/10/01(土) 18:01:02>形式主義は、永遠のいたちごっこ。しかし、
>それが無意味だと思わない。
というか、普通の数学にも終わりがないわけだから、
どちらにしても、数学は永遠のいたちごっこ。でも
それでいいwww
0620GiantLeaves ◆6fN.Sojv5w
2005/10/01(土) 18:04:240621132人目の素数さん
2005/10/01(土) 18:05:24>>608 は結局、これだろ?
>ただ、「単に感想レベルの話」でも、他人との対立や矛盾を
>許容したくないだけでは?
0622132人目の素数さん
2005/10/01(土) 18:05:570623ニートドラゴン ◆Ylfrus2v8U
2005/10/01(土) 18:06:030624132人目の素数さん
2005/10/01(土) 18:14:28形式数学も、普通数学もツマンネーよ。
数学やってる奴は皆、馬鹿。死ね死ね!
ハハハハハハ
0625132人目の素数さん
2005/10/01(土) 18:18:21実際には、計算機は止まるか止まらないかの二者択一しかないだろう。
同様に、真か偽ではある命題も、形式的に証明できるとはかぎらない。
0626ニートドラゴン ◆Ylfrus2v8U
2005/10/01(土) 18:22:57その理論的な奥深さを、自分の論理による理解として実感できるからだ。
ところが哲学厨は、微積分すらまともにできない分際で、そこらの雑学書に書かれた
パラドックスや停止問題を「あたかも」自分が理解しましたというように容易に使う。
「〜は〜できないが、〜であろう」
理解していない。理解の中身なしに語れるほど数学の世界は浅はかではないさ。
ということで、哲学厨は嫌われるんだよ。
必死で努力してやってるやつらと同じレベルで語れるはずがないだろうが。
0627ニートドラゴン ◆Ylfrus2v8U
2005/10/01(土) 18:23:280628132人目の素数さん
2005/10/01(土) 18:24:35基礎論の初歩。ただし、「証明図があれば、普通の意味で真」と
いうのも主観的判断。つまり、この形式化はおかしくないという
主観的判断。
ただし、通常はそのように期待するので、多くの場合、証明図が
あることが分かれば、普通の意味でも証明されたものと考える。
0629132人目の素数さん
2005/10/01(土) 18:26:31>切り返しって言葉を使うのは哲学厨
なんだそりゃ・・・そんなの聞いたこともないよ
こっちは哲学板のことなんか全然しらないってーの
ただ偶然にも、基礎論系のスレでいっつも同じことしてる人がいるようなんで
質問してみたまでだよ
0630132人目の素数さん
2005/10/01(土) 18:33:01本当は最初からこれが言いたかったんでしょ?
0631132人目の素数さん
2005/10/01(土) 18:33:38つーか、「これ旨いね」は真偽判定の対象ではないだろ。
ま、「『これ旨いね』という発言は本心である」なら、
まだ真偽判定の対象になりうるのかもな ← 本当かねw
0632132人目の素数さん
2005/10/01(土) 18:36:00でもさ、普通数学では「真」の定義は存在しないし、
形式体系にも存在しない。としたら、「真」を定義
する場面ってモデル理論しかないよな
0633132人目の素数さん
2005/10/01(土) 18:39:42やはり「真」の定義がある訳でない。モデル理論を形式化した場合には
「形式的な真」の定義が現れる
かなり、特殊な状況だぞ
0634132人目の素数さん
2005/10/01(土) 18:45:43すれば、解釈ごとによって何が真になるのかが変わってくる。
ということは、真の定義はあるとも言える。ま、「解釈」を定義すると
言う方がしっくり来るが…
0635132人目の素数さん
2005/10/01(土) 19:24:50君は何を言ってるのかなあ、、
君が話の流れを強引に自分の持って行きたい方向に引っ張っていかない限り
カットの話なんて全く出てくるはずが無い
そもそもこのスレを何について話すスレだと思ってるんだか、、はぁ
0636132人目の素数さん
2005/10/01(土) 19:27:30「普通数学」って君の造語ですか?初めて聞いた
それは兎も角、そろそろ話を>>1と関連した話に戻しませんか?
0637132人目の素数さん
2005/10/01(土) 20:01:12単なる「普通の数学」の略だと思われ
0638132人目の素数さん
2005/10/01(土) 20:02:57数学板的には、面白い話題ではない。
ソフトウェア工学版にこそ相応しい。
0639132人目の素数さん
2005/10/01(土) 20:06:280640132人目の素数さん
2005/10/01(土) 20:08:530641132人目の素数さん
2005/10/01(土) 20:31:350642132人目の素数さん
2005/10/01(土) 20:33:08死ね死ね死ね死ね死ね死ね
死ね死ね死ね死ね死ね死ね
死ね死ね死ね死ね死ね死ね
0643132人目の素数さん
2005/10/01(土) 20:35:02死んでも出来ませんが
0644132人目の素数さん
2005/10/01(土) 21:40:42あーあ、やっちゃいましたか?うんうん。 君は
感想が本心であれば、正しい
感想が本心でなければ、間違っている
というように表現するんだね。俺はそんな言葉使いは
控えたいね。ところで、俺は、「これ旨いね」は真偽
判定の対象ではないと本心で思っているわけだから、
俺は正しいよ。おっと、つい使ってしまったw
0645132人目の素数さん
2005/10/01(土) 21:53:36形式的証明(客観)
しかし、どちらも「真」であることについての
絶対的証明にはならない。これが現実
0646132人目の素数さん
2005/10/01(土) 21:56:11どちらも、主観的確信を強めるだけ。
0647132人目の素数さん
2005/10/01(土) 22:03:02ルールに則って判断するに「○○」
だ、という程の意味だね、普通は。
絶対的にその判断が正しいという
ことではない
絶対的な正しさには永遠に到達し
ないのは、当たり前なんだからさ
0648132人目の素数さん
2005/10/01(土) 22:09:33形式化された体系に則って判断するに
正しい、と言う程の意味だ。絶対的に
正しいとは、何ら言ってないのだよ。
しかし、ルールに則っての判断=絶対
という可笑しな脳内等式を持っている
奴が勘違いをすることがある訳だな。
0649132人目の素数さん
2005/10/01(土) 22:17:17「ルールとして何を採用するのか
?」という闘争だ。
0650132人目の素数さん
2005/10/01(土) 22:19:50自分を消すと言うことではない。
既存のルールに逃げ込むと言う
方が、適切だ。
0651132人目の素数さん
2005/10/01(土) 22:25:220652132人目の素数さん
2005/10/01(土) 22:27:030653132人目の素数さん
2005/10/02(日) 00:20:29B 間違ってます
A そうだな。旨いじゃなくて、まいうーって感じ
B 間違ってます
A じゃ、ヤバイは?
B 間違ってます
A うめぇ〜、は?
B まずいよ、これ
A 君の口には合わないんだね。君にそう言われると、僕もそんな感じがしてくるなあ
B …
0654132人目の素数さん
2005/10/02(日) 00:22:350655132人目の素数さん
2005/10/02(日) 08:33:09>関連していると主観的に思えるように形式化するけどな。
だったら、最後は形式ではなく主観で決めてんじゃん。
自分の存在を忘れるなよ(w
0656132人目の素数さん
2005/10/02(日) 08:41:440657132人目の素数さん
2005/10/02(日) 08:57:12>普通の(形式化されてない)モデル理論は
>形式体系を対象とした普通の実在主義数学。
>しかし、そのモデル理論を形式化したものこそが
>考察されるべき客体だ、と考えれば
>また形式主義が復活する。
君の間違いは、形式化されたものが客体だと考えていること。
実は形式化は客体ではない。客体でないからこそ、形式体系が
言い表しえるものを、モデル理論で考えるわけだ。
しかし、そのものとかいうのも、結局形式化してしまったら、
またそれが言い表しえるものを考えなくてはならない。
これは無限後退だね。
いいかい、そこで主体が責任をもつ必要があるんだよ。
君のように責任を恐れる臆病者には数学は無理なんだよ。
0658132人目の素数さん
2005/10/02(日) 09:07:27集合論や論理式はあとでいいから
最低限
微積分とイデアルまではやってくれ
話が紙泡ねえ
0659132人目の素数さん
2005/10/02(日) 09:08:53>普通数学では「真」の定義は存在しないし、
>形式体系にも存在しない。
>としたら、「真」を定義する場面って
>モデル理論しかないよな
その突っ込みは的外れ。
そもそも、形式体系が、いいたかったこと以外の意味も持ちえる
と示したのがモデル理論なのだから、これを形式マンセーの人が
持ち出すのは自爆である。
0660132人目の素数さん
2005/10/02(日) 09:12:14>「普通数学」って君の造語ですか?
>>637
>単なる「普通の数学」の略だと思われ
余談だが、世の中にはひらがなを嫌い
漢字だけの熟語にしたほうが
カッコイイと思う馬鹿がいる。
0661132人目の素数さん
2005/10/02(日) 09:18:42>客観的に「○○」だ、っつーのは、
>ルールに則って判断するに「○○」
>だ、という程の意味だね、普通は。
素人がそういう言葉遣いをするのは知っているが、
客観の本来の意味からすると間違っている。
0662132人目の素数さん
2005/10/02(日) 09:21:46そんなの当たり前だっつーの
ルールに従って、判断したって事を客観的って言っているんだよ。
馬鹿め(w
それが言葉の使い方だよ
0663132人目の素数さん
2005/10/02(日) 09:28:06>絶対的な正しさには永遠に到達しないのは、当たり前なんだからさ
前提条件が抜けたぞ。
「ルールに則るという行為で、絶対的な正しさを示すことはできない。」
これが正解。
しかし、正しさの判断は、常にルールに則っているわけではない。
特に、どのルールを取るか、という判断はルールに則っていない。
>>649の「何をルールとして採用するのか?」は主観的である。
しかしだからといって必ず他人と相違するというわけではない。
0664132人目の素数さん
2005/10/02(日) 09:28:19客観がどうかとか、どうでもいいから
Jordanの曲線定理の話をしませんか?
0665132人目の素数さん
2005/10/02(日) 09:29:30>馬鹿め(w
馬鹿は、常識を疑わない貴様だ。
考えないものに学問は無理だ。
0666132人目の素数さん
2005/10/02(日) 09:29:35あのさ、君の言うような事はとっくに認識しているの
君の引用した所の後に、永遠のいたちごっこってあるでしょ。
だから、と言って形式体系が消えるわけじゃないよ。君の可笑しなとこだな
0667132人目の素数さん
2005/10/02(日) 09:30:34>Jordanの曲線定理の話をしませんか?
君はできませんか?
ああ、できませんか。では、勉強してください。
君が知らないのなら話はできないでしょう。
0668132人目の素数さん
2005/10/02(日) 09:32:54>だから、と言って形式体系が消えるわけじゃないよ。
私は形式体系が消えるとは一度もいっていないが。
君が「ルールに則る」ことに異常なエクスタシーを
感じる性癖だと感じたからその愚かさを笑ったまでだ(w
0670132人目の素数さん
2005/10/02(日) 09:36:32何甘えてるんですか。
そりゃ困るでしょう。
君が無知で自分から話を始められないから
他人が話してくれるのを待って焦れてるんでしょう。
そのまんま黒焦げになってください(w
0672132人目の素数さん
2005/10/02(日) 09:50:47誰が形式マンセーなの?
モデル理論があるのは「形式体系を調べる事には意味がある」と考えているから。
君のように一つの哲学的(藁)主張をしてそれで終わりじゃないし、
モデル理論という分野が出来る前から、君の言うような事は常識に過ぎない。
形式体系が絶対じゃないのは当たり前の事だが。だからと言って、無意味と言う訳でもない。当たり前だが
君の間違いは「形式化に意味があると普通に考えてる人達が
形式体系から読み取った出張は絶対だとも考えている」と君が思ってる事にある
0673132人目の素数さん
2005/10/02(日) 09:55:51Jordanの曲線定理の話をしませんか?といいつつ
自分からは話できないのは無知だからでしょ?
違いますか?(wwwwwww
0674132人目の素数さん
2005/10/02(日) 09:58:20その人達が規則は絶対だと考えてる訳じゃない事は、当たり前。
なぜなら、規則を作ったのは自分だから
0675664
2005/10/02(日) 10:02:22あのね、上のほうでは>>1の件について普通にレスしてたんだけど
モデル理論がどうの、とか主観がどうの、とか言う人ばかりだと
話しづらいんですよ
>君が知らないのなら話はできないでしょう。
自分はスレに沿った話題を話したいのに
回りの人間のせいでできない、みたいなこと言わないで貰えませんか?
明らかにそういう状況ではありませんので
0676132人目の素数さん
2005/10/02(日) 10:02:32>一つの哲学的(藁)主張をしてそれで終わりじゃないし
一つしかない君の迷信を延々と繰り返されても迷惑だよ。
「・・・には意味がある」というのは無意味
「昔から常識」というのは誤り
「・・・が絶対じゃない」というのは苦し紛れの言い訳
単に、君自身無意識であったことを他人の指摘で
やっと気づいただけ。全ては君の軽率さによる誤り。
0677132人目の素数さん
2005/10/02(日) 10:05:37>モデル理論がどうの、とか主観がどうの、
>とか言う人ばかりだと 話しづらいんですよ
では話さなければいい。
>自分はスレに沿った話題を話したいのに
>回りの人間のせいでできない、みたいなこと
>言わないで貰えませんか?
君がいっているのはそういうことだが。
>明らかにそういう状況ではありませんので
明らかにそういう状況だが、君が恥ずかしさから
認めたがらないだけ。そりゃそうだろう。ただの
教えてクンだなんていったら「ばーかばかばか」
と罵られるのがオチ。実際は罵ってるほうも、
同類のバカなんだが(w
0678132人目の素数さん
2005/10/02(日) 10:07:40>規則を作ったのは自分だから
あとからこっそり相手のいってることをなぞったからといって
自分がはじめにいってたことの誤りが自分の中から消せるわけ
ではない。
0679132人目の素数さん
2005/10/02(日) 10:12:42もちろん、そういう事をしてない以上、そういう事をしなければいけないとも思ってない
形式化に意味があると考えるのは普通。だからと言って、形式化しなければいけないと考える気違いには
生憎、お目に掛かった事がない
0680132人目の素数さん
2005/10/02(日) 10:15:173次方程式が虚数解を持つ→グラフがx軸を1回しか交差しない→極小値が0より大きい
をヒントにがんばってみて!
0681132人目の素数さん
2005/10/02(日) 10:15:41「普通の数学」しか知らないんなら、
形式化とはどういうことかなんて
分かってないだろ。
だったら知ったかぶって口挟むなよ。
みっともないんだよ。バカが
0682680
2005/10/02(日) 10:16:170683132人目の素数さん
2005/10/02(日) 10:17:30ご安心を。正しく配送しなおしました。
0684132人目の素数さん
2005/10/02(日) 10:19:27>>679には>研究してない
と書いてあるようだが?
もしかして計算機による定理の証明の話には、
それを専門に研究している工学者しか話をしちゃいけないのか?
0685132人目の素数さん
2005/10/02(日) 10:21:06ここで主観が出て来たからと言って客観が消える訳じゃない。間違いが分かりましたか?
0686132人目の素数さん
2005/10/02(日) 10:29:07客観に意味を認めてたら、客観マンセーなのかよ?(w
0687132人目の素数さん
2005/10/02(日) 10:43:36あっ、そうか。君の周りには「形式化マンセー」って
基地外がいるのか?それを叩いてるつもりだったのか
生憎、ここは数学板。普通の数学を勉強してる人間が
中心。だから、形式化マンセー君に出会うのは難しい
のでは?普通に数学をやってる人間は形式化の意義を
認めつつ、別に絶対視してない。絶対視してないのは
それをやってないんだから当たり前なんだが
0689132人目の素数さん
2005/10/02(日) 11:00:16素人がそういう意味として使っていることを知ってるなら
そういう意味として受け取ればいいんじゃないのか?
ま、知らなかったのなら、受け取りようもないがなあ
君の間違い3.他人の発言の言葉の使い方の意味を認めず、
自分の使い方の意味で解釈することに拘り、
それを押し付けようとすること
で、さ、「君の言葉の使い方」では客観はないのだろう?
で、ないものに何でそんなに拘るのかな?
ま、俺には君がどういう意味で客観という言葉を使ってる
のかが、そもそも分からないんだけどさ。
0690132人目の素数さん
2005/10/02(日) 11:16:59哲学的な「客観」について議論したいのなら、哲版に逝ったほうが
いいと思われwww
0691132人目の素数さん
2005/10/02(日) 11:34:38あるいは、相手の発言からそれが読み
取れなかったら間違いだと考えること
正しい4.「間違ったこと」を意識していたら、
あるいは、相手の発言からそれが読み
取れたら、間違いだと考えること
0692132人目の素数さん
2005/10/02(日) 11:34:450693132人目の素数さん
2005/10/02(日) 11:38:51普通(素人)の意味で「客観」という言葉が使われているのに、
何だか哲版の意味でそれを解釈して、「間違っている」と判断
しただけでしょ。
客観がないとか、どうとか、繰り返してる人は。いい加減、
間違えを認めたら
0695132人目の素数さん
2005/10/02(日) 12:17:40ttp://mathworld.wolfram.com/images/eps-gif/AlexandersHornedSphere_1000.gif
0696132人目の素数さん
2005/10/02(日) 12:26:01基地外4.「正しいこと」を意識してなかったら、
あるいは、相手の発言からそれが読み
取れなかったら間違いだと考えること
ふつう4.「間違ったこと」を意識していたら、
あるいは、相手の発言からそれが読み
取れたら、間違いだと考えること
0697132人目の素数さん
2005/10/02(日) 12:45:34一番一般的なものなど、ありますが、どの証明がなされたのでしょうか?
また、証明検証の問題がからむと、一般的な定理の方が必ずしも簡単にはならない
ということもおきると思われます。
このような話題も色々あると思いますがね、、、。
0698132人目の素数さん
2005/10/02(日) 13:38:04>で、さ、「君の言葉の使い方」では客観はないのだろう?
>で、ないものに何でそんなに拘るのかな?
>ま、俺には君がどういう意味で客観という言葉を使ってる
>のかが、そもそも分からないんだけどさ。
おい、お前はバカか?
「客観」は存在しないのだから、理解する必要もないだろが
0699132人目の素数さん
2005/10/02(日) 13:40:03そうですかね
まあ証明が簡単になるための条件をゴタゴタくっつけた方が簡単にはなるんでしょうが
0700132人目の素数さん
2005/10/02(日) 13:40:08話がまとまるわけがないw
0701132人目の素数さん
2005/10/02(日) 13:41:12「完全証明」って言葉なんだよな
自分の業績を過大評価させるために大げさな言葉を使う
まあ良くあることではあるがいくらなんでもやり過ぎだと思うけどな
0702132人目の素数さん
2005/10/02(日) 13:42:36ポモ的だ!黒木さんに言いつけようw
0703132人目の素数さん
2005/10/02(日) 14:04:43黒木さんのページ(一番下にメアドがあります)
http://www.math.tohoku.ac.jp/%7Ekuroki/index-j.html
同掲示板
http://www.math.tohoku.ac.jp/%7Ekuroki/keijiban/
0704132人目の素数さん
2005/10/02(日) 14:08:390705132人目の素数さん
2005/10/02(日) 14:10:27>そして、別の場所で、極端なことを言っているのではないかと非難された場合には、
>3 (a) に近い穏健だが当たり前の主張を述べて批判をかわします。
『「知」の欺瞞』の相対主義批判
http://www.math.tohoku.ac.jp/~kuroki/FN/relativism.html#FN
「相対主義」が嫌われる理由
http://www.math.tohoku.ac.jp/~kuroki/FN/relativism.html#hate
0706132人目の素数さん
2005/10/02(日) 14:15:10>どの証明がなされたのでしょうか?
なぜ、自分で証明を読まないのでしょうか?
もしかして読めないのでしょうか?
0707132人目の素数さん
2005/10/02(日) 14:15:34「完全証明」という言葉で、今までの数学的証明が不十分だったと
印象操作して(強い主張)、それを非難されれば「形式的証明」と
いう意味だ、と批判をかわします。このようなことはポモに限った
ことでなく、数学的な分野でもあることです。まずは自分の身近な
分野から叩こうぜ、な
>そういえば黒木さんの掲示板も最近は寂れてるねえ
私がやってやりました!
0708132人目の素数さん
2005/10/02(日) 14:18:49>計算機による定理の証明の話には、
>それを専門に研究している工学者しか
>話をしちゃいけないのか?
なぜ形式的証明の意義という数学の哲学の話に
いきなり工学者がでてくるんだ?唐突だろ?
0709132人目の素数さん
2005/10/02(日) 14:21:24>規則に則って判断する事を客観と言う
>>687
>素人がそういう意味として使っていることを知ってるなら
>そういう意味として受け取ればいいんじゃないのか?
素人はいつでも傲慢だ。自分が間違ってるときは考えない。
考えないことによって間違いを意識せずにごまかす。
0710132人目の素数さん
2005/10/02(日) 14:22:2420万行も読む気力と暇の有る人は少ないかと
0711132人目の素数さん
2005/10/02(日) 14:23:02>まずは自分の身近な分野から叩こうぜ、な
U沢さんのことか?w
0712132人目の素数さん
2005/10/02(日) 14:24:470713132人目の素数さん
2005/10/02(日) 14:26:28>いずれにせよ、今回の報道で個人的に一番許せないのが
>「完全証明」って言葉なんだよな
形式的=客観的っていってる人は
形式的証明=完全証明っていってるように聞こえるが、どうか?
違うなら、客観のどこが完全でないか説明してちょ?
0714132人目の素数さん
2005/10/02(日) 14:26:39だからここは哲学板でもないし、数学の哲学のスレでも無いよ、というのはまあ別の話として、
「俺は普通数学しか研究してないけど」に対して
それなら口を挟むな、というレスがあったわけで、
それなら形式的証明に関して研究している人
(そういう人を工学者と呼ぶか数学者と呼ぶかはまあ呼び方の問題ね
中村教授が工学部の人であるのは間違いないけど)
しかレスするな、と言ってるのかな?と疑問を持つのは自然な事だと思いますが
0715132人目の素数さん
2005/10/02(日) 14:30:15だから、客観の普通(素人)の意味は、
ルールに則ってという程の意味だって
言ってるじゃんか、ね
0716132人目の素数さん
2005/10/02(日) 14:30:50普通の証明と形式的証明の違いを論じるのは数学の哲学だよ。
知らなかった?知らなかったなら知って。今すぐ。
>「俺は普通数学しか研究してないけど」に対して
>それなら口を挟むな、というレスがあったわけで、
数学の哲学をバカにするような無知蒙昧な輩に
口を挟むなというのは当然じゃない?
君はチーマーのオヤジ狩りに賛同するわけ?
狂ってるね。人間としてさ。
0717132人目の素数さん
2005/10/02(日) 14:31:28開き直るなよ。バーカ
0718132人目の素数さん
2005/10/02(日) 14:33:41>しかレスするな、と言ってるのかな?
形式的証明に関して研究している人が
形式的証明の意義を議論するにふさわしい
とは限らないな。
数学を研究している人が
数学の意義を議論するに
ふさわしいわけではないように。
0719132人目の素数さん
2005/10/02(日) 14:36:11哲学的な客観ってないんだよね。ないんなら、知らなくても
いいと思うだけど、違うの?哲学って奥が深いや。うんうん
そういう深い事が分かるなんて、君は凄い人なんだ。僕には
難しくて分からないや。ごめんね
0720132人目の素数さん
2005/10/02(日) 14:38:29してもいいだろ?そうじゃない人も、もちろんしていい。
そんなことに客観的「資格」を求めるのか?w
0721132人目の素数さん
2005/10/02(日) 14:54:28このスレは飽くまで信州大の人がJordan曲線の定理を計算機で証明しましたよ、
というニュースのスレであって、「数学の哲学」の観点から語らないといけない、
という縛りはないよ(君の脳内にはあるのかもしれないが)
別に普通の数学研究者の観点から今回の証明を評価するのも自由だ
>>679のどこが数学の哲学を莫迦にしてるんだ?
哲学のての字も書いて無いし、普通の数学研究者の実感を表明してるだけに見えるんだが
それをチーマーのオヤジ狩り呼ばわりする君のほうが狂ってるね。人間としてさ。
それとも「数学の哲学」では形式化に意味がある、だけでは飽き足らず
形式化しなければいけない、と極端なことを言わなきゃ無知蒙昧呼ばわりされるのかね?
それじゃほとんど宗教じゃないですか
0722132人目の素数さん
2005/10/02(日) 15:06:25いや、君と違って頭のいい人なら、哲学的な「客観」の意味も
それが存在しないことも理解できるんだよ、きっと。
頭のいい哲学さんに、君は見捨てられるのさ
>哲学さん
啓蒙活動、もっとよろしく!俺、むちゃ理解したいよ♪
0723132人目の素数さん
2005/10/02(日) 15:35:58次のようになります。
653 :132人目の素数さん :2005/10/02(日) 00:20:29
A 旨い!
B 間違ってます
A そうだな。旨いじゃなくて、まいうーって感じ
B 間違ってます
A じゃ、ヤバイは?
B 間違ってます
A うめぇ〜、は?
B まずいよ、これ
A 君の口には合わないんだね。君にそう言われると、僕もそんな感じがしてくるなあ
B …
0724132人目の素数さん
2005/10/02(日) 15:37:33一般的な定理が成立しているとして、具体的な場合に成立することを示すには、その
具体的な場合が定理の条件を示す必要がある。これは、べつに計算機で検証できる証明
にかんしたことでなくても大変なことはよくある。計算機での検証を考えると具体的
な場合というのは、その対象の表現の問題もあるので、かなり面倒なのではないで
しょうか?
一般的な定理は、定理の条件が証明に合わせて提示されている場合、証明をつくること
が簡単ということはありえる。どちらにしても数学での証明とは異なったところの工夫
が必要なはずだが、ともかく、piecewise linear 版なんですか、それとも一般版なん
ですかね。こんなことも話題にならないとすると、ニュースが Wiles の定理の証明だ
ったとしても、おんなじようにやり合うわけなんだ。
0725132人目の素数さん
2005/10/02(日) 15:41:39Bが本当に欲しい反応は、このレストラン
駄目じゃん、というものなのです。まあ、
一生かかっても、無理でしょう。
0726132人目の素数さん
2005/10/02(日) 15:43:47> Wiles の定理の証明だったとしても、おんなじよう
> にやり合うわけなんだ。
そう思われwww
0727132人目の素数さん
2005/10/02(日) 16:10:13杉村太蔵と同レベル
0728132人目の素数さん
2005/10/02(日) 16:27:21なかなか楽しかったよ、オヤジ狩り。
言っとくけどな、俺たちはチーマーじゃねえ
カラーギャングだ。今度、チーマー呼ばわり
したらぶっ殺すからな。覚えとけw
0729132人目の素数さん
2005/10/02(日) 16:39:48オヤジ=哲厨
チーマー=形式数学者
ギャング=普通数学者
0730132人目の素数さん
2005/10/02(日) 16:44:25ギャングを見て、「チーマーだ。怖い」とオヤジが言ったのに
切れたギャング達が、オヤジに襲い掛かって、ぼこぼこにする。
最後に「俺たちはチーマーじゃねぇ」と捨て台詞を吐き捨てる。
オヤジは、ギャングが切れた理由を考えるのだが…
0731132人目の素数さん
2005/10/02(日) 17:41:47「信州大の人がJordan曲線の定理を計算機で証明しましたよ」
というニュースに対して、どういう議論をしようと自由だが、
普通の証明と形式的証明との差異に対して、ルール順守が客観だ
とかいうナイーブな態度を強制するのは間違っている。
そういう狂信家は出て行くべきだ。
0732132人目の素数さん
2005/10/02(日) 17:45:10> とかいうナイーブな態度を強制する
強制はしてないだろ。「客観」という言葉の意味を説明しているに
過ぎないからな
0733132人目の素数さん
2005/10/02(日) 17:49:06まったく要約になっていない。なぜなら中身が異なるから
A「俺が”旨い”といったとき、これは真偽とは無関係だ」
B「なぜ?君が旨いと思って”旨い”といったなら、それは真実だろう」
A「しかし、お前には俺がどう思ってるか分かるまい」
B「そりゃ僕には分からんよ。しかし僕に分からないからといって
真偽とは無関係だということにはならないよ。」
A「ハァ?真か偽か分からないのに真偽を云々するなんてバカだろ」
B「おや、君は自分でも旨いと思ってないのに旨いって言ってるのかい?」
A「俺にわかっても、お前にわからないんなら意味がないだろ」
B「そんなことはない。真偽は結局主観的判断だよ。
それがたまたま君と僕の間で一致したからといって、
主観とは独立な客観の存在を考える必要はないだろ?」
0734132人目の素数さん
2005/10/02(日) 17:54:40まったく見当違い。
Bは、Aの真偽と証明に関する杓子定規な態度に対して、
その盲点をついてナンセンスさを指摘したまで。
しかしながらAは自分の主観性と向き合うことを恐れて
ナンセンスさを認めるに至っていない。
0735132人目の素数さん
2005/10/02(日) 17:56:46スタートすればいいのだ
普通(素人)の言葉では「客観」とはルールに則って、という意味
なのだから、勝手な解釈で素人の発言を捻じ曲げるのを、止めれば
いい
それに普通(素人)の言葉の意味では、「主観>客観」も「客観>
主観」もどちらも出て来はしない。人が客観という言葉を使うとき
「客観>主観」と考えているという思い込みをしているようだが、
そんなのは「客観的=絶対的」という脳内等式でも持ってなければ
出て来ない。生憎、そういう基地外には数学版では出会えないから
出会いたければ、哲版に逝ったほうがいいw
0736132人目の素数さん
2005/10/02(日) 18:01:12>チーマー=形式数学者
>ギャング=普通数学者
実際には、哲厨は「見かけはオヤジだが、実は元暴走族のヘッド」
だったりする(w
0737132人目の素数さん
2005/10/02(日) 18:03:01A 俺が”旨い”といったとき、これは真偽とは無関係だ
B なぜ?君が旨いと思って”旨い”といったなら、それは真実だろう
A その場合は「旨いと思っている」ということが真実だ。「旨い」と
いうのは真偽判定の対象でないことに変わりはないよ。
「旨い」という言葉と「旨いと思っている」という言葉は別物。君は
すぐに勝手な言い替えをする。因みに、「旨いと言った」というのも
ある。全て、別物だが。
0738132人目の素数さん
2005/10/02(日) 18:03:49君は普通という言葉で強制をしてるね。
それは捻じ曲げだから止めればいい。
素人の普通は大抵間違ってる。
なぜなら考えてないから。
自分のスカスカな脳味噌の中が全てだと思ってる。
0739132人目の素数さん
2005/10/02(日) 18:05:582.旨いと思う
3.旨いと言った
1は論外。2は旨いと思っていれば真実、思っていなければ嘘。
3は言ったのなら真実、言わなかったのなら嘘。当たり前だが。
0740132人目の素数さん
2005/10/02(日) 18:08:53じゃあ、どうぞ、どうぞ。貴方の普通(哲学)の客観を
説明したらいい。
0741132人目の素数さん
2005/10/02(日) 18:12:50ようです。
哲学さんの世界は、素人くんの世界と違って奥が深いのです
0742132人目の素数さん
2005/10/02(日) 18:15:242.も〜、駄目、死んじゃうって感じたの
3.も〜、駄目、死んじゃう、なんて叫んじゃった
全て別物ですw
0743132人目の素数さん
2005/10/02(日) 18:18:052.答えはAだと思う
3.答えはAだと言った
全て別物だけど…
0744132人目の素数さん
2005/10/02(日) 18:27:55早く。哲学(普通)の客観の意味と、それが存在しないことを
教えてー!興味津々なのー。それが分かったら、私も一人前に
なれる気がするわ。
0746132人目の素数さん
2005/10/02(日) 18:36:07待ちきれないよー
0747132人目の素数さん
2005/10/02(日) 18:40:52予告
次回は、ギャングに復讐を誓ったオヤジが
昔の暴走族(哲厨)仲間を集めるために、
お郷(哲版)に帰るシーンからになります。
0748132人目の素数さん
2005/10/02(日) 18:49:10哲版から仲間を集めてるんだ、待っててやれ。
それでも我慢できないなら、オヤジと一緒に
哲版まで逝ってきなさい。いろいろ、教えて
くれるよ、きっと。それに、皆に気に入られ
れば君も鉄柱仲間に入れてもらえるかも知れ
ないぞ!
0749132人目の素数さん
2005/10/02(日) 18:57:572.鳥を思う
3.鳥を見た
4.鳥と言う
全て違うな…
0750132人目の素数さん
2005/10/02(日) 19:03:52こっちの方が、鉄柱的には食いつきがいいのでは?
普通数学
3(客体)、9(客体)3×3(客体)
3×3=9(客体に関する解釈)
形式数学
3×3=9(客体)証明図A(客体)
Aは3×3=9の証明図である(客体に関する解釈)
0751132人目の素数さん
2005/10/02(日) 19:14:57生半可な鉄柱では太刀打ちできないね。
0752132人目の素数さん
2005/10/02(日) 19:16:01生半可な鉄柱では、太刀打ちできない。
0753132人目の素数さん
2005/10/02(日) 19:44:15Rod Downey
Victoria University, Wellington, New Zeeland
Itay Neeman
University of California, Los Angeles, USA
Michael Rathjen
The Ohio State University, Columbus, USA
Thomas Scanlon
University of California, Berkeley, USA
Simon Thomas
Rutgers University, New Brunswick, USA
0754132人目の素数さん
2005/10/02(日) 19:45:10大学が
0755132人目の素数さん
2005/10/02(日) 20:26:29証明図「A」(客体)は、真偽判定の対象ではない。
「Aは証明図である」(客体に関する解釈)は真偽
判定の対象だ。
「君」という物体(客体)、「旨い」という文字、
音声、或いは‘感覚’(客体)のいずれも真偽判定
対象外だな。
「君は旨いと感じている」、「君は旨いと言った」
(客体に関する解釈)は真偽判定対象だ。
0756ニートドラゴン ◆Ylfrus2v8U
2005/10/02(日) 20:34:38次スレは絶対に哲学板でやってくれ。
立てたら荒らす。
0757132人目の素数さん
2005/10/02(日) 20:36:39基地外5.「客体」と「客体に関する主体の解釈」の区別が
できない。
>>755 &
>A 俺が”旨い”といったとき、これは真偽とは無関係だ
>B なぜ?君が旨いと思って”旨い”といったなら、それは真実だろう
>A その場合は「旨いと思っている」ということが真実だ。「旨い」と
> いうのは真偽判定の対象でないことに変わりはないよ。
旨いという「感覚」(あるいは音声、文字etc.)は客体だ。
客体に対する主体の解釈ではない。感覚と解釈の区別ができ
ないのかい?
人間の発言行為の多くは、解釈の表現ではないのだ。感覚の
表現。この「多く」のという発言自体がな
ここら辺りで食い付いて来てね!
0758132人目の素数さん
2005/10/02(日) 20:42:360759132人目の素数さん
2005/10/02(日) 20:45:09次スレは
http://news18.2ch.net/test/read.cgi/scienceplus/1127852677/
でいいだろw
0760132人目の素数さん
2005/10/02(日) 20:47:38早く帰って来て、熱弁を振るってくれ!
0761132人目の素数さん
2005/10/02(日) 20:56:32お前が哲厨に見えるんだが
0762132人目の素数さん
2005/10/02(日) 21:00:09俺は普通数学屋だよ。数学版にまで来てくれた鉄柱と
心の触れ合いを楽しむために、彼と同類の振る舞いを
しているんだ。コミュニケーションしよう
0763132人目の素数さん
2005/10/02(日) 21:01:330764132人目の素数さん
2005/10/02(日) 21:02:46グッド! >夫馬でした
0765132人目の素数さん
2005/10/02(日) 21:24:34「お前らは形式化されたものこそ正しいと思っている!
お前らは形式化されたものこそ論理だと思っている!
だがそれは間違いだ!
お前ら形式化マンセー野郎共の認識を俺様が改めてやる!」
という決意に燃えて啓蒙活動に励む人が現れます。
「スレ違い」「話題を無理矢理そっちに持っていくな」「脳内敵とのバトルはよそでやれ」
などと注意しても、>>664-677みたいに脊髄反射で悪態をついて、しつこくスレに居座り続けようとします。
0766132人目の素数さん
2005/10/02(日) 21:27:32>>757 のネタ
> 言語と行為
> J.L.オースティン (著), 坂本 百大 (翻訳)
0767132人目の素数さん
2005/10/02(日) 21:28:56>名指しと必然性―様相の形而上学と心身問題
>ソール・A.クリプキ (著), 八木沢 敬 (翻訳), 野家 啓一 (翻訳)
0768132人目の素数さん
2005/10/02(日) 21:33:55>ウィトゲンシュタインのパラドックス―規則・私的言語・他人の心
>ソール・A.クリプキ (著), 黒崎 宏 (翻訳)
0769132人目の素数さん
2005/10/02(日) 21:39:04知ってる数学が非常に特殊なんだよね
基礎論関係か、あとは高校レベルか
計数工学科の学部生ほどの知識があれば
彼らの中では物凄い博学、ということになるんだろうけどw
0770132人目の素数さん
2005/10/02(日) 21:41:31佐々木力だ(禿
じゃなくて(藁
>夫馬でした。
0771132人目の素数さん
2005/10/02(日) 21:49:05> K・ポパー (翻訳), 小河原 誠 (翻訳), 蔭山 泰之
0772132人目の素数さん
2005/10/02(日) 21:52:20読んだんですが、無駄でした。」って結構、受けてたな
俺はイマイチついていけなかったよ >夫馬でした
0773132人目の素数さん
2005/10/02(日) 21:54:270774132人目の素数さん
2005/10/02(日) 21:56:42ICMの総合講演でも、これを期待されているらしいよ
早く来ないかな、鉄柱…
0775132人目の素数さん
2005/10/02(日) 22:09:46いや、鉄柱は「数学の哲学」の人ではない。俺が
ネタに使ったのは、その分野の基礎文献だから。
それも見抜けてない
0776132人目の素数さん
2005/10/02(日) 22:14:57数学の哲学に関して少し本を読んだのも、
ずっと昔のことで、あんまり良く覚えて
ないんだがな 夫馬
0777132人目の素数さん
2005/10/02(日) 22:15:510778132人目の素数さん
2005/10/02(日) 22:52:08ラッキー
0779132人目の素数さん
2005/10/03(月) 07:14:46早く、哲学的な「客観」という言葉の意味を説明してくれよ。
0780132人目の素数さん
2005/10/03(月) 07:15:47あいつ、駄目だろ。「数学の哲学」の初歩も知らないんだから
0781132人目の素数さん
2005/10/03(月) 08:03:12夫馬って、黒木のスレで暴れてる奴だろw
http://science4.2ch.net/test/read.cgi/math/1106568412/
0782132人目の素数さん
2005/10/03(月) 08:14:52わざわざ黒木の掲示板にまで出張したりするようだ…
0783132人目の素数さん
2005/10/03(月) 09:18:26とか、かならずしもそう言えないとかとあったけど。そう言えないといった人
に聞きたいんだけど、書き換えることが出来ない数学の推論って例えばどんな
ものがあるんだろう? 数学の(正しくかつ広く認められた)証明の推論というのは
単純かつ明らかな推論の積み重ねだと思うんだけど。
0784Euclid.Anal.Expert ◆wRpISOr80k
2005/10/03(月) 10:13:06俺の場合はそういうのがしっくりくる。数列の性質の証明問題なんかはどっちかといえば苦手だ。
0785132人目の素数さん
2005/10/03(月) 10:23:31幾何学的って言っても高次元幾何だと直感はあてにならないんで、
厳密に論理に従うしかないんじゃないの?
0786132人目の素数さん
2005/10/03(月) 10:24:25の適切にが今の所マジックワードで
残ってるから、まずはそこを何とか
せねば
実は、真であるにも関わらず普通の意味で証明できない命題があるかという段階で
証明がマジックワードになっているんだけどね
0787Euclid.Anal.Expert ◆wRpISOr80k
2005/10/03(月) 10:25:28すごく簡単にいえば、命題にとって必要十分になる全ての場合を数え上げて表にでもできるなら完全証明。
それができそうにないなら、完全証明は難しいってことだろ。
πにまつわるエトセトラが一番わかりやすい例かも。
0788132人目の素数さん
2005/10/03(月) 10:47:16出来ない証明=不十分
と定義をすれば、十分な証明は適切な形式証明に書き換えることが
できる。
ところで、形式証明には「厳密」と「厳密でない」の区別がない。
0789132人目の素数さん
2005/10/03(月) 10:57:05当たり前というか、無意味。AはAであると言ってるのと同じ
0790132人目の素数さん
2005/10/03(月) 11:00:34>πにまつわるエトセトラが
そのエトセトラの1つを具体的に上げてみてくれないか。
なるべく簡単な例を
0791132人目の素数さん
2005/10/03(月) 11:11:48なら、定義じゃなくても、「性質」としては認める?
最初の問題はこれを認めるか、認めないかの価値観の
問題。
0792132人目の素数さん
2005/10/03(月) 11:13:540793132人目の素数さん
2005/10/03(月) 11:16:35「十分」、「適切」が双方ともに感覚の問題だからな。
近いけれどもちょっと違う、というのが本音。
0794132人目の素数さん
2005/10/03(月) 11:19:05中には 全然、違う! とか言う奴もいるかもなwww
0795132人目の素数さん
2005/10/03(月) 12:29:46だけど先生が言うんですよ、「俺は赤チャを薦めるぞ」って
もうアフォかとバカかと俺は偏差値30なんだと、あんなもんわからないと、
だから先生に言ってやったんです。「買ってみたんですけど全然わかりません」
そしたら先生が「アフォか!あの程度もわからないのか、じゃ黒大数やれよ」
それで僕は先生のいうとおり黒大数を買ったのです。
「すいません、黒大数も全然わからなかったんですけど・・・」
「はぁ?お前はどうしたいわけ?俺を困らせたいのか?それ以前にお前はたぶんで物を語るな!!だからお前は彼女に振られるんだよ!!」
それでついに僕は切れたんです
「ってかテメー俺は糞バカだって知ってるだろ!!偏差値30、わかる?30だよ30!
数学の偏差値30って言ったら哲学科のレベルだぞ!哲学科レベルの奴があんなもんできるわけねーだろ!!」
その後に少し沈黙があって、
「・・・そんな言葉口にしちゃいけない、やつらはいくら頑張っても数学は出来るようにならないんだ、お前はまだ可能性があるけどな」
「先生すいません。つい」
「いいんだ。ただしこれからは“哲学科”と“数学”の関係を口にしてはいけない、これは差別用語だからなわかったか?」
「はい」
0797132人目の素数さん
2005/10/03(月) 14:44:08http://academy4.2ch.net/test/read.cgi/philo/1099864239/479-488
0798132人目の素数さん
2005/10/03(月) 15:49:10>感覚と解釈の区別ができないのかい?
主体と客体の区別をしちゃうのかい?(w
オースティンのチンカスは旨いかい(w
0799132人目の素数さん
2005/10/03(月) 15:53:52ヴィトゲンシュタインは哲学書を読まないことで有名だった。
0800132人目の素数さん
2005/10/03(月) 16:05:23知ってるのは算数だけだ(w
しかし全て算数で書ける、とゲーデルはいっている(w
(いや、本当はゲーデルはそうはおもってなかったんだが
クリプキともう一人の人がそれを示しちゃったんで
ゲーデルは心底驚き呆れたらしい)
0801132人目の素数さん
2005/10/03(月) 16:58:41それはポパー?
0802132人目の素数さん
2005/10/03(月) 17:06:10総合司会をさせて頂く事になりました。
さてっ、皆様お待ちかねの鉄柱が帰って来ました!
まずは、哲学的な客観の意味の説明が始まります。
我々に、どんな熱弁をふるってくれるのでしょう。
わくわく、わくわくw
0803132人目の素数さん
2005/10/03(月) 20:53:340804132人目の素数さん
2005/10/03(月) 20:58:550805132人目の素数さん
2005/10/03(月) 23:07:29ジョルダンでしょう
0806132人目の素数さん
2005/10/03(月) 23:09:56>全て算数で書ける
なんのこと?これじゃ良く意味が分からないんだが?
ブール・エルだっけ?
0807132人目の素数さん
2005/10/05(水) 14:16:20ショボン
0808132人目の素数さん
2005/10/05(水) 14:16:570809132人目の素数さん
2005/10/05(水) 14:28:540810132人目の素数さん
2005/10/05(水) 14:53:280811132人目の素数さん
2005/10/05(水) 15:50:48プール・エルだ。
0812132人目の素数さん
2005/10/05(水) 15:58:14ttp://www.geocities.jp/enten_eller1120/postmodern/witt.html
0813132人目の素数さん
2005/10/05(水) 16:32:070814132人目の素数さん
2005/10/05(水) 17:27:36>アスペクトというのは,別のアスペクトが
>ありうる場合にのみあるものなのである.
客観という言葉をどう捉えるているか?
私はこう捉えているということは、別の
捉え方もあることを知っているからだ。
0815132人目の素数さん
2005/10/05(水) 17:31:060816132人目の素数さん
2005/10/05(水) 17:33:180817132人目の素数さん
2005/10/05(水) 17:36:150818132人目の素数さん
2005/10/05(水) 17:54:160819132人目の素数さん
2005/10/05(水) 18:08:38意味は
ピューマにたべられた馬ですか
0820132人目の素数さん
2005/10/05(水) 18:18:20↓無職の引き篭もりのキモヲタの精神障害者フマ
〜∞
/⌒⌒ ̄ ̄ ̄\ 〜∞
/ \ 〜〜〜〜〜
| ____丿ノノ.__| つ〜ん
| /U ._) ._) プゥ〜ん
| | ( 〜〜〜
| ノ(6 ∵ ( 。。) ) _______
U ) 3 .ノ / ________
/ \ ヽ ,,_ U ___,,ノ / /
\,,______,ノ \/ / _____
./ / /|
.. ./ / ./ .|
「殺人的ブスいないかなぁ?僕ちゃんブス大好き☆」
0821132人目の素数さん
2005/10/05(水) 23:25:030822132人目の素数さん
2005/10/06(木) 11:51:30>「コンピューターは規則に従い損ねない」と言ったが,
>これは,コンピュータに「アスペクト」がないからである.
つまり、ここの自称素人のいう客観は
実は「アスペクト盲」の状態なのであり
「アスペクト」の違いが問題となる場合
には何の意味も持たない。
0823132人目の素数さん
2005/10/06(木) 16:22:40まさに、それは「コンピュータ」って。
てな訳で「形式証明=客観」なんだよw
「アスペクト」の違いを問題にしない。
0824132人目の素数さん
2005/10/06(木) 16:23:26自称哲学君は何をやっていたんだい?
0825132人目の素数さん
2005/10/06(木) 16:26:16君も、あえて「アスペクト盲」である「コン
ピュータ」を使ったりするよね?
0826132人目の素数さん
2005/10/06(木) 16:29:21非アスペクト盲>アスペクト盲
どちらかの不等式が常に成り立つ訳ではないんだよ
時と場合によって、適切さは変わるのさ
ところで「客観がない」というときの客観の説明を
早くしてくれないかな?w
0827132人目の素数さん
2005/10/06(木) 16:43:20数学ではまともに話ができるkingの貴重さがよくわかる。
0828132人目の素数さん
2005/10/06(木) 16:45:05つまり、 King>>>>>>夫馬 って訳だw
0829GiantLeaves ◆6fN.Sojv5w
2005/10/06(木) 16:45:140830GiantLeaves ◆6fN.Sojv5w
2005/10/06(木) 16:45:460831132人目の素数さん
2005/10/06(木) 16:46:420832132人目の素数さん
2005/10/06(木) 16:47:290833GiantLeaves ◆6fN.Sojv5w
2005/10/06(木) 16:54:010834132人目の素数さん
2005/10/06(木) 16:57:09http://academy4.2ch.net/test/read.cgi/philo/1099864239/479-488
0835132人目の素数さん
2005/10/06(木) 17:16:27>> 実は「アスペクト盲」の状態なのであり
>まさに、それは「コンピュータ」って。
>てな訳で「形式証明=客観」なんだよw
>>825
>あえて「アスペクト盲」たる事を客観という。
「ボク、コンピュータ」の幼稚な発想に逃げ込んだか(w
> 君も、あえて「アスペクト盲」である
>「コンピュータ」を使ったりするよね?
しかし、君のように自分を機械だとおもう
馬鹿な真似はしないが(w
0836132人目の素数さん
2005/10/06(木) 17:21:53>アスペクト盲>非アスペクト盲
>非アスペクト盲>アスペクト盲
>どちらかの不等式が常に成り立つ訳ではないんだよ
>時と場合によって、適切さは変わるのさ
時と場合を全く明らかにできない君の言明は
まったく不適切なものだね。
>「客観がない」というときの客観の説明を
>早くしてくれないかな?w
肝心なことを忘れているな。
「コンピュータには「アスペクト」がない」
という言明の証明は?
0837132人目の素数さん
2005/10/06(木) 18:45:320838132人目の素数さん
2005/10/06(木) 19:14:15囲碁やるの?
0839132人目の素数さん
2005/10/06(木) 19:15:06かつ、そうであることを期待されています
早く客観の意味とその非存在を説明してくれよ(w
0840132人目の素数さん
2005/10/06(木) 19:17:41お前の力を見せ付けてやれ!
0841132人目の素数さん
2005/10/06(木) 19:43:42かつ、そうであることを期待されています
想定と期待の違いは?
0842132人目の素数さん
2005/10/06(木) 19:56:560843132人目の素数さん
2005/10/06(木) 19:57:450844132人目の素数さん
2005/10/06(木) 19:59:46http://academy4.2ch.net/test/read.cgi/philo/1099864239/479-488
0845132人目の素数さん
2005/10/06(木) 20:28:190846132人目の素数さん
2005/10/06(木) 20:28:560847132人目の素数さん
2005/10/06(木) 20:47:470848132人目の素数さん
2005/10/06(木) 21:03:590849132人目の素数さん
2005/10/07(金) 08:45:500850GiantLeaves ◆6fN.Sojv5w
2005/10/07(金) 08:55:030851132人目の素数さん
2005/10/07(金) 08:57:31哲学と数学
http://science4.2ch.net/test/read.cgi/math/1128612119/
1 :132人目の素数さん :2005/10/07(金) 00:21:59
哲厨隔離用ゴミ箱
0852132人目の素数さん
2005/10/07(金) 09:09:15>コンピュータは規則通りに動く、と想定されています
>かつ、そうであることを期待されています
それは主観だね。
期待や想定ぬきの証明を早く!早く!!早く!!!
できるといったじゃないか!!!君。
0853132人目の素数さん
2005/10/07(金) 09:12:09鉄柱がデムパなら、Kingはさしずめスカラー波(w
0854132人目の素数さん
2005/10/07(金) 09:13:01>「厳密性」に随分と拘るんだな。
素人って二重基準なんだな(w
0855132人目の素数さん
2005/10/07(金) 09:14:070856132人目の素数さん
2005/10/07(金) 09:17:16君の脳内等式1.「あ、うん」=「あ、うんと思う」
君の脳内等式2.「コンピュータ」=「コンピュータに対する期待」
0857132人目の素数さん
2005/10/07(金) 09:17:510858132人目の素数さん
2005/10/07(金) 09:20:21別物なんですけど…
0859132人目の素数さん
2005/10/07(金) 09:21:38なるほど、君は
命題P⇔命題Pが真
には反例があるというんだね?
どんな反例だい?いってごらん?ん?どうした?(w
0860132人目の素数さん
2005/10/07(金) 09:21:430861132人目の素数さん
2005/10/07(金) 09:22:58これは839の脳内の等式だろ(w
>>860も同様。
0862132人目の素数さん
2005/10/07(金) 09:24:05「あ、うんが真」=「あ、うんと思う」
「あ、うんが真」=「あ、うん」
0863132人目の素数さん
2005/10/07(金) 09:24:24どんどんぶっ壊れるねえ。君(w
じゃあ、聞くけど
「証明図で示せない証明」
って何なの?
0864132人目の素数さん
2005/10/07(金) 09:25:41君の間違い
「あ、うんが真」=「あ、うんが証明できる」
0865132人目の素数さん
2005/10/07(金) 09:26:43それとコンピュータ自体は別だな。
お前はバカだから、しょうがないよ
0866132人目の素数さん
2005/10/07(金) 09:28:48何にも分かってない。一から出直せ
0867132人目の素数さん
2005/10/07(金) 09:29:20>じゃ、コンピュータに対する期待が主観だからといって、
>それとコンピュータ自体は別だな。
そもそも「コンピュータ自体が存在する」という考えが主観だな。
どこまでいっても、主観抜きの客観はない。
バカの君は考えないからこのことに気づかない。
0868132人目の素数さん
2005/10/07(金) 09:29:500869132人目の素数さん
2005/10/07(金) 09:30:40脳内等式.「主観抜きの客観がない」=「客観がない」
0870132人目の素数さん
2005/10/07(金) 09:30:55そうか、ダメか君。
何も分かってない。ゼロから出直せ。
いいか、イチじゃないゼロだぞ。
イチがあると思ったから失敗したんだ。
ゼロからイチへのもっとも困難な壁を乗り越えろ
0871132人目の素数さん
2005/10/07(金) 09:31:45無駄だよ。おバカさんw
0872132人目の素数さん
2005/10/07(金) 09:32:380873132人目の素数さん
2005/10/07(金) 09:33:16引っかかったぜ!このバカが!
>>859を見ろ
>君の脳内等式1.「あ、うん」=「あ、うんと思う」
今お前は
「客観」=「オレが客観だと思う」
という等式をつかったんだぞ!(w
お前はお前自身を否定するのか?(w
0874132人目の素数さん
2005/10/07(金) 09:35:12頭の悪い君の脳内等式.「主観抜きの客観がない」=「客観がない」
0875132人目の素数さん
2005/10/07(金) 09:35:25でもどう違うか言えない。
なぜ言えないか?言ったら
「実は証明って主観なんだぜ」
と認めることになるから。
それは自分の首をかき切るから言えない。
図星だろ?(w
0876132人目の素数さん
2005/10/07(金) 09:36:230877132人目の素数さん
2005/10/07(金) 09:37:31「実は証明って主観なんだぜ」
え、そうだけど。これって、当たり前のことなんだけど
0878132人目の素数さん
2005/10/07(金) 09:38:07「証明図」(客観)
0879132人目の素数さん
2005/10/07(金) 09:38:15バカな君の脳内等式
「客観」=
「オレが客観だと思ってるが、
「オレが」とは思ってない」
0880132人目の素数さん
2005/10/07(金) 09:38:48認めるも何も、当たり前のことなんだが…
0881132人目の素数さん
2005/10/07(金) 09:39:30おやおや、都合が悪くなると寝返るんですね。
これから君を小早川クンと呼びましょう(w
0882132人目の素数さん
2005/10/07(金) 09:40:15「実は」は不自然だな。
『当たり前だが、証明は主観』
0883132人目の素数さん
2005/10/07(金) 09:40:56>「証明図」(客観)
ただの図とアスペクトが分離できると思うくらいバカな発想だ。
0884132人目の素数さん
2005/10/07(金) 09:42:50は?お前は勘違い。どうせ、数学のことを分かってない連中(底辺高校の
数学教師とか)が「証明は客観」とか言うの聞いて、数学者もそう思って
いるとか勘違いした訳だw
0885132人目の素数さん
2005/10/07(金) 09:45:12証明図があっても証明とは認めないよw
0886132人目の素数さん
2005/10/07(金) 09:46:210887132人目の素数さん
2005/10/07(金) 09:49:370888132人目の素数さん
2005/10/07(金) 09:50:170889132人目の素数さん
2005/10/07(金) 10:02:31当たり前過ぎて、改めて言うのも恥ずかしい。
0890132人目の素数さん
2005/10/07(金) 10:03:240891132人目の素数さん
2005/10/07(金) 10:55:04「平面を曲線の内と外に分けない閉曲線」
が発見される可能性はあったの?
0892132人目の素数さん
2005/10/07(金) 11:44:56これがわかるかわからないかで、数学できるかできないかが区別できるな。
毎日数学の問題解いてるやつなら、この意味はすぐにわかる。
0893132人目の素数さん
2005/10/07(金) 14:16:51で、その意味は?
あ、よく読めば、お前が「できる」側だとは一言も言ってないな、スマソ。
0894132人目の素数さん
2005/10/07(金) 14:43:58答え:採点の仕方が規則的(=客観的)という意味。
その結果による順位の評価(=価値観)が客観的と
いう意味ではありません。当たり前だがな
ところで、哲学的な客観の意味とその非存在を早く
説明してくれないかなあw
0895132人目の素数さん
2005/10/07(金) 14:45:21「機械的」の方がイイ感じだな
答え:採点の仕方が機械的(=客観的)という意味。
その結果による順位の評価(=価値観)が客観的と
いう意味ではありません。当たり前だがな
0896132人目の素数さん
2005/10/07(金) 14:46:30チュキ、チュキ、鉄〜柱♪
0897132人目の素数さん
2005/10/07(金) 14:53:31効率的に捌くには便利だ
0898132人目の素数さん
2005/10/07(金) 14:54:260899132人目の素数さん
2005/10/07(金) 15:19:50鉄柱の典型的特長
「意味」を尋ねたがる。
自分で証明問題を練習してみれば、すぐに気づくことなのに、努力はしない。
いいか、数学は、意味でわかるようになるものじゃない。
数学は知識や情報じゃない。
情報を扱う能力なのさ。アビリティ!アビリティ!
努力なしで理解することはできず、自ら証明問題を解くこともせず語ることもできん。
鉄柱、だらけた夢みてんなよ。
0900132人目の素数さん
2005/10/07(金) 15:56:24じゃあ主観てなんなの?という問いへの答えも主観的にならざるを得ない。
つまりこの世はオール主観!
問題は「Aさんの主観」と「Bさんの主観」が同値がどうかってことでしょう。
え、同値かどうかも主観で決まるって?そりゃないよ‥‥
0901132人目の素数さん
2005/10/07(金) 15:57:500902132人目の素数さん
2005/10/07(金) 16:00:51相変わらず、頭悪いな
主観的に「主観と客観」を区別する。主観的に「主観と客観」がある。
このことと「客観がある」ことが。何で矛盾するんだ?訳分からんw
0903132人目の素数さん
2005/10/07(金) 16:02:32そうしたら、「客観テスト」がなくなるのかよ?頭、わり〜w
0904132人目の素数さん
2005/10/07(金) 16:03:14すべての人間にとって遠くのものは小さく見えますよね。
では自分から遠ざかるほど物体は小さくなるか?っていうとそうでもない。
しかし主観オンリーなら上記は成り立つわけです。。。
0905132人目の素数さん
2005/10/07(金) 16:03:55「客観テスト」はなくなりませんよw
0906132人目の素数さん
2005/10/07(金) 16:06:44鉄柱の基地外等式.「小さい」=「小さく見える」
結局、こればっかw
0907132人目の素数さん
2005/10/07(金) 16:07:02やはり、哲厨。
オタの悲しさか。
0908132人目の素数さん
2005/10/07(金) 16:08:530909132人目の素数さん
2005/10/07(金) 16:09:55説明してくれないかなあw
0910132人目の素数さん
2005/10/07(金) 16:13:07何を揉めているのかわからん。
0911132人目の素数さん
2005/10/07(金) 16:19:32バカな鉄ヲタの脳内等式.「証明」=「証明図」
鉄ヲタの推論 →
「証明」は主観。だから「証明図」も主観www
0912132人目の素数さん
2005/10/07(金) 16:20:59効率的に捌くには便利だ
0913132人目の素数さん
2005/10/07(金) 16:22:450914132人目の素数さん
2005/10/07(金) 16:25:52鉄柱は厳密性に拘りますwww
0915132人目の素数さん
2005/10/07(金) 16:28:39ってのは誰の価値観なんだ。>>25でも一度書いたが、「厳密さは時代の関数」と言った
偉い数学者がいたと思ったよ。
0916132人目の素数さん
2005/10/07(金) 16:46:13客観テストは受験生を効率的に捌くのに便利です! by 大手私大w
0917132人目の素数さん
2005/10/07(金) 16:47:34> ってのは誰の価値観なんだ
答え:大手私大
0918132人目の素数さん
2005/10/07(金) 16:48:56マクドのマニュアルと同じ価値観だ!
0919132人目の素数さん
2005/10/07(金) 16:48:56そりゃせいぜい創造性をまったく評価されないような人間を
おおざっぱに扱うのに効率がよいという程度の二次的な価値じゃないか。
大手私大だって創造性の高い生徒を育てることができるという評判が立てば
評価が上がるとおもわれるよ。
0920132人目の素数さん
2005/10/07(金) 16:51:47財務上、効率性は非常に高い価値があります by 大手私大&マクド
0921132人目の素数さん
2005/10/07(金) 16:54:15そりゃそうだが、同時にイノベーションを続け、陳腐化しないような
付加価値を付け加え続けなければ競争には勝てないのであって。
0922132人目の素数さん
2005/10/07(金) 16:56:14だから、人材を区切って使い分けています。
0923132人目の素数さん
2005/10/07(金) 16:57:42それと数学とにどういう関係が?
0924132人目の素数さん
2005/10/07(金) 16:58:58私大は受験料収入&入学金(すべり止め確保用)が
重要な収入源だからねw
0925132人目の素数さん
2005/10/07(金) 17:00:43私大経営や受験産業とは大いに関係します。
0926132人目の素数さん
2005/10/07(金) 17:02:250927132人目の素数さん
2005/10/07(金) 17:04:07鉄柱の勘違い.数学=客観=敵
正しくは、「私大経営&受験産業=客観=敵」
客観性を攻撃するなら学歴版の方が相応しいぞ
0928132人目の素数さん
2005/10/07(金) 17:04:550929132人目の素数さん
2005/10/07(金) 22:18:14大学入試で証明問題が客観テストになり
まつ
0930132人目の素数さん
2005/10/07(金) 22:18:560931132人目の素数さん
2005/10/08(土) 00:25:51計算ミスは自動的に零点かw
0932132人目の素数さん
2005/10/08(土) 01:17:54それこそが客観的
By大手私大
0933132人目の素数さん
2005/10/08(土) 06:11:21自分で証明問題を解けばすぐわかること。
0934132人目の素数さん
2005/10/08(土) 07:18:010935132人目の素数さん
2005/10/09(日) 15:56:35ここで、連続というだけであるからとても難しい。
長さが定義できないような連続曲線だとか、任意の点のどれだけでも
近いそばを通る曲線だとか、とても絵に書けないようなものでも、
それが連続曲線に含まれている以上は扱われていなければならない。
0936132人目の素数さん
2005/10/09(日) 19:09:30(2)数学は約一名の哲厨の考える意味では厳密でない
約一名の哲厨も含めて、このスレの大半の人は(1)も(2)も認めてる。
そして、「このスレの大半の人は(1)も(2)も認めてる」という事を
1. このスレの大半の人は認めていて、
2. 約一名の哲厨は認めていない、
という構図。
脳内に仮想敵を作って
「君らは俺の考える意味で数学が厳密じゃない事を理解できないバカ(w」
とか言って仮想敵を煽られても、妄想乙としか言いようがないな。
0937132人目の素数さん
2005/10/09(日) 22:03:59そして、√4が有理数である証明を書け。
中学生でもできる。
次に、√2が有理数ではない証明をしてみろ。
その仮定で、証明とは何か、数学的帰納法がなぜ必要か、そして完全証明とは何なのかがわかる。
自分で頭を動かさずに、想いだけ飛ばしてるのが鉄柱。
だからオナニーなんだよ。カスが。
0938132人目の素数さん
2005/10/09(日) 23:48:36http://science4.2ch.net/test/read.cgi/math/1128822537
0939132人目の素数さん
2005/10/10(月) 08:46:52豆知識: 任意の a<1 に対して, [0,1]×[0,1]内のジョルダン閉曲線で,
そのルベーグ測度が a 以上なものが存在する.
>>936
非常に分かりやすい解説をありがとう. おまいアタマいいな.
0940132人目の素数さん
2005/10/10(月) 10:10:39だからオナニーなんだよ。カスが
0941132人目の素数さん
2005/10/11(火) 08:33:271)数学屋のいう「厳密性」が「形式的に証明できていること」を指すなら
数学の証明は、形式的な証明になっているとは限らない点で厳密でない。
また「数学の証明は、必ず形式的な証明になる」という数学屋の
考えは何の根拠もない点で、まったく厳密性がない。
2)また「形式的に証明できていること」が「数学として正しいこと」と
考えているなら、それもまた間違っている。
つまり数学屋のいう厳密性は、全く達成されていない上に
そもそもその達成が本来の目的とは異なる点で、二重に
無意味である。
0942132人目の素数さん
2005/10/11(火) 08:36:04実は数学者は一人もいない(w
0943132人目の素数さん
2005/10/11(火) 09:33:21指しません
> 数学の証明は、形式的な証明になっているとは限らない
限らない、ではなく、そもそも違うもの
> 数学の証明は、必ず形式的な証明になる
これはただの感想、価値観の表現。数学者でも人によって
感じ方、価値観は異なる。こう感じてない方が多いと思う。
> 「形式的に証明できていること」が「数学として正しい
> こと」と考えている
考えてない
0944132人目の素数さん
2005/10/11(火) 09:45:02鉄柱はことごとく勘違いから出発している訳だなあ。
形式証明=客観
ある証明の厳密さ=主観
ある形式証明の適切さ=主観
そもそも、「証明(普通の)」と「証明図(形式証明)」は
別物です。鉄柱さんはそこから、お勉強しなおしましょうね
------
客観テストの採点方法=客観的(機械的)
客観テストの問題の答え=主観的
これを混同している訳だ。形式証明は客観的
(客観テストの採点方法のように)であるが、
その適切さは主観的(問題の答えのように)。
適切さが主観的だからと言って、前者の客観
性が消える訳じゃない。
0945132人目の素数さん
2005/10/11(火) 11:18:41>> 数学屋のいう「厳密性」が「形式的に証明できていること」を指すなら
>指しません
では、何を指す?
>> 「形式的に証明できていること」が「数学として正しいこと」と考えている
>考えてない
では、どう考える?
否定だけでは答えにならない。
0946132人目の素数さん
2005/10/11(火) 11:21:18>形式証明=客観
>客観テストの採点方法=客観的(機械的)
そもそも客観的=機械的とかいうのが馬鹿。
鉄柱嫌いは勉強できないだろ?
だからこういう勘違いをする
まず機械的=客観的という嘘を否定することから勉強しろ
0947132人目の素数さん
2005/10/11(火) 11:23:22それはお前が勝手にそう思っているだけだ。
お前がいくらわめいたところで、客観が存在するわけではない。
0948132人目の素数さん
2005/10/11(火) 11:31:54ははは?じゃあ、君の言う客観の意味と
その非存在を早く説明してくれよ
大事なのは君は非存在を主張してること
だぜ。分かってる?
0949132人目の素数さん
2005/10/11(火) 11:34:22>客観的(客観テストの採点方法のように)で
これは、「普通の客観の意味」を君に説明して上げたの。
で「君の言う客観」って何だい?
0950132人目の素数さん
2005/10/11(火) 11:39:44紅色との違いは?説明することは不可能ではない
かもしれないが、感覚とその説明には必ず乖離が
生じるのさ。証明は主観であり、感覚だから仕方
ないよなあ。
非存在の主張は大変だねw
0951132人目の素数さん
2005/10/11(火) 11:43:37それに対して、証明図は客観なの
0952132人目の素数さん
2005/10/11(火) 11:44:420953132人目の素数さん
2005/10/11(火) 11:50:42対して非存在は説明しなきゃいけない。分かってる?
赤の存在は説明しなくても、赤を提示すればいいの。
0954132人目の素数さん
2005/10/11(火) 11:50:55はあ?何いってんだお前?
数学的帰納法による証明すらまともにできんくせに。
0955132人目の素数さん
2005/10/11(火) 11:53:07それと数学の証明は同じなのさ。なぜなら、証明は感覚の問題だからだよ。
0956132人目の素数さん
2005/10/11(火) 11:54:50だからと言って、赤がない訳じゃないんだよ
0957132人目の素数さん
2005/10/11(火) 11:57:52ぜんぜん違う。
フェルマーの定理について概説した本をかいた女哲学者と同じ間違いを犯してる。
翻訳は数学がわかる訳者にたいそう叩かれてた。
間違いだらけだとな。
0958132人目の素数さん
2005/10/11(火) 11:58:11君には数学の「証明」が見えないだけ
もう仕方がないから、代わりに「証明図」でも
見てなさい
0959132人目の素数さん
2005/10/11(火) 12:01:24今の君と同じ症状だね。
それとも何かい?君は数学が分かってるのに証明の意味が
分からないとでも
0960132人目の素数さん
2005/10/11(火) 12:04:51独学ではなく、正規の教育を受ける人間は、専門以前にリベラル・アーツの段階で、そのような間違いを犯さない手法を身につける。
ところが鉄柱はそうではない。
おおよそ、このスレでおきているような、くだらないいい争いは、その学習の段差によって生まれているコミュニケーションの問題にすぎない。
0961132人目の素数さん
2005/10/11(火) 12:06:34数学者でも専門が違えば、見えない方が普通だよ。
0962132人目の素数さん
2005/10/11(火) 12:09:38ほとどいないねえ。
0963132人目の素数さん
2005/10/11(火) 12:12:55ふーん、バグ取りをコンピュータがやってくれんのか。便利だな。
VC10ぐらいには搭載されるかなあ。
0964132人目の素数さん
2005/10/11(火) 12:40:120965132人目の素数さん
2005/10/11(火) 17:10:02実際に混乱しているのは、鉄柱ではなく鉄柱嫌いのほう。
彼は自分の混乱を、メタ言語のせいにしているが、それは間違っている。
実際には鉄柱嫌いは、高等教育を受けたことがないと見た
(つまり大学にいったことがない)
正規の教育=リベラル・アーツなんて平気で口にするのは
大学に一切いったことがなくネットで四苦八苦しながら
独学してる奴だけ。
0966132人目の素数さん
2005/10/11(火) 17:11:100967132人目の素数さん
2005/10/11(火) 17:11:440968132人目の素数さん
2005/10/11(火) 17:11:49>独学してる奴だけ。
えらいよねそんなことできるなら
0969132人目の素数さん
2005/10/11(火) 17:12:36> えらいよねそんなことできるなら
はずかしいね嘘を本当だと思い込む馬鹿なんて
0970132人目の素数さん
2005/10/11(火) 17:14:38はずかしいね反射的に書き込む馬鹿なんて
0971132人目の素数さん
2005/10/11(火) 17:15:25>はずかしいね反射的に書き込む馬鹿なんて
はずかしいね反射的に書き込んだ馬鹿の君(w
0972132人目の素数さん
2005/10/11(火) 17:16:33哲学は客商売なんだぞ
主観なんてゴミとおんなじだ
0973132人目の素数さん
2005/10/11(火) 17:17:48>はずかしいね反射的に書き込む馬鹿なんて
はずかしいね反射的に書き込んだ馬鹿の君(w
あのね教えてやろうか
どんどん書き込んでこんな目障りなのをどっかに
やりたいだけなの
0974132人目の素数さん
2005/10/11(火) 17:17:57一番恥ずかしいのは、
「主観はゴミ」という主観的主張を
行う反哲学的宗教家
哲学的懐疑を嫌うのは宗教的狂信
0975132人目の素数さん
2005/10/11(火) 17:18:330976132人目の素数さん
2005/10/11(火) 17:19:18君ももうすぐ死ねる
0977132人目の素数さん
2005/10/11(火) 17:19:29恥ずかしいというこころだ
な
いいか
0978132人目の素数さん
2005/10/11(火) 17:19:53君の望みだろ?
0979132人目の素数さん
2005/10/11(火) 17:20:250980132人目の素数さん
2005/10/11(火) 17:20:26どんどん書き込め
0981132人目の素数さん
2005/10/11(火) 17:20:560982132人目の素数さん
2005/10/11(火) 17:21:040983132人目の素数さん
2005/10/11(火) 17:21:560984132人目の素数さん
2005/10/11(火) 17:22:20なぜなら、体験とは意識あってのことだからだ。
0985132人目の素数さん
2005/10/11(火) 17:23:26はい次
0986132人目の素数さん
2005/10/11(火) 17:23:280987132人目の素数さん
2005/10/11(火) 17:23:59次は?
0988132人目の素数さん
2005/10/11(火) 17:24:260989132人目の素数さん
2005/10/11(火) 17:25:030990132人目の素数さん
2005/10/11(火) 17:25:480991132人目の素数さん
2005/10/11(火) 17:25:51数ヲタにとって大事なのは、主観の方(=証明)なんだが…
0992132人目の素数さん
2005/10/11(火) 17:26:140993132人目の素数さん
2005/10/11(火) 17:26:50なんて言ってないでほら書き込め
0994132人目の素数さん
2005/10/11(火) 17:26:57数ヲタにとって真に大事なのは自分。
0995132人目の素数さん
2005/10/11(火) 17:27:440996132人目の素数さん
2005/10/11(火) 17:27:48代替物として、「証明図」(客観)があるんだよ
0997132人目の素数さん
2005/10/11(火) 17:28:290998132人目の素数さん
2005/10/11(火) 17:31:480999132人目の素数さん
2005/10/11(火) 17:32:261000132人目の素数さん
2005/10/11(火) 17:33:2610011001
Over 1000Threadもう書けないので、新しいスレッドを立ててくださいです。。。
レス数が1000を超えています。これ以上書き込みはできません。