1 :
132人目の素数さん :
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
「私達が始めて完全証明した」とはおこがましい ヘボい企業の人が営業で言いそうな台詞だ。
3 :
132人目の素数さん :2005/09/28(水) 02:27:12
コムのチェック機能かぅ
4 :
132人目の素数さん :2005/09/28(水) 02:47:44
プルーフチェッカーのデモの一つとして、曲線定理をやってみただけでは?
5 :
132人目の素数さん :2005/09/28(水) 02:49:57
今井数学的だな
6 :
132人目の素数さん :2005/09/28(水) 02:56:29
ニュー速よか盛り上がりが低い、ってのもねえ。
8 :
132人目の素数さん :2005/09/28(水) 03:00:57
その20万行を全部見ないことには何とも もっともそんなの見る気にもならんが
20万行… 証明の長さ的にもギネス級でわ?
12 :
132人目の素数さん :2005/09/28(水) 07:55:41
20万行… ごジョルダンでしょ?
>>10 公理からダイレクトに出してない,くらいの意味だとおも
14 :
132人目の素数さん :2005/09/28(水) 09:11:46
これは下手をすると 「数学者は役たたず.自分の縄張りの問題も解決できない やっぱり工学は偉い」 みたいなレトリックに転嫁されそうですね 数学プロパのみなさん 曲線定理の経緯とこの信州大の人の仕事の意義を 詳しく説明してください
・ この信州大の人の仕事の意義
4 名前: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 公理からダイレクトに出してない,くらいの意味だとおも
16 :
132人目の素数さん :2005/09/28(水) 09:58:42
>>15 もうちょっとツッコんだ分析をお願いします
17 :
132人目の素数さん :2005/09/28(水) 10:25:48
ミザール言語というのを、証明を記述する方式としてアピール できたのが最大の成果ではないかな。ミザール言語からTeXへ、 TeXからミザール言語へ変換するようなスクリプトやエディタ があると、今後は普及していくかも知らん。
18 :
132人目の素数さん :2005/09/28(水) 10:33:41
プルーフチェッカーによる証明のチェックが初めて出来た、ということ 出来てない、というか、してない有名定理は五萬とある訳で プルーフチェックが今後、簡便化されていけば、将来的に実用もあるん じゃないかねえ?自分で書いた証明をチェッカーに掛けて検証するとか
19 :
132人目の素数さん :2005/09/28(水) 10:52:22
将来的には本当の未解決問題に 自動証明を応用することはありえるのでしょうか?
20 :
132人目の素数さん :2005/09/28(水) 10:56:33
>>19 当分はないんじゃない?これは既にある証明の構文チェックをするものなので、
証明をするのとは次元が違うとおもわれ。教科書の証明をどんどんミザール言語に
翻訳したり、ライブラリを作ったりするのが今後の発展方向では?
21 :
132人目の素数さん :2005/09/28(水) 10:58:08
将棋とかチェスのプログラムみたいな方法論で 未解決問題を証明することはできないでしょうか?
22 :
のりお :2005/09/28(水) 11:11:20
「完全証明」って、じゃあ俺の知ってる証明はなんなんだ?
23 :
132人目の素数さん :2005/09/28(水) 11:12:22
>>21 既に自動証明と言うジャンルはある。任意の命題を一階述語論理の範囲で
真か偽か判定するものなので、その過程は証明であると言えば言える。
しかしその種のプログラムは一般に、有限時間の範囲で真または偽という
判定がでるとは限らない。囲碁や将棋では、この手は損だと思ったら
適当な基準で考えるのを止めていいんだが、証明はそうでないという
点が最も異なる。とはいえ未解決問題や証明のギャップを、有限時間
考えてみるというプログラムが登場してくる可能性はありうる。
それだって、(ミザール言語による)数式のライブラリがある程度
充実していないとなかなか機能しないと考えられるが。
24 :
132人目の素数さん :2005/09/28(水) 11:16:27
25 :
132人目の素数さん :2005/09/28(水) 11:23:36
26 :
132人目の素数さん :2005/09/28(水) 11:27:43
289 :132人目の素数さん :2005/09/28(水) 11:18:08
>>287 黒木のように、直観力がなく、客観に頼ろうとする人間には
数学は無理だったんだよ。結局
27 :
132人目の素数さん :2005/09/28(水) 11:32:48
その前に(何の前かはおいといて)、ジョルダンの曲線定理のまともな証明 が載ってる本教えて。なるべく手に入りやすいのが有難い
>>27 Jordan, Cours d'Analyze de l'Ecole Polytechnique (1887)
クゼ・コスニオフスキ トポロジー入門
30 :
132人目の素数さん :2005/09/28(水) 13:51:59
287 :132人目の素数さん :2005/09/28(水) 11:16:27 夫馬です。 「客観的な証明は20万行」も掛かるんだってさ。こんなの やってられないよね。普通の証明は、「直感」的なんだよね。 客観的ではないのよ。分かりましたか
31 :
132人目の素数さん :2005/09/28(水) 14:49:53
>プルーフチェックが今後、簡便化されていけば、 >将来的に実用もあるんじゃないかねえ? そのためには、人間にとっては直観的に明らかな命題を 自動証明する"行間を埋める"機能が必要だね。
行間を埋める機能で足りない場合に、人間が教えてやらなければならない。 約14年間にわたる共同作業の大部分は、人間にとって間を埋められるのが わかりきっている部分を、計算機に手取り足取り教えるのに費されたのでは ないかと。
33 :
132人目の素数さん :2005/09/28(水) 15:41:29
>わかりきっている部分を、計算機に手取り足取り教える もし黒木が査読者だったら、んなことせにゃならんのか?
34 :
132人目の素数さん :2005/09/28(水) 15:44:01
これからの数学論文はミザール言語で書く必要がありますね
>>28 それは最初にクレームしただけで、間違っている。Veblen の1905年論文は
ぐぐるとヒットするはず。シェーンフリース1906やL.ブラウワ1909(不動点定理
のほう、有限群のほうはR.ブラウワ)の論文もある。
Jordanよりも四色問題やケプラー問題のプルーフチェックをしてくれると
助かるね。
>>32 って事は結局、自動証明が実用的なものにならない限り、
人手も時間も掛かりすぎて駄目っぽいな
37 :
132人目の素数さん :2005/09/28(水) 15:51:18
>>36 通常、「自動証明」というのは人間にとっても意味のある定理を
証明することを目標にする
この場合は、人間にとって自明な命題を証明できればいい
厳密には区別できないが、そいうことだ
38 :
132人目の素数さん :2005/09/28(水) 15:56:19
人間にとっても意味のある定理の自動証明 人間にとっては自明な命題の自動証明 この間にある間隙はいかほどのものだろう
>>37 「人間にとって自明」ってのは、「良く知られた事実」と「良く知られた論法」の中から
「その場面において適切なものを選び出」せば、わずかな手順で証明が探索出来るって事だよね。
数学的事実とか論法のデータベース化と、
それらをどんな場面でどうやって組み合わせるのが適切か、という知識のデータベース化が進めば、
人間にとって自明な命題が証明出来るようになるのかな。
40 :
132人目の素数さん :2005/09/28(水) 16:04:10
Mizarはproof checkerだから、自動証明とは関係ないね。 既存の証明をMizar言語に翻訳して、Mizarに食わせて、 受理されるかどうかを確かめるってハナシでしょ。 しろうとの勘違いだったらスマン。
41 :
132人目の素数さん :2005/09/28(水) 16:06:54
>既存の証明をMizar言語に翻訳して、Mizarに食わせて、 >受理されるかどうかを確かめる それで済むなら、既に実用段階に近いということだね。 どっちが正しいのかは知らないが
42 :
132人目の素数さん :2005/09/28(水) 16:07:44
自動証明なんて出来ないから考えてもムダ。 それより、表題の件は証明チェッカーを通すために人間が 証明を機械にわかる形に書いたのが20万行ってことだろうな。 このステップ数をなんとか数千行くらいまで落とせれば実用になるだろう。
43 :
132人目の素数さん :2005/09/28(水) 16:09:50
44 :
132人目の素数さん :2005/09/28(水) 16:11:34
「人間が書いた証明が20万行」かよ。こりゃ、たまらんな
45 :
132人目の素数さん :2005/09/28(水) 16:13:51
「人間が書いた20万行の証明」を「Mizarプルーフチェッカー」に 食わせた、ということか?
46 :
132人目の素数さん :2005/09/28(水) 16:21:28
>Oswald Veblen が 1905年に一応の証明をしたと言われて >いますが、前提となる知識の到るところに直感が使われ、 >完全証明とは言いがたいものでした。 数学の定理のほとんどは、そうなのだが… 直感なしの証明が与えられている定理なんて、ほとんどない
・・・・・・・・・・・・(20万行) ・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・ ・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・ ・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・ ・・・・・・・・・・・・ これが証明すべきものであった.
48 :
132人目の素数さん :2005/09/28(水) 16:26:15
49 :
132人目の素数さん :2005/09/28(水) 16:29:22
結局、「人間が書いた1千行の証明」を「20万行の完全証明」に 自動変換するシステムが必要になるな。
50 :
The_Knight_of_Mathematics ◆uGlSZOV4Kc :2005/09/28(水) 16:29:39
>>48 そのためにPDが職を得るのSA
教授の原案をもとに数十人がかりでNA
世の中うまくまわるようになっるYO
51 :
132人目の素数さん :2005/09/28(水) 16:30:37
程度問題だろう。自然数の概念だって直感がないと理解出来ないし。 だからって、その概念があいまいで信用出来ないってことはない。 ある意味、直感ほど正確で信用おけるものはない。 程度によるけど。だから程度問題。
52 :
132人目の素数さん :2005/09/28(水) 16:30:38
>>49 自動証明はやったのか?やらなかったのか?それが問題だ!
53 :
132人目の素数さん :2005/09/28(水) 16:32:21
54 :
The_Knight_of_Mathematics ◆uGlSZOV4Kc :2005/09/28(水) 16:34:44
レズが早熟すぎる
55 :
132人目の素数さん :2005/09/28(水) 16:34:56
人間にとっても意味のある定理の自動証明 人間にとっては自明な命題の自動証明 この間にある間隙はいかほどのものだろう
56 :
132人目の素数さん :2005/09/28(水) 16:37:08
「人間にとって自明な命題の自動証明」ができることが 実用化の必要十分条件
57 :
The_Knight_of_Mathematics ◆uGlSZOV4Kc :2005/09/28(水) 16:38:26
人間の手で証明することは最上である MIZARによるものはその次によい - ウィリアム・メークピース・サッカリ(イギリスの小説家)
58 :
132人目の素数さん :2005/09/28(水) 16:40:56
「ピタゴラスの定理」の完全証明って、何行くらいになるの?
16人の共同研究じゃ誰にアーベル賞をあげるのか迷うだろうな。
>>58 ユークリッド幾何をMIZARが食えるように書き直すってのは
まあ面白いかもね。
今回は、ジョルダンという「自明のようだが証明はわかりにくい」定理の
プルーフチェックを計算機で行ったという着眼点がよかった。
ピタゴラスの定理だったら、さほど評価されないね。
四色問題なら14年ですまないw
フェルマーは人間がチェックするほうがはるかに早い。
論文の TeX ソースを MIZAR に変換する自動プログラムなんて、
当分無理だしね。
>>56 だろうな。検証対象の証明文を書くにしてもライブラリに登録する文章を書くにしても、
完全に行間を埋めなきゃいけなかったら、大変すぎて非実用的。
自明な行間くらいはコンピュータが自分で補ってくれないと。
「組み合わせ的に考察すれば明らか」とか「定数項に着目すれば明らか」とかを
詳しく書いてられない。
62 :
132人目の素数さん :2005/09/28(水) 17:31:06
自動証明は無理だって。あきらめな
64 :
132人目の素数さん :2005/09/28(水) 17:36:39
つーか、ジュルダンの定理は前から証明されているだろ。 フェルマー予想もな。 で、ほとんどの証明されてる定理には、まだ完全証明は 与えられていない。 ここ200年の間の数学的成果で完全証明の与えられて いる定理の割合は1%も行かないんじゃない
65 :
132人目の素数さん :2005/09/28(水) 17:38:01
証明と完全証明はまったく違うものだ 完全証明⊂証明だろうけど
>>62 それはproof checkerが実用的な(人手も時間も
掛からない)ものになる可能性を否定するも同然かと。
67 :
132人目の素数さん :2005/09/28(水) 17:39:25
「人間にとって自明な命題の自動証明」ができない限り プルーフチェックの実用化は無理だよん。諦めなwww
68 :
132人目の素数さん :2005/09/28(水) 17:40:28
自動証明⊂完全証明⊂証明
69 :
132人目の素数さん :2005/09/28(水) 17:47:33
>>66 proof checkerと自動証明はまったく別ものだろう。
難度から言ったら自動証明のほうがはるかに、というより可能と
不可能の違い。
70 :
132人目の素数さん :2005/09/28(水) 17:52:01
>>69 proof checker の実用化=自明な命題の自動証明
自動証明=意味の有る定理の自動証明
という意味でなら、違うなあ
71 :
132人目の素数さん :2005/09/28(水) 17:53:54
>>69 つまり、自明な命題の自動証明は可能、
意味の有る定理の自動証明は不可能と
いうことですかい
永田・可換体論の「自明」を自動証明できるレベルじゃなきゃダメだろw
73 :
132人目の素数さん :2005/09/28(水) 17:57:28
コンピュータが自動で行間を埋めない限りは、 人間がすべての行間を埋めなければならない それは人間が「定理の証明図」を書かないと いけない、というのと同じ これでは、プルーフチェックは全く実用的で ない
74 :
132人目の素数さん :2005/09/28(水) 18:00:21
>>72 「禿 藁 to appear 論文」の自明を
自動証明ができるレベルじゃなきゃ
ダメだろw
75 :
132人目の素数さん :2005/09/28(水) 18:02:52
>>74 それが出来たら、禿ちゃんの数学者としての名誉も完全回復だね♪
76 :
132人目の素数さん :2005/09/28(水) 18:04:37
>>74 それは「自明」ではなく「間違い」。百歩譲って「ギャップ」。
本人による手動証明もできるレベルでないwww
77 :
132人目の素数さん :2005/09/28(水) 18:05:26
>>75 禿ちゃん、病院のベッドの上でMIZARを必死に勉強中らすい
78 :
132人目の素数さん :2005/09/28(水) 18:07:35
>>76 いや、Ann. Math. の査読者が間違っているんだよ。
正しいのは分科会だった、ということまで自動的に
証明できるよ♪
細かい行間についてはコンピュータに自分で埋めて貰って、
一定時間内に埋められなかった行間は自己申告して人間に埋めて貰う。
んでその埋められなかった行間が多すぎなければ実用的と言えるかと。
>>74-78 巣に帰れ。他スレにまで迷惑掛けるな。
80 :
132人目の素数さん :2005/09/28(水) 18:10:28
完全証明って何?人間の脳よりコンピューターの方が正確ってこと?
82 :
132人目の素数さん :2005/09/28(水) 18:15:57
>>79 ただ、今回のは「行間を埋める」じゃなくて、何が仮定されてるのか
よくわからんから証明をチェックしてみました〜って話だから、
「自明をコンピュータで埋める」とは違うかと。
論文の自明は「ルーティンだけどめんどくさい」が多いので、
さまざまなルーティンを全部プログラムにぶち込むのは今のところは
不可能。今回は、ジョルダンに特化してるわけで、何にでも使える
わけではない。
83 :
132人目の素数さん :2005/09/28(水) 18:16:32
>>81 数学基礎論(とくに証明論)の初歩の初歩をどうぞ
84 :
132人目の素数さん :2005/09/28(水) 18:20:21
85 :
132人目の素数さん :2005/09/28(水) 18:42:27
>>83 「完全証明は史上初」という売り文句は素人相手に有効だよね。
完全証明ということばで、今までの証明は数学的に不十分だったと
思わせられるから。
86 :
132人目の素数さん :2005/09/28(水) 18:49:07
>>85 そうすると、現在までに証明されているほとんどの定理には
数学的に完全な証明はないことになるんだけどね。
スレタイみて思い出したんだけど昔幾何系のスレでジョルダンの閉曲線定理を S_nのアレキサンダー双対とかいうので証明したスレがあったとおもうんだけど あれどこだっけ?おぼえてるひといまつ?
88 :
海援隊 :2005/09/28(水) 19:22:08
ジョルダンなんかでジョルダン言うか!
89 :
132人目の素数さん :2005/09/28(水) 19:35:08
武田鉄也の弟の名前は?
90 :
132人目の素数さん :2005/09/28(水) 19:48:00
Mizar言語の職人が量産されて、それがMizarドカタ等と蔑まれる時代が来るのだろうか…
>>90 それが崩れの生きる道。数学の就職問題が解決されるかも
92 :
132人目の素数さん :2005/09/28(水) 19:57:14
これで中村教授も日本を代表する数学者の仲間入りか。
93 :
132人目の素数さん :2005/09/28(水) 20:27:55
信濃毎日新聞のバカ記者をなんとかしてくれ! ---------------------------------------------- 9月28日(水) ------------------------------------------------------------------------ ジョルダンの曲線定理 信大教授ら「完全証明」 ------------------------------------------------------------------------ 信大工学部の中村八束教授(62)=長野市青木島、数理情報学=が28日 までに、約120年間、数学的に完全に証明されなかった「ジョルダンの曲線 定理」を、ポーランドの数学者らと共同で初めて完全証明した−と同教授が管 理するホームページ上で発表した。 ジョルダン曲線定理は、「閉じた曲線は、平面を内と外に分ける」というも の。1887年、フランスの数学者カミーユ・ジョルダンが発表した。中村教 授は「直感的には当然だが、誰も数学的に完全な証明ができなかった」として いる。 中村教授は1991年、ポーランドのワルシャワ大学ビアリストーク分校に 勤務する数学者とともに証明に取り組み始めた。同国の数学者らが管理する、 数学の証明をチェックするコンピューターシステム「ミザール」を用い、両国 の計16人の数学者が分担、14年かけて証明を終えた。 中村教授は「ジョルダン曲線定理を前提にしていた多くの証明がある。今回 の証明で、そうした別の証明にも根拠を与えることができる意義は大きい」と している。 東工大大学院情報理工学研究科の小島定吉教授(位相幾何学)は「基本的に は証明された定理だと考えているが、数学者にとっては、どこまで証明すれば 完全かという問題がある。ミザールを使い、完全に証明できたという点に意味 があるのではないか」としている。
ミザールを使った今回の証明が完全であることは、どう証明するの?
95 :
132人目の素数さん :2005/09/28(水) 21:27:24
数学者が普通のやる厳密にしかみえない証明も 見方によっては、実はあいまいな直観にたよった証明だった という事実に衝撃 数学側からみて物理の人の使う数学が 「いい加減なことやってんな」 と思うのに似てるのか?
96 :
132人目の素数さん :2005/09/28(水) 21:49:45
>>94 互換性のある別の処理系を作って追試するしかないんじゃないか。
直感的に正しいんだからそれでいいじゃんって人はいっぱいいて。 でもそれで満足しなかった人が数学的に証明したりして。 それでも満足しなかった人が計算機にチェックさせたと。 それでもなお満足しない人はチェッカが正しいことを何らかの方法で確かめて、 その方法が正しいことを確かめて(以下無限ループ) になるんだろうかねえ
98 :
132人目の素数さん :2005/09/28(水) 21:59:48
>>97 それでも満足しない人は
公理系の妥当性を疑う
そしてノイローゼになる
>そしてノイローゼになる ワロスwww でも実際、数学はそういう公理の元、つまりある程度人間の空想であるもの、 これの上で成り立っているものだから、 「数学的な証明」っていうのはどうなってくるんだろうなぁ。。。
>>99 人によっては、人間の存在とは全く別個に数学的現象の実在を信じ、
実在する数学的現象を人間が記述する事が数学である、と思ってる人もいる。
そういう人にとっては、公理ってのは人間が後から取ってきた一つの言語に過ぎないし、
ZFCか型の理論かそれら以外かとかもどうでもいい事。
ゼータの実在を信じてる人も。
101 :
99 :2005/09/28(水) 22:49:31
>>100 さん:
マジレスありがとうございます。
そういう捉え方もありましたか。。。
何か数学について人間について考えさせられました。本当にありがとうございます。
数学って物理的な部分を持つ反面、何かと哲学っぽいですね。
102 :
132人目の素数さん :2005/09/28(水) 22:52:30
哲学を数学に持ち込むな 数学徒は鉄柱にだけはなってはいけない
103 :
132人目の素数さん :2005/09/28(水) 23:31:13
一楽重雄の「位相幾何学」(朝倉書店)に初等的な証明がある。私はおかしいと思わなかったが、ギャップを見つけた人は教えて欲しい。
104 :
132人目の素数さん :2005/09/28(水) 23:41:46
105 :
132人目の素数さん :2005/09/29(木) 00:47:46
タマゴの内側と外側は実は分けられないってことを直感で証明せれって言われてもなぁ
>>105 それはむしろ閉曲面バーションっぽいな。
3次元ユークリッド空間の場合も「証明」済みなんかな?
>>106 1次元以上なら何次元でも成り立つ(0次元球面は2点空間)。
>>46 直観を使うにせよ、せめて直観を論理で埋めることが
可能なことくらい確認するはず
>>56 まあ永田雅宜先生にとって自明な命題≠普通の数学者にとって自明な命題
だけどなwww
110 :
132人目の素数さん :2005/09/29(木) 09:06:14
しょうがねえな、素人は。あれはプルーフ・チェッカーの試験として 行っただけだろ。なにもジョルダンの定理の証明が不完全だから機械にかけて 完全な証明を行ったわけじゃない。お前等のポイントがずれてるんだよ。 つまり勘違い。あの20万行の内容を具体的にみればわかるだろうけど、 あれは既存の証明を機械にわかる形に書いただけのもんだろ。
お前等って誰のこといってるんだ? 半分以上の人間はそんなこと分かってると思うが
112 :
132人目の素数さん :2005/09/29(木) 09:18:37
素数が無限個あるっての Euclid の有名な証明あるよね? あれを Mizar 言語で だれか書いてくんない? Mizar の感じをつかみたい
113 :
132人目の素数さん :2005/09/29(木) 10:19:35
>>42 矛盾してるな。
20万行を数千行に圧縮するには、
圧縮された証明の行間を埋められる
程度に賢い自動証明が不可欠。
述語論理の充足可能性の非決定性の壁を
突破しろなんて誰もいっちゃあいない。
114 :
132人目の素数さん :2005/09/29(木) 10:27:39
>>82 >今回のは「行間を埋める」じゃなくて、何が仮定されてるのか
>よくわからんから証明をチェックしてみました〜って話だから、
>「自明をコンピュータで埋める」とは違うかと。
一口に「自明」といっても奥が深い。
単純に論理学的に少ないステップで証明できるものとは言えない。
直観的には人間は理解できるが、機械がチェックできるような
形式的な理論が構築されていない場合は多々ある。
ただ、こういう話は、昔AIで議論されたフレーム問題にも関わる。
AIが記号主義からコネクショニズムにパラダイムシフトした
最大の理由は、いちいち言葉で書くのが面倒くさいので、
機械が勝手に学習してくれればいいなと思ったから。
115 :
132人目の素数さん :2005/09/29(木) 10:27:57
116 :
132人目の素数さん :2005/09/29(木) 10:32:03
>>115 一方で、自動証明はダメといいつつ、
もう一方で、行数を少なくしろといってること。
行数を少なくすれば、行間が広くなる。
そこは、単純に推論規則に当てはまってるかどうか
だけではチェックできない。行間を埋められるような
推論規則の組み合わせが存在するかどうかを確かめる
必要がある。それはまごうことなき「自動証明」だ
117 :
132人目の素数さん :2005/09/29(木) 10:35:02
>>93 >基本的には証明された定理だと考えているが、
(本音)同じ分野の連中は皆納得してるって
>数学者にとっては、どこまで証明すれば完全かという問題がある。
(本音)ただ、畑違いの連中が「わかんねー」
なんていうからめんどくせーんだよ。
>ミザールを使い、完全に証明できたという点に意味があるのではないか
(本音)ま、そういう連中が納得できるんなら、いいんじゃねーの?
118 :
132人目の素数さん :2005/09/29(木) 10:35:12
とにかくAIやってる連中は楽観過ぎる。能天気というか、SFの 読みすぎというか。20世紀における科学技術の進歩に幻惑されて るんだろうな。
119 :
132人目の素数さん :2005/09/29(木) 10:39:47
>>116 >一方で、自動証明はダメといいつつ、
>もう一方で、行数を少なくしろといってること。
行数を少なくしろなんて言ってないだろ。
実用になるには行数が多くては駄目という当然のことを言ってる。
自動証明が駄目という意味は、non-trivialな定理の証明が駄目って
いうこと。すこしは、意を汲んだらどうだ、コンピュータじゃあるまいし。
120 :
132人目の素数さん :2005/09/29(木) 10:45:58
>>118 「楽観過ぎる」というのはその通りだな。
もっとも、誰にも迷惑はかけていないと思うが(w
121 :
132人目の素数さん :2005/09/29(木) 10:48:55
>>120 >もっとも、誰にも迷惑はかけていないと思うが(w
税金使ってないか?
122 :
132人目の素数さん :2005/09/29(木) 10:56:55
>>121 使ってるだろうけど、それがなくなると
貴様のところにいったいいくら戻ってくるか
一度でもマジメに計算したことあるのか?
123 :
132人目の素数さん :2005/09/29(木) 10:59:43
>>93 >小島先生も相変わらず言葉を濁してるねwww
数学者の間で証明されたと認められている定理でも
完全証明のないものは非常に多い。例えばワイルズ
により証明されたフェルマーの最終予想もその一つ
でしょう。この研究は、それらの定理に完全証明が
与えられるようになる第一歩となるのではないかと
期待できる
とでも言っておけば…
124 :
132人目の素数さん :2005/09/29(木) 11:14:16
>>122 そう開き直られてもな。第5世代コンピュータ開発計画
(つまりAI)というのが鳴り物入りで始められたことがあったよな。
あのプロジェクトにいくら使われたのか。数億程度なわけないだろ。
で結局失敗。その責任を取ったやつっているのかよ。
誰もいないから、まだ懲りずにAIやって飯食える。甘い世の中だよな。
125 :
132人目の素数さん :2005/09/29(木) 11:18:04
数学者の間では既に証明されたと認められている定理でも 完全証明のないものは、ジュルダンの閉曲線定理以外にも 非常に多い。例えばワイルズにより証明されたフェルマの 最終予想もその一つでしょう。この研究はそれらの定理に 完全証明が与えられるようになる第一歩となるのではない か、と期待できる
126 :
132人目の素数さん :2005/09/29(木) 11:37:07
>>125 それを言うならピタゴラスの定理だって完全証明はないんじゃないの?
完全証明なんていらないってのがほとんどの数学者の意見だろう。
まあ、ケアレスミスのチェックにあれば便利というくらいで。
ただし、20万行も書かなきゃなんないのなら論外。
もっと効率よく補題や補助定理を扱えるような 証明工学的なアプローチが必要なんだよな 20万行だと一寸本職の数学者が使う気にはならないな プログラマにとって見れば大したこと無いんだろうけど (WindowsのOSが2000万行くらいだったっけ?オーダーはあってるはず)
128 :
132人目の素数さん :2005/09/29(木) 11:47:46
>>126 そうだけど。そこまで言ってしまうと角が立つから、
大人の対応としての発言として、こんなのどう?、と
いう提案だ。
129 :
132人目の素数さん :2005/09/29(木) 12:03:13
>>124 >第5世代コンピュータ開発計画
これの残党でちゃっかり数学教授におさまってるのが
R命館にいるな
指導者の淵も大学におさまちゃってるが
責任とらずに
>第5世代コンピュータ開発計画 >(つまりAI) AIは第五世代コンピュータ開発計画の一部だよ 似たような例として、第五世代=シグマという勘違いをしてる人もよく見掛けるね
131 :
132人目の素数さん :2005/09/29(木) 12:35:08
>AIは第五世代コンピュータ開発計画の一部だよ AIはあのプロジェクトの主要な部分だからな。だからなに?
>>124 の文章の「AI」を別のものに変えれば
TRONもΣもなんだって批判できるよなぁ、程度の意味です
133 :
132人目の素数さん :2005/09/29(木) 13:59:47
だから彼らの失敗も免罪されると? 違うだろ。能天気すぎるんだよ。AIやってる連中は。 SFの読み過ぎだって。映画「2001年宇宙の旅」の見すぎ。 あの映画は2001年を舞台にしたものでHALというAIコンピュータ が活躍するな。で2005年の現実はっていうと、あんなものは影も形もない。 あの原作者のクラークは通信衛星なんかを予言して、わりと先見性があるけど AIに関してはまるで大はずれ。彼はSF作家だから、はずれても問題ないけどな。
134 :
132人目の素数さん :2005/09/29(木) 14:02:17
>>133 HAL は中に人がいる設定だったけどな
その意味じゃはずれてない
>>133 君はそんなにAIに期待を持っていたのかね
なるほどそれでボクの心を裏切ったんだと
シンジ君宜しく発狂寸前な訳ですな( ´,_ゝ`)
136 :
132人目の素数さん :2005/09/29(木) 14:20:25
んなことはない。公開当時は俺はガキだったけど、あんなものは 出来っこないとバカにしていたよ。まあ、おとぎ話として、 映画は映画として見たが。
137 :
132人目の素数さん :2005/09/29(木) 14:27:27
>第5世代コンピュータ開発計画(つまりAI) 第五世代=AIというのはいくらなんでも無知すぎるな。 AI以前の理論計算機科学のところが大きいんだが。 >結局失敗 そりゃ君が勝手に高望みしてるからじゃないか? 少なくとも日本で理論計算機科学で博士取得者を 沢山生産できたのは成功だよ。まあ、高山さんとか 数学に逃げられてしまったが(笑
138 :
132人目の素数さん :2005/09/29(木) 14:33:04
>ピタゴラスの定理だって完全証明はないんじゃないの? あれは、暗にこの世界がおおむねユークリッド空間であることに 全面的に依存してる。 もしこの世界が例えば双曲的非ユークリッド空間だったら失敗する。
139 :
132人目の素数さん :2005/09/29(木) 14:33:26
>AI以前の理論計算機科学のところが大きいんだが。 今のAI研究も同じようなもんだろ。AIとは名ばかり。 >そりゃ君が勝手に高望みしてるからじゃないか? 第5世代コンピュータって出来てないだろ。 これが失敗でなくて何?
140 :
132人目の素数さん :2005/09/29(木) 14:34:33
141 :
132人目の素数さん :2005/09/29(木) 14:35:10
ところで >数億程度なわけないだろ。 日本の人口を一億として、十億なら十円、百億なら百円。 まあ、百円戻ってくるならジュース一本くらい買えるかな。 職場内の自販機だと百円で買えるし(w
142 :
132人目の素数さん :2005/09/29(木) 14:38:25
143 :
132人目の素数さん :2005/09/29(木) 14:40:56
正確にいえば、曲率がもし非常にわずかだったら 失敗したとは気づかれない。 それは、非常に遅い速度では相対性理論を 必要としないのと同じようなものである。
144 :
132人目の素数さん :2005/09/29(木) 14:43:02
>>141 何も日本人全員に割り振るなよ。まともに税金納めてる人間は
30%くらいだろ。そうすると、300円か。
俺だったら100円でもドブに捨てたくないね。
AIとか全然知らなくてレスの字面だけ読んだだけだけど、 「第五世代なんちゃらは、投下した税金に見合った成果が得られていない、 プロジェクトとして見通しが甘すぎた」 って言いたいんじゃないの?
146 :
132人目の素数さん :2005/09/29(木) 14:43:49
>>135 シンジはまだ幸せ。
ODの心境はさながらアスカのようなもの。
147 :
132人目の素数さん :2005/09/29(木) 14:47:01
>投下した税金に見合った成果が得られていない 一見もっともらしいが、じゃあいったいどういう成果を 期待していたんだと聞くと、実に妄想モード全開みたいな 回答がバカバカでてきて、呆れ果てる。
148 :
132人目の素数さん :2005/09/29(木) 14:49:18
>俺だったら100円でもドブに捨てたくないね。 漏れは君が使うほうがドブに金を捨てた気分になるが(w
149 :
132人目の素数さん :2005/09/29(木) 14:51:24
>>142 世界が非ユークリッドだとユークリッド幾何学の定理が証明出来ないのか?
そんなことはないだろ。幾何学というのは、我々の住む世界だけを
扱うわけではない。
150 :
132人目の素数さん :2005/09/29(木) 14:55:23
「完全証明」ってのは基礎論的な概念なのか? 基礎論ヲタの人教えて。
151 :
132人目の素数さん :2005/09/29(木) 14:56:18
>>149 >世界が非ユークリッドだとユークリッド幾何学の定理が証明出来ないのか?
図形を切った貼ったする証明に関してはそう。
152 :
132人目の素数さん :2005/09/29(木) 14:59:33
つまり、世間的にいう「ピタゴラスの定理の証明」とは、実は 「ユークリッド空間ではピタゴラスの定理が成り立ちますよ」 という実証でしかない。
>>138 の「世界」という専門用語を「今考えている形式的体系」という風に
非常に好意的に無理矢理解釈すれば、まぁ間違いではないか。
154 :
132人目の素数さん :2005/09/29(木) 15:04:01
>>151 切った貼ったって三角形の合同だろ。そんなものは、ユークリッドの公理
から出るだろ。
156 :
132人目の素数さん :2005/09/29(木) 15:13:53
>>152 何を当たり前なことを。
誰も非ユークリッド空間でピタゴラスの定理が成立つとは言ってないよ。
トンデモは除いてだが。
157 :
132人目の素数さん :2005/09/29(木) 15:17:45
>>155 まあ、誤解をまねく用語なことは確か。
形式的証明でもちょっとおかしいけどね。
もっとも基本となる前提から通して証明されたことはなかった くらいにしときゃ誤解も無いんだろうけどな
159 :
132人目の素数さん :2005/09/29(木) 15:33:20
>>157 >>125 数学者の間では既に証明されたと認められている定理でも
形式的証明はなされていないものは、ジュルダンの閉曲線
定理以外にも非常に多い。例えば、ワイルズにより証明が
なされたフェルマーの最終予想もその一つでしょう。この
研究はそれらの定理にも形式的な証明が与えられるように
なる第一歩となるのでないか、と期待できる
そうすると素直に読めるなwww
160 :
132人目の素数さん :2005/09/29(木) 15:36:27
そういや
>>138 みたいなことを真顔で主張した挙句
したがってワイルズの証明は間違っているとやった人が
アメリカに居たねw
>>150 No
単に証明の計算機による検証のことを
信州大の教授が完全証明と称しているだけ
163 :
132人目の素数さん :2005/09/29(木) 16:19:35
>>162 数理論理では、記号論理による数学の定理の証明のことをさす
用語があるんじゃないの? 形式証明でいいのかな?
普通はそれを単に証明って呼ぶと思いますけど もちろん、メタ論理のレベルでの、たとえば不完全性定理の「証明」とかとは 意味が違う訳ですが、文脈から言って誤解する可能性はほとんど無いですし まあ、形式的証明とか形式証明とか言っとけば 言いたいことは通じるんじゃ無いでしょうか
>>163 > 形式証明でいいのかな?
他にも、証明図という呼び方をする場合もある。
面倒なので単に「証明」と呼んで、通常の証明を「非形式的証明」と言ったりもする。
>>163 「証明図」とか「証明木」とかは見た事がある。単に「証明」って言う事が多い。
「完全証明」と名付けてるのは見た事がない。
あと「形式証明」って言ったら、
普通は「証明する対象がメタでない」という事の強調として捉えると思う。
>>138 の理屈で言うと
この世界は概ねユークリッド空間だから
非ユークリッド空間で成立するとされている全ての定理は
証明に失敗しているわけですね。
てゆうか1次元や2次元で成立する定理も全部ダメですね。
この世界は概ね3次元なんですから。
自然数もダメ。あれ無限だし。この世界にあるのは自然数の
有限部分集合だけだもんね。数学は窮屈な学問だね。
168 :
132人目の素数さん :2005/09/29(木) 16:36:31
>>153 にたずねるが君の知ってるピタゴラスの定理の証明を
一つここに書いてくれないかね。
証明図ってのは自然演繹とかSequent計算で使うことが多いかな
次は有限単純群の分類証明を 計算機でチェックできる形式に書き下してくれ
171 :
132人目の素数さん :2005/09/29(木) 16:43:55
>切った貼ったって三角形の合同だろ。 そう。 >そんなものは、ユークリッドの公理から出るだろ。 物理的に切った貼ったするならユークリッドの公理に従うとは限らない(w つまり、そこが盲点というわけだ。
172 :
132人目の素数さん :2005/09/29(木) 16:46:12
いずれにしてもシロートさんたちが 勧違いしてしまいそうだから 数学会として公式見解を出しておく 必要がありそうですね Up野先生,こういうときこそ その指導力を善用してください 若手いじめではなく
ヒルベルトの幾何学基礎論の、ピタゴラスの定理の証明は 原理的に計算機でチェックできるくらい厳密じゃないのかな (実数論の公理を一寸手直しする必要があるかもしれない) もっとも、この本は全く直観を排して書かれていることで有名だけども、 それでもとある「明らかだが証明が難しい」定理が、 "困難も無く"得られることになっているのだがw
>>170 そもそも証明が完全に公表されて無いんじゃなかったっけ
175 :
132人目の素数さん :2005/09/29(木) 16:55:35
>>173 にたずねるが、君が始めて習った証明は
そのヒルベルトの幾何学基礎論による証明かい?
すり替えはよくないね。学問を否定する悪行だよ。
176 :
132人目の素数さん :2005/09/29(木) 16:57:30
>>174 いや公表はされてるんだけど
あまりに膨大で入りくんでいるため
確認がとれない
最近の Aschbaher らの仕事で
あやしかった部分が克服されて
ようやく完成したと見ていいでは(?)
という話
177 :
132人目の素数さん :2005/09/29(木) 16:59:17
ヒルベルトの幾何学基礎論というのは、ある意味 中村八束氏の仕事の先駆といってもよいものだ。 つまり、ヒルベルトの証明と通常の作図による証明の差を理解すれば 形式的証明と通常の証明(あるいは説明)の差を理解できるはずである。
178 :
132人目の素数さん :2005/09/29(木) 17:03:01
>>172 では、公式見解の叩き台を考えましょう。
数学者の間では既に証明されたと認められている定理ではあっても
形式主義的に満足できる証明がなされているものは、非常に少ない。
例えば、ワイルズによって証明がなされたフェルマーの最終予想も
形式的証明までは、まだ遠いようである。今回の中村氏らの研究は
それらの定理にも、形式的な証明が与えられるようになる第一歩と
なるのではないか、と大きな期待を抱かせるものである。
>>175 別にそんなこと一言も主張してないが
初めて習うときに多分に直観的な証明がされて何が悪い?
180 :
132人目の素数さん :2005/09/29(木) 17:08:29
>>178 数学者の間では既に証明されたと認められている定理ではあっても
形式主義的に満足できる証明がなされているものは、非常に少ない。
例えば、ワイルズによって証明がなされたフェルマーの最終予想も
形式的証明までは、まだ遠いようである。今回の中村氏らの研究は
それらの定理にも、形式的な証明が与えられるようになる第一歩と
なるのではないかと我々数学者に大きな期待を抱かせるものである。
最後の行に「我々数学者に」を入れてみたけど
>>177 計算機によって証明が検証された!とか言っても
今度は計算機とそのプログラムの信頼性の問題が出てくるわけで
往々にして健全な直観の方が信頼が置けたりするわけで
まあ、たとえJordan曲線定理にしか適用できないようなモノだったにせよ、
それまで殆ど計算機科学者の机上の空論だった証明チェッカが
初めて実際に実際の数学の定理の証明をチェックした、
という意味で意義の有る仕事だとは思うけどね
しかし
>>177 のレスは、まるで
形式的証明以外はすべてただの説明である、証明に非ず
って暗に言ってるような感じで一寸違和感があるな、、
直観が混じった証明か、原理的に論理規則と公理だけからできる証明かは
数学者だったら簡単に区別くらいつけられる
183 :
132人目の素数さん :2005/09/29(木) 17:13:51
>>178 だから形式証明なんかほとんどの数学者は必要としてないんだって。
手軽に出来るならケアレスミスのチェック用に便利っていうだけ。
だけど手軽になんか出来ないだろ。
184 :
132人目の素数さん :2005/09/29(木) 17:14:12
>>179 >初めて習うときに多分に直観的な証明がされて何が悪い?
問題は、その直観が隠れた前提を持っているかどうか。
例えば作図の場合、たいていの人は作図による合同と
物理的な「切った貼った」の違いに気づかない。
しかし、非ユークリッド幾何学のクラインモデルや
ポアンカレモデルを理解するにはこの違いに気づく必要がある。
185 :
132人目の素数さん :2005/09/29(木) 17:15:18
>今度は計算機とそのプログラムの信頼性の問題が出てくるわけで >往々にして健全な直観の方が信頼が置けたりするわけで それは今のところね。しかも、健全な直観を獲得するのは ごく専門領域に限ったとしても大きな労力を要することは 君もよく知っているはずだよね だから、コンピュータによる自動化が今後なされることは、 それなりに意味のあることだろう。まだ実用段階にはない だろうけど。特に数学の証明問題の自習に役立つと思うし、 数学者だって自分の証明のチェックに使えるだろう
186 :
132人目の素数さん :2005/09/29(木) 17:17:51
>>183 「必要ない」なんていったら、角が立つだろう。
これは政治的な話でもあるんだよ。素人の誤解を
解きつつ、見解は相手を立てる言い方にしないと
別に相手を立てる言い方はしてなかったつもりなのに 新聞記者が勝手に都合の良い所だけ切り取ってきた、という可能性もあるがな
188 :
132人目の素数さん :2005/09/29(木) 17:19:33
189 :
132人目の素数さん :2005/09/29(木) 17:20:25
>>181 >往々にして健全な直観の方が信頼が置けたりするわけで
プログラムのミスも人間のミス(w
それも含めて人間がミスしやすいのは明らか。
>>182 そう読むのは間違っている。
> 直観が混じった証明か、原理的に論理規則と公理だけから
>できる証明かは数学者だったら簡単に区別くらいつけられる
これは大嘘。数学者は無意識に直観を混入させている。
その直観が論理規則と公理で正当化できるかどうかなど
数学者にはさしたる関心はない。時間の無駄だからだ。
>>185 そんなに手軽に証明チェックが出来るようになるものかな?
普通証明する場合は同様に、で済ませるようなところだって
機械はそれじゃ理解してくれないし
191 :
132人目の素数さん :2005/09/29(木) 17:23:36
ヒルベルトは「必要」という立場だったわけでさ 当時の現実的可能性の少なさに負けたとも言える その可能性を追求している人達を無碍に否定する 必要もなかろうて
192 :
132人目の素数さん :2005/09/29(木) 17:26:58
>「必要ない」なんていったら、角が立つだろう。 いや、必要ないと思ってるならはっきりそういうべきだろ。 喧嘩が怖いチキンは真っ先に食われる。
193 :
132人目の素数さん :2005/09/29(木) 17:27:11
>>190 >機械はそれじゃ理解してくれないし
だから、今はね。今後の可能性を否定
しなくてもいいでしょ。そういうこと
やってる人の研究を、部外者が見解を
出すに当たっては気の利いたリップ・
サービスをしてこうぜ
2chで誹謗中傷は、大いに結構だがw
194 :
132人目の素数さん :2005/09/29(木) 17:29:10
数学者の考える正しさ ・オレが理解できたらその定理は正しい (ただしオレ自身が証明した定理を除く)
195 :
132人目の素数さん :2005/09/29(木) 17:30:04
>>193 やれやれ批判と誹謗中傷と区別できない馬鹿がここにもいたか。
196 :
132人目の素数さん :2005/09/29(木) 17:31:22
>>192 必要ないのは、多くの数学者の感覚に過ぎないだろ。
大体、数学会には「基礎論屋」だっているんだから
基礎論屋なんて追い出せ、という教条主義を掲げる
決意をこれからは持つというならそれもありかもな
そいつらは必要だと思ってやっているわけだから、
それに合わせてやれ
197 :
132人目の素数さん :2005/09/29(木) 17:32:18
数学者の嫌いな正しさ ・オレが理解できないのに機械が検証したなんて認めない!
198 :
132人目の素数さん :2005/09/29(木) 17:34:34
>>191 >ヒルベルトは「必要」という立場だったわけでさ
根拠は?
199 :
132人目の素数さん :2005/09/29(木) 17:35:02
>だから、コンピュータによる自動化が今後なされることは、 >それなりに意味のあることだろう。まだ実用段階にはない >だろうけど。特に数学の証明問題の自習に役立つと思うし、 >数学者だって自分の証明のチェックに使えるだろう 実用化されれば、役立つじゃんか。まあ、実用化されるのに どれだけ時間が掛かるのは分からんがなw
200 :
132人目の素数さん :2005/09/29(木) 17:35:31
>>196 いまや、ロジシャンなんてソフトウェア科学会とか
科学哲学会あたりに亡命しちまったと思ったが(w
数学屋の嫌論理なんてのはヨーロッパの反ユダヤ主義
くらい根深いもんだろ。
201 :
132人目の素数さん :2005/09/29(木) 17:36:39
>>198 一般に流布している常識を知らない?まあ、
常識が正しいという確証はないわけだが…
202 :
132人目の素数さん :2005/09/29(木) 17:39:06
ロジシャンが数学屋に嫌われるのは、彼らの成果が 数学屋のプラトニズムという信仰の虚妄を明らかに するものだからだろう。 数学的プラトニズムが極右なら 論理的フォーマリズムは極左
>>196 別に基礎論屋がこういう証明を支持するかというと
また微妙かもしれないけどね
>>200 50年前にこういうふいんきは無かったはず
というか、日本特有じゃないのかな、基礎論異端視がこんなに激しいのは
集合論屋にはプラトニズムの塊みたいな人も多いけどね
205 :
132人目の素数さん :2005/09/29(木) 17:42:52
206 :
132人目の素数さん :2005/09/29(木) 17:44:53
>>203 >別に基礎論屋がこういう証明を支持するかというと
>また微妙かもしれないけどね
彼らは専門家だから、より慎重でしょう。
ただ、こういう方向性の研究自体には、普通の数学者
よりも親近感を持つ人が多いでしょう。中には、近親
憎悪的過剰反応を示す香具師もいるかも試練が。
207 :
132人目の素数さん :2005/09/29(木) 17:45:07
>数学屋のプラトニズムという信仰の虚妄を明らかに >するものだからだろう。 どう明らかにするんだよ。
208 :
132人目の素数さん :2005/09/29(木) 17:46:28
>>205 「ヒルベルトは形式主義の提唱者」という常識
209 :
132人目の素数さん :2005/09/29(木) 17:47:28
>>203 いや、世界的傾向だね。
ロジックは結局言葉の学問だからね。
たいていの日本人は、ロジックが存在する意味すら理解できていない。
だから、極少数の理解者は、さながら隠れキリシタンのようなもの。
210 :
132人目の素数さん :2005/09/29(木) 17:50:15
別分野だからといって、彼らの研究を否定する必要はない。 どっかの研究科みたいに、教条主義を掲げて別分野をパージしますか?w
211 :
132人目の素数さん :2005/09/29(木) 17:52:44
ま、数学者の価値観は厳密性よりも 『面白さ&有用さ』にあるからね。
>>208 俺は205じゃないけども
ヒルベルトの形式主義は別に計算機で証明をチェックすれば
厳密性が確保できる、とか言うことじゃなくて
証明を形式的に書き下せば自然数論なり実数論なり、
特定の形式的数学の無矛盾性が証明できるから、(りゃ
という思想だったはず
もちろん俺はヒルベルトの後継者だ!とか自負するのは勝手だけど
一寸ヒルベルトの考えに対する勝手な憶測が入りすぎかと
213 :
132人目の素数さん :2005/09/29(木) 17:53:03
>>206 ロジシャンは興味を持つだろうね。
ただ、ロジシャンは素人のようにロジックに絶対的信頼は置いてない。
だから、フォーマルだから正しいとは言わない。
彼らが興味を持つというのは、正しいかどうかよりも、どういう
フォーマリズムによってそれが証明されるのかという仕掛け。
ある意味、マニアというかヲタク的興味。
214 :
132人目の素数さん :2005/09/29(木) 17:53:48
面白さ>>>厳密性 有用さ>>>厳密性 基礎論屋は、死ね!
216 :
132人目の素数さん :2005/09/29(木) 17:54:51
まあまあみなさんおちついて 私見では置換群が鍵のように見えるんですが…
217 :
132人目の素数さん :2005/09/29(木) 17:57:39
無矛盾性にこだわるのは単なる厳密性フェチよりも重症。 ヒルベルトがつきぬけてるのは、文字面だけ考えればイイ! というところに気づいた点。 ただ、こういう発想は数学者にはとっても嫌われる。 美女も骸骨だけみりゃいいみたいな感じにとられるわけだ(w
218 :
132人目の素数さん :2005/09/29(木) 18:00:11
あれ?! マツシン先生いますか? いたら返事をしてください
219 :
132人目の素数さん :2005/09/29(木) 18:02:11
>>212 計算機でチェックするとは言ってないでしょ。大体、
当時はコンピュータがなかったんだから
ヒルベルトは2段構え
1.定理の客観性を確保するために、形式体系内で証明を行う
2.当該の形式体系が少なくとも全く無意味であることを保障
するためには、(有限の立場で?)無矛盾性を確認する
2はゲーデルによって(一応の)否定を見たわけだけど、1は
なんら否定を受けていないからさ
一応、形式的に証明されれば客観的な訳で、もちろん矛盾した
体系ならば、すべての命題が正しいから意味はないけど。その
場合であったとしても正しいということ自体は客観的ではある
220 :
132人目の素数さん :2005/09/29(木) 18:02:22
>集合論屋にはプラトニズムの塊みたいな人も多いけどね いまどきの集合論屋は数学者です。 彼らを、基礎論屋とかロジシャンとか呼ぶとたいてい蹴られます。
221 :
132人目の素数さん :2005/09/29(木) 18:04:19
>>219 >2.当該の形式体系が少なくとも全く無意味であることを保障
> するためには、(有限の立場で?)無矛盾性を確認する
すまん、書き間違えたよん。
2.当該の形式体系が少なくとも「全くの無意味」ではないことを
保障するためには、(有限の立場で?)無矛盾性を確認する。
222 :
The_Knight_of_Mathematics ◆uGlSZOV4Kc :2005/09/29(木) 18:04:38
アルゴリズムのなかにも数学的性質が立ち現れてくるわけだから コンピューティングによる証明を否定するゆえはない 例えば ピタゴラスの定理の証明の一つなどで辺に接続する図形を移動することで証明とする場合を 否定するようなものだ 俺ってキングとは逆に幾何学大好きだから目で見てわかる証明のほうが美しいと感じる
223 :
132人目の素数さん :2005/09/29(木) 18:09:24
>>219 別に客観性なんてヒルベルトの関心にはなかった筈。
>一応、形式的に証明されれば客観的な訳で
しかし実際には、形式的証明は激しく読みにくい。
したがって「機械は正しいといってるがオレにはチンプンカンプン」
という状況がおきる可能性大。客観的というより「無観的」といった
ほうがいい。
224 :
132人目の素数さん :2005/09/29(木) 18:12:27
>>219 >1.定理の客観性を確保するために、形式体系内で証明を行う
これ普通に数学者がやってることなんじゃないの? ただ記号論理でやらないだけで。
225 :
132人目の素数さん :2005/09/29(木) 18:12:44
>>223 だから別に読まなくてもいいんだって、
それはコンピュータに読ませるための
証明なんだからさ
ユークリッド幾何を勉強するのに幾何
学基礎論を読まなくてもいいでしょ
勉強をして感覚を養うのと、正しさを
厳密に確認するのは、違う作業だって
ことはよく知ってるでしょ
226 :
132人目の素数さん :2005/09/29(木) 18:13:26
227 :
132人目の素数さん :2005/09/29(木) 18:16:14
228 :
132人目の素数さん :2005/09/29(木) 18:16:59
>>223 >別に客観性なんてヒルベルトの関心にはなかった筈。
集合論のパラドックスに端を発して、
数学(的定理?)の正しさを保障する
方法が必要であると考えたのが、常識
として「ヒルベルトの動機」だったと
いうことになってるよ
229 :
The_Knight_of_Mathematics ◆uGlSZOV4Kc :2005/09/29(木) 18:17:00
230 :
132人目の素数さん :2005/09/29(木) 18:20:42
>>227 だから、フェルマーの定理だってペアノ公理系から
(その肯定も否定も)導けるか、どうかは分かって
ないよ。数学者が証明したということと公理系から
形式的に導けるということは別物なの。
これが分かってないと、中村教授の「完全証明」と
いう言葉で誤解をしてしまう素人さんの一人に入る。
231 :
132人目の素数さん :2005/09/29(木) 18:21:11
>>225 >だから別に読まなくてもいいんだって、
>それはコンピュータに読ませるための
>証明なんだからさ
コンピュータを信頼する根拠は?
>ユークリッド幾何を勉強するのに
>幾何学基礎論を読まなくてもいいでしょ
それはむしろ君の主張を否定するもののような希ガス
>勉強をして感覚を養うのと、正しさを厳密に確認するのは、
>違う作業だってことはよく知ってるでしょ
理解せずに正しさを確認できるという発想は
どこか精神を患っている希ガス
232 :
The_Knight_of_Mathematics ◆uGlSZOV4Kc :2005/09/29(木) 18:23:30
コンピューターのなかに再現された座標系で パズルが噛み合うから証明できたよーんっていうようなものだろ ほら見ろよ 噛み合ってんじゃん!って その証明を否定しようにもスパコンひっぱってこなきゃならんし 20万行読まなきゃならんしで大変・・・ 今後はこういう証明が台頭する状況になっていくかと
233 :
132人目の素数さん :2005/09/29(木) 18:25:17
>>230 >ペアノ公理系から
なんでペアノ公理系からなの?
集合論の公理系でいいじゃない。
そこからフェルマーは証明されてんでしょ。
234 :
132人目の素数さん :2005/09/29(木) 18:28:43
>>230 ああ、いろいろ使ってるからなあ。
しかし、素人の誤解とかいう時点で
君も玄人の誤解に陥ってるな(w
235 :
132人目の素数さん :2005/09/29(木) 18:30:13
>>231 >理解せずに正しさを確認できるという発想は
>どこか精神を患っている希ガス
別に理解しなくても。「正しさだけなら確認」
できる。というのが、ヒルベルトの形式主義。
もちろん、それに対して貴方がどう思うかは、
自由だよ。
ま、単に「正しい」という言葉で意味しいてる
事が違うだけと思うが
ただ、「君の考える正しさ」は、主観的にのみ
確認できるものだと思うけど。それはプラトニ
ズムだな。もちろん、そういう立場もあるよね
236 :
132人目の素数さん :2005/09/29(木) 18:31:26
>>233 >集合論の公理系でいいじゃない。
それも分かってないけど
237 :
132人目の素数さん :2005/09/29(木) 18:33:30
>>236 はあ? それじゃ証明されてないんじゃない。
238 :
132人目の素数さん :2005/09/29(木) 18:33:39
239 :
The_Knight_of_Mathematics ◆uGlSZOV4Kc :2005/09/29(木) 18:34:18
お前らずいぶん哲学的だな 俺にはもうついてけんよ
240 :
132人目の素数さん :2005/09/29(木) 18:36:04
>>234 だから、「基礎論の初歩」を知っている数学の先生に
聞いてみな、ね
この「中村氏の完全証明」と「普通の証明」の違いが
分からないんですけど、どういうことですか?、って
結論から言えば、「普通の数学者の証明」は形式的に
証明できるということとは違うんだ、って答えになる
241 :
132人目の素数さん :2005/09/29(木) 18:40:15
>>235 >別に理解しなくても「正しさだけなら確認」できる。
>というのが、ヒルベルトの形式主義。
違うなあ。「理解しなくても」「確認できる」なんていうのは
君が勝手にそう思ってるだけのこと。
実際には数学の理屈は文字の操作に完全に還元できるという発想。
まあ、唯名論だな。
しかしこれは大きな落とし穴がある。
つまりそもそも文字操作として表した形式化が正しいかどうかは
分からんってこと。だから実は理解ぬきには客観性なんかないって
ことさ。論理マンセーの素人が必ず陥る初歩的な穴だな。
242 :
132人目の素数さん :2005/09/29(木) 18:40:19
>>237 だから、中村氏の発言になるんでしょ?
ジョルダンの曲線定理は、数学者の言う普通の意味では
証明はできていたけど、形式的証明はできていなかった。
今回、我々はそれに成功したぜ
って言っているの。
>>236 君はもしかしてワイルズの証明はどこかで
公理に拠らない直観を使用しているかもしれないから
計算機で確認するまで証明されたとは認めないつもりかな
おかしな人だなあ、というのが普通の数学の人の反応な訳だけど
ちなみにFermatの最終定理みたいな数論的な定理は、 たとえ証明の途中で集合論的な選択公理を援用したにせよ、 原理的には証明からそのような除去できる、って定理があったから かなり弱い公理から導けると思って間違いないかと
245 :
132人目の素数さん :2005/09/29(木) 18:44:05
>>241 いまどき、基礎論なんて古臭い言葉を繰り返す奴は
ロジックの初歩も知らんというのが相場。
こっちは、ロジシャンから聞いたこと書いてるんだよ。
246 :
132人目の素数さん :2005/09/29(木) 18:45:50
>>240 >結論から言えば、「普通の数学者の証明」は形式的に
>証明できるということとは違うんだ、って答えになる
それは程度問題じゃないの。本質的違いじゃなくて。
だから今回みたいに数学者の証明を書き下していけば機械に通るわけで。
247 :
132人目の素数さん :2005/09/29(木) 18:46:08
いまどき、基礎論なんて古臭い言葉を繰り返す奴は マジックの初歩も知らんというのが相場。 こっちは、マジシャンから聞いたこと書いてるんだよ。
>>240 あのねえ、普通の数学者は、原理的には時間をかければ
計算機で検証可能なレベルで、厳密に定理を証明できるだけの能力は持ってるよ
(まあ幾何学者とか一部あまり厳密で無い人も居るけど)
単に時間が無駄だからそうしないだけでね
249 :
132人目の素数さん :2005/09/29(木) 18:46:45
>文字操作として表した形式化が正しいか そこは問題にしない、というのが形式主義だろ? 君がその考えは取りたくないというのは勝手だよ しかし、それだとどこにも客観性はないが。別に そういう立場はありだ、と思うよ。でも、それは 貴方の考えで。いろんな考え方があるの。 形式主義の考え方ならこうなるよ、って言ってる。 で、中村の完全証明っていうのは、そう言う話だ。 それに価値があるか、どうかは人それぞれの価値 観だ。俺も「ジョルダンの曲線定理の形式証明」 自体にそんなに価値がある、とは思ってないけど。 これは俺の個人的価値観だから。
250 :
The_Knight_of_Mathematics ◆uGlSZOV4Kc :2005/09/29(木) 18:46:58
数学教師:「いいかお前ら!」 平面上の閉じた曲線は、 ↓ ○ ↑ 平面を曲線の内と外に分ける これが「ジョルダンの曲線定理」だっ!!! 生徒→ ('A`)「・・・・」
251 :
132人目の素数さん :2005/09/29(木) 18:49:13
>>248 激しく勘違い。もう君は駄目だ。「基礎論の初歩」を知ってる
普通の(基礎論でない)数学者に聞いてみろよ。直接
やっぱり公式見解が必要かな。こういう勘違い君がいるとこを
見ると。どうにかしてくれって感じだが
252 :
132人目の素数さん :2005/09/29(木) 18:50:23
>>文字操作として表した形式化が正しいか >そこは問題にしない、というのが形式主義だろ? 重大な間違いだな。誰もそんな馬鹿げたことはいっていない。 >しかし、それだとどこにも客観性はないが。 君が間違ってる。むしろ問題にしないほうが客観性がない。 そういう立場は君だけの主観的なものだな。他人には通用しない。 君の同類には通用するかもしれないが、具体的な事例になると 君と君の同類の見解はことごとく相違し、了解がとれなくなるだろう。 要するにコミュニケーションを否定した独我論に陥ってるわけだ。 プライドばかり強いとそういう馬鹿げたことになる。
253 :
132人目の素数さん :2005/09/29(木) 18:52:44
>>251 だから、君のいう「基礎論の初歩」は間違いだよ。
まったく素人に限って勝手に自分の中に似非専門家を
つくるから困ったもんだ。素人が即座に専門家に
なれるわけがないだろ。
254 :
132人目の素数さん :2005/09/29(木) 18:55:36
>>252 何だか、数学の話じゃなくなってるんですが…
何だか、君は哲学的見解を主張されてるようで
数学者は「数学者同士で」、ある程度、共通の
主観を持っているから高度な数学の話が通じる。
実際、俺はそう感じているよ
255 :
132人目の素数さん :2005/09/29(木) 18:57:41
>>253 はあ?初歩なんだから、専門家じゃなくても分かっていても
可笑しくないだろ。
数学の専門家じゃなくても、数学の初歩を知ってる人はいる
よね。
256 :
132人目の素数さん :2005/09/29(木) 18:58:35
いるかはジョルダン曲線定理をしっているか
257 :
132人目の素数さん :2005/09/29(木) 18:59:10
>>254 >>249 の「そこは問題にしない」というのは数学じゃないよ。
>数学者は「数学者同士で」、ある程度、共通の主観を
>持っているから高度な数学の話が通じる。
>実際、俺はそう感じているよ
共通かどうかはともかくとして、実際には数学者自身の理解と
相互の了解が、数学の定理の正しさを根拠づけているという
主張は私自身がここでしてきたことで、いまさら君の主張だと
言い張られても迷惑なんだが。
258 :
132人目の素数さん :2005/09/29(木) 19:01:22
>>255 いや、初歩だから、素人が誤解しても可笑しくないんだよ。
見当違いのことをいう人は、たいてい初歩からダメだよね。
君がそう。どうせ独学だろ?だから誤解したまま気づかないんだ。
独学は結局自慰だからな。
>>251 勘違いしてるのは君だよ
俺は別に数学の普通の論文がどれくらい論理的に緻密に
書かれてるか、なんてことは主張して無い
ただ書こうと思ったら書けるよ、と言ったまでのこと
260 :
132人目の素数さん :2005/09/29(木) 19:04:04
>共通かどうかはともかくとして、実際には数学者自身の理解と >相互の了解が、数学の定理の正しさを根拠づけているという >主張は私自身がここでしてきたことで、いまさら君の主張だと >言い張られても迷惑なんだが。 だから、それが数学者が普通の意味で言う証明です。 それと、「形式的証明」は違いますよ、って言う話 なんだがなあ。それは分かるでしょ。 俺は、普段、形式的証明なぞ全くしないし、貴方の 定理は(かくかくしかじかの形式体系で)証明でき ますか?と聞かれたら、「全く分かりません。どう なんでしょう?」としか、答えようがないよ。
261 :
132人目の素数さん :2005/09/29(木) 19:05:39
形式的証明する奴いる?
262 :
132人目の素数さん :2005/09/29(木) 19:10:17
>>261 普通はしない。それに普通の証明したからって、
それで形式的に証明できるのか、どうかなんて、
全然、分からないよ
で、今回、中村は形式的に証明できましたって
話でしょ。
もし、今までの数学者の証明=形式的証明なら
中村の「初めて」って話は嘘になるけど、俺は
嘘だと別に思わないな
「云うまでもないが、人間の推論構造はしなやかである。 一階の述語論理が人間の推論様式を全般に渡って記述しうるというのは 十分な検証を要する一種のドグマである。」 by 某W先生 「一階の述語論理」の部分を「NBG集合論」にしてみたり、 「人間の推論様式」の部分を「数学者の推論様式」にしてみると、 >書こうと思ったら書けるよ ってのは楽観的すぎかなとも思う。
>>262 まあ初めて「形式的に証明」できました、じゃ無くて
初めて「完全証明」できました、なんて言っちゃってるけどな
>>263 まあそりゃそうだね
266 :
132人目の素数さん :2005/09/29(木) 19:19:22
ジュルダンの曲線定理は、数学的にはとっくに証明されているね しかし、「形式的証明」は今回、初めて我々の手によって与えら れましたって言うんだから 結局、ジュルダンの定理の「普通の証明」と「形式的な証明」は 違うわけで
267 :
The_Knight_of_Mathematics ◆uGlSZOV4Kc :2005/09/29(木) 19:28:29
>>266 ジョルダンの曲線定理とジュルダンの定理はどう違うんだ?
268 :
132人目の素数さん :2005/09/29(木) 19:32:02
「数学者の言う普通の証明」と「形式的証明」は、別物 ジェルダンの曲線定理の「普通の証明」なら、とっくに あった、でFA。
269 :
132人目の素数さん :2005/09/29(木) 19:33:30
>>266 >結局、ジュルダンの定理の「普通の証明」と「形式的な証明」は
>違うわけで
誰も同じとは思ってないだろ。
だけど、これは量の問題であって質の問題じゃないだろ。
他の証明、例えばフェルマーの定理の証明だって時間と手間を
かければ形式証明が出来るだろう。そんなことは昔からわかってることだろう。
少なくともあるところで1年も2年もひっかかりそうな気はしないよね >ポーランドの数学者ら16人との約14年間にわたる共同作業 って14年間も何してたんだろ
271 :
132人目の素数さん :2005/09/29(木) 19:43:06
>フェルマーの定理の証明だって時間と手間を >かければ形式証明が出来るだろう。 その肯定が形式体系から証明できるか、どうかは 分かりません。 ただし、その手の専門家によれば、今までの経験 から予想するに証明できる公算が高いのではない か、という噂なら聞いたよ 「時間と手間を掛ければ、形式的証明ができる」 ことが分かってるなら形式式証明ができてるのと 同じことじゃないか? でも、少なくともジョルダンの曲線定理は、そう じゃなかったよね。ということは「数学者の言う 証明」は「形式的証明」では必ずしもないという ことだ。 で、ワイルズのフェルマーの定理の証明が形式的 証明だと言う根拠は何なの? 数学者が「形式的証明」であると言ってたかな?
272 :
132人目の素数さん :2005/09/29(木) 19:46:15
だから、まだ形式的に証明できていないなら、 形式的に証明できるか、どうかは分からない よね 形式的にも証明できそうだ、という「予想」 することは何ら問題ではないけどね
273 :
132人目の素数さん :2005/09/29(木) 19:49:29
>例えばフェルマーの定理の証明だって時間と手間を >かければ形式証明が出来るだろう。そんなことは、 >昔からわかってることだろう。 何が分かってるの?フェルマーが証明されたのは最近。 今もまだ形式的な証明ができるかどうかは分からない。 基礎論の専門家の間では、できるのではないか?、と 予想されているという噂は聞いたよ。
あのねえ、君は数学の厳密性を舐め過ぎだって 誰もWilesの200ページ弱の証明がそのまま形式的証明だなんて言ってないだろ? そんな勘違いをしてるのは君だけ >でも、少なくともジョルダンの曲線定理は、そうじゃなかったよね。 実際に形式的な証明が出来ただろ? 「直感的には当然だが、誰も数学的に完全な証明ができなかった」 なんていってるのは中村教授とそのお仲間だけで 平地健吾だって小島定吉だって、オリジナリティの低い低レベルな結果だ、と 内心考えてると思うよ
275 :
132人目の素数さん :2005/09/29(木) 19:54:54
>>269 >そんなことは昔からわかってることだろう。
分かってる、ということは
仮定:数学者が(数学者じゃなくてもいいが)こうこうこう言う風に証明
⇒
結論:その定理は形式的に証明可能
という定理でもあるのかい?そんなのがあったら
教えて欲しいなあ。で、ワイルズの証明が、その
定理の仮定を満たしてる事も確認できてるのかな
276 :
132人目の素数さん :2005/09/29(木) 20:00:02
>>274 >実際に形式的な証明が出来ただろ?
ジョルダンの場合はね。他の定理もそうだ、というのは
どうして分かるんだい?
分かるというなら『「普通の証明」⇒「形式的証明」』
という定理が成り立つんだよねえ。
つか、その前に「普通の証明」というのを数学的に定義
しなきゃならんがwww
>>269 はそんな定理があるなんて言ってないだろ
単に、必要があれば、充分形式的なレベルまで証明を緻密にする
自信がある、というだけだろ
証明の形式化のどの部分がそんなに難しいと考えてるのかな?
少なくともZFCの公理から、必要な諸概念を定義して、
完全に形式的に証明するのは、述語論理の基礎を理解している数学者には
簡単なことだと思うがな
今回14年掛かったことだって、単に能力が欠けていた、としか思われない
278 :
132人目の素数さん :2005/09/29(木) 20:06:18
せいぜい分かるのは、「数学者によって証明されている定理」の ほとんどは「形式的にも証明できる」だろう、という予想でしょ。 よく考えたらゲーデルの第二不完全性定理があるじゃん。 「無矛盾性を意味する(とある)命題」が正しいけれども、 それは形式体系では証明できないって定理だね。
>>276 他の場合も出来るはずだ、という強い確信があるだけだよ
もちろん確実な根拠なんて無いわけだが、
それは、集合論の公理系は矛盾しているかもしれないのに、
実際には現今の数学者は、そんな可能性微塵も考えずに、
無矛盾に決まっている、その無矛盾な集合論で基礎付けできる現在の数学も
無矛盾だろう、と判断して研究を進めるのと同じことでしょ?
それを、無駄に不安を煽るのは、昔杞の国の人が、
天が崩れて落ちてきたらどうしようと憂いて夜も眠れなかった、という故事と一緒で
単なる無駄な取り越し苦労だと考えるべきかと
280 :
132人目の素数さん :2005/09/29(木) 20:11:23
>単に、必要があれば、充分形式的なレベルまで証明を緻密にする >自信がある、というだけだろ 何だ、自信の話ですか。それは「かくかくしかじかの定理」は 形式的にも証明できると私は予想しています、って話だね。 予想することと、確認することは別だよね。
281 :
132人目の素数さん :2005/09/29(木) 20:12:41
>>279 他の場合って、どの場合よ。現に出来ないものを
ゲーデルは見つけたでしょ?
>>278 それがどうしたの?
もしかしてそれが
>「数学者によって証明されている定理」の
>ほとんどは「形式的にも証明できる」だろう、という予想
に対する反例になると考えているのかな?
君はゲーデルの第二不完全性定理を理解していませんね
そもそもその文脈で挙げるのは第一不完全性定理で充分なはずだけど
>>277 そりゃ手でやりゃあ 14 年もかからずできるさ
問題はどうやって数学的概念を計算機に理解させるか.
俺らが何気なく定義するようなものも,直感(というよりも常識)が多分に入るから,
それを計算機に理解させるためにたくさん手続きが必要になる.
だいぶ基本的な定義が出来上がった後でも,「領域が有界」であることを定義するために
120個も条件連ねなきゃならんのだから,全部証明するのに苦労するかは押して知るべし.
284 :
132人目の素数さん :2005/09/29(木) 20:19:22
>>279 別に「形式的証明」がなくても不安じゃありませんけど。
というか、形式的証明ができない事が分かったとしても
不安じゃないよ
無矛盾性の証明は形式的に証明できないね。でも、不安
じゃありません。自分の定理が、仮に「形式的に証明」
できなかったとしても不安ではありませんね。
その否定が形式的に証明されたのなら、俺って馬鹿、と
思うだろうけど。そんなことをする暇人はいないから、
気にしてないけどね
285 :
132人目の素数さん :2005/09/29(木) 20:23:07
>「数学者によって証明されている定理」の >ほとんどは「形式的にも証明できる」だろう、という予想 に対する反例になると考えているのかな? はあ?反例って、予想って書いたけどさ、これは 数学的な定理じゃないよね。 「ほとんど」ってあるよね。これって、数学的な 定義になってないじゃんか? だから、この予想って書いたけど、これはただの 感想だから。反例も証明もあるわけない。人それ ぞれの感想だからさ
第二不完全性定理はさ、(自然数論を含む)数学の形式的理論Tが (無矛盾で、再帰的に公理化可能ならば、) その体系の無矛盾性とメタレベルで同値になる、従って直観的には真となるはずの 命題ConTが、【その体系内では】証明できない、という定理でしょ? だからその体系内でその定理がたとえ証明できなくても、 適当に公理を付け加えた体系T'では普通に証明できて何も困らない だから計算機で検証不可能な定理の存在を示していることにはならないよね だから >現に出来ないものをゲーデルは見つけたでしょ? これは君の明らかな勘違い
287 :
132人目の素数さん :2005/09/29(木) 20:25:15
だから、仮に誰かが >「数学者によって証明されている定理」の >ほとんどは「形式的にも証明できる」だろう と言ったとしても、これはその人の感想を述べただけね
>>285 予想に反する例、「ほとんど」に当てはまらない例、と言わないと分かって貰えないかな
289 :
132人目の素数さん :2005/09/29(木) 20:27:32
>>286 >適当に公理を付け加えた体系T'では普通に証明できて何も困らない
それは分かってる、ってば。
でもさ、「証明したい定理を公理に加えた体系T'」では、その定理は
証明できるよねwww
>>289 そうだよ
だからどうしたの?
じゃあ
>>281 の>現に出来ないもの
って何のことだよ?言ってみてくれよ
291 :
132人目の素数さん :2005/09/29(木) 20:31:05
>「ほとんど」に当てはまらない 当てはまるか、当てはまらないか、はどうやって決めるの? >予想に反する 予想に反してないか、どうか、は? ただの感想ですか?
292 :
132人目の素数さん :2005/09/29(木) 20:35:14
>>290 どうやら、終わったみたいだね。
だから、「無矛盾性を意味する(とある)命題」が
その形式体系では証明できないってこと。
「無矛盾性を意味する」というのは、ここでの話し
ではあまり関係ないがな。
>>291 形式的に証明できれば当てはまるし、予想に反しない、
形式的に証明できないものは当てはまらないし、予想に反する
それくらい文脈から明らかだろうに
>>281 によると
>現に出来ないものをゲーデルは見つけたでしょ?
だそうだから、その「現に出来ないもの」が予想に反するんじゃないかな
それと、数学的なstatement以外を全て「感想」で片付けるのは
止めてくれないかな
別にこのスレはひたすら数学的な定理と証明を書き込むスレじゃないんだからさ
294 :
132人目の素数さん :2005/09/29(木) 20:42:18
結論←かなり常識的でつまらないけど >ある定理を正しいと認めた数学者が、 >その定理が成り立つ適当な公理系が >何であるか?についてまで分かって >いるとは限らないよ。 もちろん、適当でなければ、いくら でも思いつくよ。例えばその定理を 定理を含んだ公理系とかね。www
295 :
132人目の素数さん :2005/09/29(木) 20:43:24
基礎論系のスレはいつもおんなじネタで議論になるね 頼むから名前欄に仮のハンドルをつけてくれ
296 :
132人目の素数さん :2005/09/29(木) 20:48:25
>ある定理を正しいと認めた数学者が、 >その定理が成り立つ適当な公理系が >何であるか?についてまで分かって >いるとは限らないよ。 で、ジョルダンについては、ごくごく常識的な 公理系で形式的に証明できました、ということ でしょう もちろん、これも感想だけどさ。何か異論ある 感想を否定はしてない。感想は感想に過ぎない というだけのことだよ。
とりあえず一人 age 続けてる基礎論厨さんは名前付けて sage て返信先にアンカー(>>xxx)張ってください
298 :
132人目の素数さん :2005/09/29(木) 20:51:34
>俺は、普段、形式的証明なぞ全くしないし、貴方の >定理は(かくかくしかじかの形式体系で)証明でき >ますか?と聞かれたら、「全く分かりません。どう >なんでしょう?」としか、答えようがないよ。 これも結論だね。感想だけどさ。
299 :
132人目の素数さん :2005/09/29(木) 20:55:03
俺は、296=298だけど、基礎論厨ではない。 普通の数学をやっているから。 で、自分が証明した定理が成立する適当な「形式 体系」なぞさっぱり分からないね。それで不安に なったりはしないよ これも感想だ
300 :
132人目の素数さん :2005/09/29(木) 20:55:38
あぼ〜ん
Jordan曲線定理が、ごくごく常識的な公理系から 証明できる、というのは大昔に数学者が確認したことなんだよ 今回の「完全証明」とやらの意義は、Jordan曲線定理を証明するのに 必要な公理の強さを確定したとか言うことじゃなくて、 proof checkerが、実用化に近づいた、ということだろ
302 :
132人目の素数さん :2005/09/29(木) 21:00:28
>Jordan曲線定理が、ごくごく常識的な公理系から >証明できる、というのは大昔に数学者が確認した >ことなんだよ じゃあ、その体系で形式的に証明されてたんだね。 ホント?
>ある定理を正しいと認めた数学者が、 >その定理が成り立つ適当な公理系が >何であるか?についてまで分かって >いるとは限らない しかし、集合論的な一部の数学を除けば、ZFCの範囲で大体事足りる 事足りない場合でも、基本的には、ZFCから独立かどうかを判定する ための一般論は確立されている、というのが 常識的な数学者の所信(君の言う「感想」w)だと思うがな そう思わないとしたら、基本的に感覚がずれている
>>302 何が「じゃあ」なのか分からないが
まだ形式的な証明と、普通の数学者の証明の区別も付かないのかなあ、、
もう説明する気無いよ
305 :
132人目の素数さん :2005/09/29(木) 21:04:10
>>301 俺は自分の証明して、論文に発表した定理が、
「適当な公理系から形式的に証明できること」
なんて全く確認してない。他人の論文を読む
ときもね。
形式的に証明できることなんて、普通の数学
者は全然、確認しないと思うが?
306 :
132人目の素数さん :2005/09/29(木) 21:06:26
>>304 だから、違うんでしょ。違うなら
普通に証明したからって、形式的に証明できるか
どうかは、分からないよね
307 :
132人目の素数さん :2005/09/29(木) 21:07:10
はいはい、結論が出ました! >普通に証明したからって、形式的に証明できるか >どうかは、分からない
形式的証明に拘ってる一名は放っておいてプルーフチェッカーについて話そうぜ
とりあえず
http://mizar.org/fm/ と20万行目に目を通したんだけど,ほとんど全てが
定式化のための定式化で冗長としか思えんかった.
知識蓄積する以外になんかこのあたり簡単にできんかな?
>>305 多少論理学の知識があれば、形式的に証明するのは簡単そうだ、
と分かるはずだから問題ないよ
何で名前入れないの? PCにWebブラウザのクッキー情報が残ると、なんか不都合なことでもあるの?
311 :
132人目の素数さん :2005/09/29(木) 21:09:23
>普通に証明したからって、形式的に証明できるか >どうかは、分からない ジョルダンの定理は普通に証明されていたが、今回、 形式的に証明がなされた、ということでいい訳だね
>>308 Goedelがある論文の中で
これこれのformal proofは、まともに書くと長くなるが、
これこれメカニズムを入れれば、短縮できる、みたいな
証明工学なことにも触れているのは流石だ、と言って
林晋が褒めてたかと
もうそのページ消されたのでInternet Archive探さないと残ってないっぽいけど
313 :
132人目の素数さん :2005/09/29(木) 21:15:30
>>309 全然、思わないがな。それに「公理系」と「定理」の
採用の仕方によるね。普通の数学者は、どんな形式的
体系で、どんな命題に置き換えるかなんて、意識して
ないと思うが。
だから、お前らの言っていることは、多くの場合には
数学者の証明を見ると適当な公理系と定理に対応する
適当な命題を思いつく自信があるよということでしょ。
君の感想だよね。別に、否定するつもりはないけどね。
ってちょっと違うな.もうちょい探してみます
316 :
132人目の素数さん :2005/09/29(木) 21:21:25
結局、「基礎論屋」と「普通の数学屋」の感想の違いだったみたいだね。 もう一度、書いておく。 >自分が証明するときに形式的に証明されるか、どうか、なんて >気にしちゃいねーよ。だから、形式的に証明できるか、どうか >なんて分からないし、仮に形式的に証明ができないものだった >としても、気にしないね。普通に証明できればOKだ。
>ゲーデルの論文では、定義とは、省略記号なのだということで通してあります。 >しかし、さすがゲーデルというか、そういう定義を完全に展開してしまうと >扱っている論理式が非常に大きくなるだろうとか、Principia Mathematica のよう、 >定義のメカニズムが入っていれば、短くなるが、などの証明工学的な話もちゃんと議論しています。 >前原先生がイオタ記号を使われたのは、ここら変を曖昧にしておくのが嫌だったからでしょう。 ここらへんのことです 論理式の長さ、でしたね、失礼 まあ証明の長さにも同じことは言えると思いますが
>>316 だから>仮に形式的に証明ができないものだった
そんなものがあるかもしれないと信じてる数学者は殆どいねえっていうのに
>>306-307 を見てレスする気力がなくなったけどね
319 :
132人目の素数さん :2005/09/29(木) 21:31:43
>>318 具体的に「定理と公理系」を特定しなければ、
形式的に証明できるとか、できないとかが、
意味を持たないだろう。
ということは、「そういうものがある」という
のもただの感想だし、「そういうものがない」
というのもただの感想にしか過ぎないね。
君は感想を言ってるんだ。俺もだがな。自覚し
ようぜ
320 :
132人目の素数さん :2005/09/29(木) 21:33:03
その定理を公理として含む公理系を考えれば、 その定理は形式的に証明できるからな。
>>317 Principia Mathematica のようなメカニズムって,数々の省略記号のことかな?
だとしたら相当楽観的な判断に思えるんだがなあ.
322 :
132人目の素数さん :2005/09/29(木) 21:36:48
>>318 少なとも、俺はあると思うぜ。
ない、と思う奴もいるだろう。
いずれにしても、どちらも間違ってない訳だ。
ということは「意識調査」の問題だな。
各国の数学者に「意識調査」をして見るのも
いいかもしれないね。時代とか、国によって
どう変わるかとかね。ちょっと見てみたい。
323 :
132人目の素数さん :2005/09/29(木) 21:42:57
1.「普通の証明」と「形式的証明」は違う → これは共通認識 2.「普通に証明できてるものは『適当な』公理系で形式証明可能」 いや、「できないものもある」 → どちらを考えるにしても、ただの感想。正しい、間違って いるの問題ではない。因みに、俺は「できない派」だけどね。
324 :
132人目の素数さん :2005/09/29(木) 21:44:28
>>323 『適当な』という部分が個人の主観だからね。
>>319 だから「確信、所信」を「感想」に変えないでくれないかな
意味が違う言葉だからさ
>>323 具体的にはどういう定理がそうなると思うのかな?
まさか具体例は無い、なんてことは無いだろうけど
326 :
132人目の素数さん :2005/09/29(木) 21:50:37
普通に証明できてる定理の中に、『適当な』公理系で形式主義的に 証明ができない定理がある と俺は思う。もちろん、これはただの感想。『適当な』というのが 個人的主観だから
327 :
132人目の素数さん :2005/09/29(木) 21:53:19
>>325 >だから「確信、所信」を「感想」に変えないでくれないかな
>意味が違う言葉だからさ
意味が分からないな。だって、普通の意味で反証可能命題では
ないじゃない。ということは、感想だろが?
確信という言葉は、反証可能な命題でなければ意味ないぜ
あんたの言うことの意味が分からない
329 :
132人目の素数さん :2005/09/29(木) 22:05:34
>普通に証明できてる定理は、『適当な』公理系で形式主義的に >証明可能 これは感想とか、意見の類でしかないよね。ご自由にどうぞ 俺の意見は、「証明不可能なものもある!」だ。というか、実は どっちでもいいんだけどね。 俺が本当に言いたいことは、「それって、どちらにしても、結局 意見にしか過ぎない!」ということ
330 :
132人目の素数さん :2005/09/29(木) 22:09:52
>>328 確信って、「正しいか、間違ってるかが決まる」ことに対して
言うんでしょ。決まらないことに言うのは、ただの意見だよ。
というか、どちらも正しい訳だから矛盾が許容される世界での
「おしゃべり」だね。それも、結構だと思うよ
こっちは経験を根拠にほとんど確実にできると主張してるんだから、 あんたは不可能なものがあると信じる根拠を挙げなきゃ意見未満だよ あと確信ってのは正しいと信じていること。決まるかどうかとは無関係。 さらに言えばあんたの立場では決まらないかどうかもわかんないでしょ?
332 :
132人目の素数さん :2005/09/29(木) 22:16:25
>>331 意味が分からない。だって、「適当な」って言うのが
完全な個人の主観じゃない。
決まらないよ。何度も言うように「適当な」ってのが
主観だからね。
ここをどうするのよ。もちろん、そこを定義すれば、
決まるかもね。
実は、定義があるのかな?www
日常言語に数学的な定義を求める阿呆が一匹居ますね 工房でしょうか スルーが吉かと
334 :
132人目の素数さん :2005/09/29(木) 22:19:25
>>331 「適当な」ってままじゃ、何を言っても意見だよ。
君の経験に基づく感想だ。
だから、「意識調査」でもしようぜ、な
適当な、ってのは、ageてる人が自分の逃げ道を残すために 一方的に使ってる言葉だよ よく読んだほうがいいよ
336 :
132人目の素数さん :2005/09/29(木) 22:23:58
>>333 あれ?今、数学のことを話てるんだよね。
数学で「適当な」というだけで、定義が
なければ、それはまだ意見でしょ。もち
ろん、今後、定義がなされて定理になる
可能性を秘めた意見もある。でも、
>普通に証明できてる定理は、『適当な』公理系で形式主義的に
>証明可能
なんての、上手く定理に出来るもんかね?
>>336 んなこたーない.論文とかで「適当な仮定の下で」ってj表現見たこと無い?
数学で「適当」って言ったら,妥当な条件が共通知識としてあるものだよ?
339 :
132人目の素数さん :2005/09/29(木) 22:27:59
>>335 >その定理を公理として含む公理系を考えれば
>その定理は形式的に証明可能である
正しいねえ。
340 :
132人目の素数さん :2005/09/29(木) 22:32:07
>>338 うんうん、あるね。それは、「条件」を明確に
あげることが出来る場合だよね。じゃあ、頑張って
>普通に証明できてる定理は、『適当な』公理系で形式主義的に
>証明可能
の「適当な」も明確な条件に置き換えてみてよ。もしも出来たら
いい仕事じゃないの?うんうん、すごいねwww
>>336 数学をすることと数学について話すことの区別も付かないのかなあ
しかもお前が言い出した良くわかんない命題を
なんでうまく定理にしないといけないのか
>>323 のできない例って具体的にどういう場合を想定してるのか
いい加減教えてくれよ
数学で証明できるものには範囲がある。
343 :
132人目の素数さん :2005/09/29(木) 22:51:43
>>341 だから、命題じゃないんでしょ。じゃあ、
意見でしょ。自分で認めたのね。
いや、それとも何か別の命題があるのかな
別に数学的な命題じゃなくてもいいけど。
物理的命題もあれば、医学的命題もある。
いずれにしても、命題は正しいか、正しく
ないかが決まるものだけどね。
直感をある程度使ったスマートな証明の方が、厳密すぎる証明よりもカッコいいと思う。
345 :
132人目の素数さん :2005/09/29(木) 22:58:25
>できない例って具体的にどういう場合を想定してるのか >いい加減教えてくれよ 「たくさん、あるんだから、その中にはあるんじゃね」って 感じの話だ。感想だけどね。 喩えて言えば「宇宙は広いから地球以外に生命体がいても、 いいんじゃね」というような感想。この場合、まだ、生命体 とかに一応の定義ができそうだから、まだ命題っぽいけど。 それに比べても、 >普通に証明できてる定理は、『適当な』公理系で形式主義的に >証明可能 こっちは、全く命題になってないから、どうしようもない。どう あがいても、感想だ。 もしも君が感想以上のことを言いたいなら、どうぞ言って下さい よ。
>「宇宙は広いから地球以外に生命体がいても、 >いいんじゃね」 今数学の話してたんじゃ無かったのか? 物理や生命科学が、形式的に証明できると思ってるのか?
347 :
132人目の素数さん :2005/09/29(木) 23:01:26
あ、もちろん、「感想を言い合う」ことに意味がない なんてことは、思ってないよ。 だから、「意識調査」を見てみたい気もするんだよね。
>>345 あのですね,
>普通に証明できてる定理は、『適当な』公理系で形式主義的に
>証明可能
は,あなたが
>>329 で引用として持ち出したわけですけど,その原文は
どこにも無いわけですよ.あなたが勝手に妄想で持ち出した引用文なわけですよ.
勝手に人の主張を捏造しないでもらえますか?
数学的なstatement以外の相手の全ての主張を 「感想」の一言で片付ける 自分はというと都合が悪くなったら突然 数学の話をそらして宇宙の生命体の話をしだす こいつ頭が悪すぎる 駄目だ
350 :
132人目の素数さん :2005/09/29(木) 23:05:06
>>346 形式的に証明できなくても、数学的に証明できなくても
科学的命題というのはあるよね。分からないかな?
>「宇宙は広いから地球以外に生命体がいても、
>いいんじゃね」
これは、宇宙とか生命体があやふやだから、命題と
して不十分だと思うよ
351 :
132人目の素数さん :2005/09/29(木) 23:06:25
>勝手に人の主張を捏造しないでもらえますか? だから、さっきから言ってるでしょ。 貴方の感想でない主張はどこにあるの?聞かせて
一応初出は
>>326 かな
適当な、という言葉を二重括弧で括って
自分勝手な意味で使ってますよ、ということをアピールしてたから
誰もその発言には突っ込んでない訳なんだけどな
354 :
132人目の素数さん :2005/09/29(木) 23:09:59
>数学的なstatement以外の相手の全ての主張を >「感想」の一言で片付ける すべてではないよ。たまたま、ここでは感想以外のものが 見当たらないだけ。
355 :
132人目の素数さん :2005/09/29(木) 23:11:13
356 :
132人目の素数さん :2005/09/29(木) 23:12:24
はいはい、感想以上の主張は? 書いてみて
>>354 >>343 で
>命題じゃないんでしょ。じゃあ、 意見でしょ。
とあるのであんたの中では 「not 命題 ≡ 意見」 と判断されても仕方が無いわけだが
ところで意見と感想は同じ?
358 :
132人目の素数さん :2005/09/29(木) 23:18:13
感想だからって、意味がないとは言っていない。 「誰々さんのこれこれというタイトルの論文は いいね」 これは感想だね。正しいとも、決まらないし、 間違ってるとも、決まらない。 でも、こうした感想には意味がある事もある。 また、それぞれの意見を持つ事は、自由だね。 対立する意見があったからと言ってどちらかが 間違っているという訳でもない。
359 :
132人目の素数さん :2005/09/29(木) 23:19:15
360 :
132人目の素数さん :2005/09/29(木) 23:20:22
>>357 not「命題 ≡ 意見」
これは当然です。
361 :
132人目の素数さん :2005/09/29(木) 23:25:50
>>358 「普通に証明できてるものは『適当な』公理系で形式証明可能」
いや、「できないものもある」
→ どちらを考えるにしても、ただの感想。正しい、間違って
いるの問題ではない。因みに、俺は「できない派」だけどね。
362 :
132人目の素数さん :2005/09/29(木) 23:27:59
>>361 対立した感想を持っているに過ぎず。どちらが
正しいとか、間違ってるとか、そういう話では
ないということ。分かるかな?
これに関する「意識調査」って、ないのかな?
>>359 >「普通に証明できてるものは『適当な』公理系で形式証明可能」
を言ったのはお前だろ?
>どちらを考えるにしても
も何も,そんなの考えてるのはお前だけ.
364 :
132人目の素数さん :2005/09/29(木) 23:33:45
>>363 じゃあ、貴方は何が言いたかったの?感想でも、命題でも
いいから聞かせてよ、ね♪
俺は「できない派」だよ!ちゃんと、見てくれてるかな?
365 :
132人目の素数さん :2005/09/29(木) 23:35:14
>>361 を見て!
>因みに、俺は「できない派」だけどね。
ってあるよね。
366 :
132人目の素数さん :2005/09/29(木) 23:36:16
結論をもう一度 >「普通に証明できてるものは『適当な』公理系で形式証明可能」 >いや、「できないものもある」 > → どちらを考えるにしても、ただの感想。正しい、間違って >いるの問題ではない。
>>366 おめでとう!あなたの勝ちです。よかったね!
というわけでここからは本題に戻ってプルーフチェッカーの話をしましょう。
368 :
132人目の素数さん :2005/09/29(木) 23:43:55
プルーフチェッカーに20万行入力するだけで1年かかったんじゃないか?
プログラミングの世界では常識的な行数だと思うけど
>>370 :
そうだったのか。。!
プログラミングに関してはHello Worldに毛が生えたような知識なもんで。。
参考のため, Windows で 5000万行
373 :
132人目の素数さん :2005/09/29(木) 23:56:20
面白さ>>>厳密性 有用さ>>>厳密性 基礎論の豚どもは、死ね!
375 :
132人目の素数さん :2005/09/29(木) 23:59:42
形式的証明は無意味。要らないよな 基礎論屋は、居なくていいよwww
376 :
132人目の素数さん :2005/09/30(金) 00:00:36
直観的証明>>>(壁)>>>形式的証明
それ以前にこの工学部の人は計算機屋であって基礎論屋じゃ無いわけだけどな
378 :
132人目の素数さん :2005/09/30(金) 00:04:05
証明工学って下らないな。死んでいいよ ハハハハハハ
379 :
132人目の素数さん :2005/09/30(金) 00:05:25
無意味、無意味。形式証明は無意味
380 :
132人目の素数さん :2005/09/30(金) 00:06:01
形式証明やってる奴は、死ね!
381 :
132人目の素数さん :2005/09/30(金) 00:20:59
>「普通に証明できてるものは『適当な』公理系で形式証明可能」 >いや、「できないものもある」 > → どちらを考えるにしても、ただの感想。正しい、間違って >いるの問題ではない。 どんな定理でも形式証明は可能なのだよ。いや、 どんな命題でも形式的証明は可能なのさ。なぜ なら、その命題を公理として含む形式的体系を 考えればいいから 君はこんな簡単なことも知らなかったのかいw 形式証明は必ず出来るのさ!
382 :
132人目の素数さん :2005/09/30(金) 00:22:43
>>381 出来ない、というのは「ただの間違い」だから。分かった?
>>381 君は基礎論の入門書でも読んだときに随分そこで引っ掛かったんですねえ
384 :
132人目の素数さん :2005/09/30(金) 00:25:18
すべての命題は形式証明が可能。わざわざ、数学者は 証明しなくてもいいのだ。すべての命題は証明できる
385 :
132人目の素数さん :2005/09/30(金) 00:28:20
1+1=2 :証明可能 ¬(1+1=2) :証明可能 すべては証明可能。だから、証明なんかしなくていいんだよ
386 :
132人目の素数さん :2005/09/30(金) 00:29:12
数学は矛盾している。それでいいwww
387 :
132人目の素数さん :2005/09/30(金) 00:41:23
終わったな、証明 証明は無意味だ!
388 :
132人目の素数さん :2005/09/30(金) 00:42:01
形式的証明=無意味 数学的証明=無意味
389 :
132人目の素数さん :2005/09/30(金) 01:11:22
>>17 MIZ→Tex(pdfだったかな?)は、あるよ。
それを論文の一部として出してたりしてたからね。
390 :
132人目の素数さん :2005/09/30(金) 01:12:28
普通の数学者は、適当な形式的証明があろうが、なかろうが どちらでも全く不安ではありません。 「適当な」というのに正確な意味がないけどねw つーかさ、ある形式体系で証明可能であったとしても、その 形式体系が無矛盾か、どうかは結局、数学者の主観に永遠に 留まるしかない。もちろん、その妥当性を検証し続ける事は 可能だが、いつまで立っても完全に肯定的結論は得られない。 主観的信念が強まるだけだ。そのような事が無意味だ、とは 言わないけど もっと言えば、当該の「形式的体系の価値」が主観的、相対 的なものに過ぎないから決着は永遠にありえない。あくまで 「一つの試み」だが「こんなもんで十分なんじゃないの」と 言う感想に留まるのみなのだ リップサービスとして、「初めて」の形式的証明である、と 言うのは良いことだよ。これは政治的価値判断の問題だけど
391 :
132人目の素数さん :2005/09/30(金) 01:13:54
>>389 pdfとtex、全然違うが???一体、何なの???
392 :
132人目の素数さん :2005/09/30(金) 01:16:39
>>391 MIZを、英語で書かれた数学論文(pdf)に自動変換します。
優れものです。w
texに変換できたらそれから自動的にpdfに直せるじゃん
394 :
132人目の素数さん :2005/09/30(金) 01:17:31
MIZを、英語で書かれた数学論文(TEX)に自動変換します。 優れものです。w
395 :
132人目の素数さん :2005/09/30(金) 01:18:31
396 :
132人目の素数さん :2005/09/30(金) 01:19:59
つーか、証明工学屋って、専門家のつもりなんだろうけど 自分達がやってることも理解できてないみたいだね。
397 :
132人目の素数さん :2005/09/30(金) 01:26:13
でもさ、プルーフ・チェックが実用化されたら(そんなことあるか どうか知らんが)、証明問題の自習用とか、数学者が自分の証明の チェックに使えて便利だと思うね。でも別にプルーフ・チェックが 通らなかったからと言って証明に穴があるとは思わない。穴がある 可能性があると思うだけだ
398 :
132人目の素数さん :2005/09/30(金) 01:28:31
むしろ、プルーフ・チェックの通らない部分があるが、その 部分の証明には自信がある、という状態はなかなか気持ちが いいと思うね。
399 :
132人目の素数さん :2005/09/30(金) 01:30:17
所詮は工学屋。数学は素人
400 :
132人目の素数さん :2005/09/30(金) 01:32:09
あぼ〜ん
sage
>>391 いや、俺が単純に覚えてないだけ。
MIZ→TeX→PDFだったのか、MIZ→PDFだったのか、、。
最終的に、PDFになってたのだけは覚えてる。
オレの研究と全く関係ないのに、俺もやらされたよMIZAR。
ゼンゼンわからんかったけどね。工学の人間なんでオレ。
中村さんは、確か理学博士だったような、、、。
とりあえず、or(V)を、スラッシュとバックスラッシュ 「\/」で表現してたから、日本語環境だとYENに見えて、 見づらかったのだけは良く覚えてるわwww
404 :
132人目の素数さん :2005/09/30(金) 01:39:41
>>402 聞きたいのは、それって「普通の証明」に変換されるの?
それとも証明図とかになって出てくるの?
「普通の証明」になって出てくるなら、俺は面白いと思う
>>404 普通の証明だったと思うよ。
多分Webのどっかに落ちてるから、探してみるよ。変換例。
406 :
132人目の素数さん :2005/09/30(金) 01:42:43
やっぱ、普通の証明に変換するのは無理みたいだな。 「普通の証明→形式証明」に変換する以上に難しいと 思う。
407 :
132人目の素数さん :2005/09/30(金) 01:45:15
>>405 ほんとに?と言っても、「普通の証明」というのが
実は主観でしかないから
でも、よろしく頼むよ。それをいろいろな数学者に
見せて、感想を聞いてみるのは面白い、と俺は思う
普通の証明って日本語が含まれてるから まずAIを作らなきゃ駄目なんじゃ まだ、検索エンジンで無理矢理翻訳したみたいな 自然言語での証明を生成する方が楽かと
409 :
132人目の素数さん :2005/09/30(金) 01:46:53
410 :
132人目の素数さん :2005/09/30(金) 01:48:06
>>405 もし、そうならプルーフ・チェックも実用化も
そんなに絵空事でないような気もするね。
411 :
132人目の素数さん :2005/09/30(金) 01:56:02
>>409 サンクス。
>BOOLEってリンクの先がMIZAR記述で、Contents (PDF format)
うん。普通の形式証明(普通の証明でなく)の記号の部分を、
普通の英単語に機械的に置き換えた感じがするね。ちょっと
見ただけだから確証はない。
412 :
132人目の素数さん :2005/09/30(金) 02:01:57
普通の数学でも、厳密な証明ではなく ポイントになるところをイメージ喚起 的に説明するのは、非常に難しいよ。 俺はこれは得意じゃない。厳密にしこ しこ証明を書くほうがルーチン的で、 体力を使うが気は楽。厳密といっても 形式的証明では、もちろんないけど。
二日で400レス越えかよすげぇな(;´Д`)
414 :
132人目の素数さん :2005/09/30(金) 03:58:25
数学板で伸びるスレは質問すれだけかと・・・おもっていたガ
415 :
132人目の素数さん :2005/09/30(金) 07:48:30
>>274 >平地健吾だって小島定吉だって、
>オリジナリティの低い低レベルな結果だ、と
>内心考えてると思うよ
それ以前に、
「数学の話じゃないだろ」
と思ってるだろ。
そしてそれは正しい。
416 :
132人目の素数さん :2005/09/30(金) 07:54:44
>>277 >証明の形式化のどの部分がそんなに難しいと考えてるのかな?
>少なくともZFCの公理から、必要な諸概念を定義して、
>完全に形式的に証明するのは、述語論理の基礎を
>理解している数学者には簡単なことだと思うがな
まず、数学者は述語論理もZFCも正確に理解してるわけではない
次に、理解していたとしても、自分たちが直観で扱ってきた概念を
完全に記号操作として書ききるのは実は箆棒に困難な作業である。
最後に、上記の「翻訳」の作業で、多くのミスが発生し形式化された
理論が、直観的概念に照らし合わせて妥当かどうかチェックする
必要がいたるところで発生する。
プログラムのデバッグをやったことがある人にとっては明らかなこと。
417 :
132人目の素数さん :2005/09/30(金) 08:05:03
>>284 >別に「形式的証明」がなくても不安じゃありませんけど。
ごもっとも。
数学の証明はプログラム検証とは違う。
数学は読んだ人が理解できればそれでよい。
ギャップは読者にとって自明でないから問題になるのであって
多くの専門家が「自明」と判断すればそれはギャップでなくなる。
「玄人の誤解」とは、数学が実は数学者の頭の中の世界における
共同の了解事項であるにすぎないにもかかわらず、あたかも
自分たちとは全く独立なる真偽の根拠があると信じていること。
そしてそれが嘘であることを暴くのが形式的証明。
なぜなら、誰一人了解しない機械的検証を、数学者はまったく
信頼しないからである。
418 :
132人目の素数さん :2005/09/30(金) 08:11:25
>>308 >とりあえず
http://mizar.org/fm/ と20万行目に目を通したんだけど,
>ほとんど全てが 定式化のための定式化で冗長としか思えんかった.
主語をはっきり書こう。論理的であるということはそういうこと。
さて、あなた(もっと広く人間サマ)にとって冗長であるからといって
機械にとっても同じとは限らない。機械は記号処理しかできない石頭
であるということを忘れてはならない。
>知識蓄積する以外になんかこのあたり簡単にできんかな?
簡単にしたために、形式化自体を否定する結果になるかもしれん。
あんたの勝ちなんだからもういいでしょ。形式的証明に拘ってる奴はもう居ないって。
420 :
132人目の素数さん :2005/09/30(金) 09:17:04
>>390 >つーかさ、ある形式体系で証明可能であったとしても、その
>形式体系が無矛盾か、どうかは結局、数学者の主観に永遠に
>留まるしかない。
集合論の公理系に矛盾が発見されない限りそうだな。
だから表題のジョルダンの定理の証明も、元になってる公理
(集合論だろう?)に矛盾がないと証明されてないわけだから
客観的な意味で正しいかどうかはわからない。
結局、形式主義は自己矛盾で行き詰まることになってる。
形式主義の最大の問題は意味を無視していること。
定理の意味こそ重要なのにな。
421 :
132人目の素数さん :2005/09/30(金) 09:30:04
アインスッタイン博士の業績も 当時は理解できるひとがほんど少なくてなあ んでもんで後年追試されていったけんよ ほなこの証明もなんだかんだでアルゴリズムになってよ CGとかいろんなプログラムに応用されるようになったらな ああこれこれってなるくらいになって認められるんべいよ でかい目でみんれば技術投資なんだべよなキタコレ
422 :
132人目の素数さん :2005/09/30(金) 09:36:35
>>417 >「玄人の誤解」とは、数学が実は数学者の頭の中の世界における
>共同の了解事項であるにすぎないにもかかわらず、あたかも
>自分たちとは全く独立なる真偽の根拠があると信じていること。
「共同の了解事項であるにすぎない」のすぎないに引っかかるな。
なぜそう言い切れる? つまり実在論が嘘だと何故言い切れる?
>そしてそれが嘘であることを暴くのが形式的証明。
>なぜなら、誰一人了解しない機械的検証を、数学者はまったく
>信頼しないからである。
この「なぜなら」がまったく分からない。
もっと詳しく説明してもらいたい。
423 :
132人目の素数さん :2005/09/30(金) 09:43:24
>>361 >「普通に証明できてるものは『適当な』公理系で形式証明可能」
>いや、「できないものもある」
極論をいえば、公理や推論規則を適当に追加すれば
名目上「形式的証明」にはできる(w
ただし実際にはぎりぎりまで絞った公理と推論規則だけを
用いた形式的証明ができるかどうかを問題にしている。
「できると信じたいが、もしかしたらできないかもしれない。」
これが率直な気持ちだろう。
機械的検証を信用しない数学者なんてもういないだろ。 俺も人間が検証できるに越したことはないと思ってはいるがな。
425 :
132人目の素数さん :2005/09/30(金) 09:49:44
>実在論が嘘だと何故言い切れる? 嘘だとはいっていないよ。 ただ、本音はそうじゃないってこと。 いざというときに、自分の理解してないことは認めない。 それが本音。そもそも数学者は理解するために数学しているんで 自分が理解できない定理なんて数学者には不愉快なだけでしょ(w
426 :
132人目の素数さん :2005/09/30(金) 09:53:06
>機械的検証を信用しない数学者なんてもういないだろ。 ビル・サーストンは信用してないみたいだけど。
427 :
132人目の素数さん :2005/09/30(金) 09:53:07
>>424 はあ?信用なんて出来ないよ。この場合はな。20万行の中身を
見ないことには。さらにはMizarとかいうソフトのコードも調べないことには。
428 :
132人目の素数さん :2005/09/30(金) 09:57:41
普通は足し算の結合法則や交換法則を疑う奴はいない。 しかし帰納法抜きのロビンソン算術では証明できない。 ロビンソン算術は弱いといわれるが、普通の自然数の計算は ちゃんとやるから、直観的には証明できそうに思える。 しかし、実際には「想定外の反例」がある。 つまりロビンソン算術では自然数を十分に定義できていない。 形式化の穴はいたるところにある。
>>428 「証明不可能」だったらまだいいかな。
でも、NBG集合論からは「否定が証明可能」で、
多くの数学者にとって正しいと思われてる命題って具体的にある?
430 :
132人目の素数さん :2005/09/30(金) 10:02:03
帰納法入りのペアノ算術で、足し算の結合法則や 交換法則を証明すると、直観との乖離に気づく。 加法の形式的な定義はそもそも不自由である。 上記の証明は、パズル的な面白さは感じられるが それは当たり前のことを面倒な状況で示すだけのことで これで正しさが保証されるという感じはしない。
431 :
132人目の素数さん :2005/09/30(金) 10:03:14
>>425 >いざというときに、自分の理解してないことは認めない。
誰のことを言ってる?一からげにしなさんな。
それに文意もはっきりしない。自分の理解してなことは、認めるも
認めないもノーコメントが普通の態度だろ。
>そもそも数学者は理解するために数学しているんで
だから、一からげにしなさんな。
432 :
132人目の素数さん :2005/09/30(金) 10:05:53
>>429 >NBG集合論からは「否定が証明可能」で、
>多くの数学者にとって正しいと思われてる
>命題って具体的にある?
なぜZFCでなくNBG?
もしかして、クラスを考えないと
「証明されてるが受け入れられない定理」
があるのかな?(例えば集合の全体が存在しない、とか)
433 :
132人目の素数さん :2005/09/30(金) 10:09:03
>>431 >一からげにしなさんな。
十巴一からげとはいうが、一からげとはいわない。
>自分の理解してなことは、認めるも認めないも
>ノーコメントが普通の態度だろ。
それが「認めない」ということ。
>>432 圏論とかはクラスで考える方が自然じゃない?
ZFCで出来なくはないだろうけど。
435 :
132人目の素数さん :2005/09/30(金) 10:13:36
>>434 >圏論とかはクラスで考える方が自然じゃない?
じゃ、集合の圏では成り立たないが
別の圏で成り立つ命題があるかどうか
探して見ればいいのでは?
あってもおかしくはない希ガス。
436 :
424 :2005/09/30(金) 10:16:55
>426 名前:132人目の素数さん[] 投稿日:2005/09/30(金) 09:53:06
>>機械的検証を信用しない数学者なんてもういないだろ。
>
>ビル・サーストンは信用してないみたいだけど。
勝手なことを言わないように。サーストンはコンピューター大好き人間だし、
機械を使った証明検証に対する彼の好意的な意見は
ttp://arxiv.org/abs/math.HO/9404236 に述べられているから読んでおくように。
437 :
132人目の素数さん :2005/09/30(金) 10:18:11
>>433 >十巴一からげとはいうが、一からげとはいわない。
口語では一からげで十分通じるし、そう言う言い方もありなの。
そちらの地方では言わないかもしれないけどな。
>それが「認めない」ということ。
ノーコメントがなんで認めないになるんだよ。
分からないってだけだろ。
>>437 口語では「一緒」というよな。
一からげなんてちょっとわざとらしくて不自然
そのくせ省略してるところがハンパ。
>ノーコメントがなんで認めないになるんだよ。
>分からないってだけだろ。
分からないなら認めないってこと。
440 :
132人目の素数さん :2005/09/30(金) 10:25:28
数学者なんて自分の理解してない定理でも使いまくりだよ。 幾つかの分野にまたがる研究していたら、使っている定理が 正しいかどうかなんて個人ではチェックしきれないからね。 安全のために、その分野のエキスパートに確認する程度だよ。 だから自動プルーフ・チェッカーがあって正しい定理を認定して くれるってんなら、そりゃ便利だわな。
>数学者なんて自分の理解してない定理でも使いまくりだよ。 それは他人の理解を信頼してるからであって、 形式的証明への信頼とは異なる話だな。 >自動プルーフ・チェッカーがあって正しい定理を認定してくれる >ってんなら、そりゃ便利だわな。 チェッカーが便利なのは、正しさを認定するからじゃないよ。 どこにバグがあるかを判定してくれるから。 証明がチェックを通ったから正しいとはいえない。 形式化自体が間違っている可能性は多々ある。
442 :
132人目の素数さん :2005/09/30(金) 10:35:40
>>439 >一からげなんてちょっとわざとらしくて不自然
全然不自然ではないよ、だけどスレと関係ないからな。
>分からないなら認めないってこと。
違うだろ。面倒だから、仮にそうだとしてそれがいけないのか?
つまり、分からないことに対しては、ノーコメントじゃいけないのか?
443 :
424 :2005/09/30(金) 10:38:26
>>438 サーストンは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 では
>彼がフォーマリズムを信頼してないことが分かる。
とビミョーに意見をずらしたね。
>>442 >>一からげなんてちょっとわざとらしくて不自然
>全然不自然ではないよ
君が、一緒のことを一からげとかいう実に辺鄙な田舎で
子供時代をすごしたという「特殊な人」なら仕方がない。
別に何県何郡何村大字何某字何某なんて聞かないから
安心したまえ。書いたらどこの誰だか分かっちゃうだろ?(w
>面倒だから、仮にそうだとしてそれがいけないのか?
>つまり、分からないことに対しては、ノーコメントじゃいけないのか?
だから、君の「認める」という言葉の理解が間違ってる。
>>443 >ビミョーに意見をずらしたね。
いや、私はもともと*human understanding*が重要だといってるんで
それ抜きに形式的だから正しいということにはならないといってるわけ。
サーストンの文章を正しく読めば、彼が「機械が検証すれば、
人間の理解ぬきに正しい」とはいっていないことがわかる。
446 :
132人目の素数さん :2005/09/30(金) 10:45:58
>>444 おれは生まれも育ちも東京だよ、環状線の中。
ごちゃごちゃ言わなくていいから、これに答えてくれ。
>つまり、分からないことに対しては、ノーコメントじゃいけないのか?
447 :
424 :2005/09/30(金) 10:48:33
>いや、私はもともと*human understanding*が重要だといってるんで
>>426 では機械検証を信用してない数学者の例として
サーストンを挙げたんじゃなかったのか?
彼はどこでそんなことを言ってる?
>おれは生まれも育ちも東京だよ、環状線の中。 じゃ、両親が田舎の人か。最近は珍しくない。 悪いがおれは祖父母の代から東京市内。 ごちゃごちゃ弁解するな。お前の日本語が間違ってるんだ。直せ。
>>447 >彼はどこでそんなことを言ってる?
サーストンに対するインタビュー記事で
彼が一時期直観主義に傾倒していて、
形式的証明がそれゆえに正しいという
考え方に対して疑念を抱いているという
文章を読んだ。
450 :
132人目の素数さん :2005/09/30(金) 10:55:17
>>一からげにしなさんな。 >十巴一からげとはいうが、一からげとはいわない。 何このどうでもいい突っ込み。ここ本当に数学板?
451 :
424 :2005/09/30(金) 10:59:53
>>449 はいはい。ソースはないわけね。
それに、二十年前に機械検証を信用しなかった数学者ならいくらでもいるしな。
>426 名前:132人目の素数さん[] 投稿日:2005/09/30(金) 09:53:06
>>機械的検証を信用しない数学者なんてもういないだろ。
>
>ビル・サーストンは信用してないみたいだけど。
452 :
132人目の素数さん :2005/09/30(金) 11:03:38
>>451 >はいはい。ソースはないわけね。
残念だが、君の期待ははずれだ。
数学人群像―プロフィルとインタビュー
D.J. アルバース (編集), G.L. アレクサンダーソン (編集), 一松 信 (翻訳)
>それに、二十年前に機械検証を信用しなかった
>数学者ならいくらでもいるしな。
機械検証をしたことがある人なら、今でも
形式化の誤りが深刻だというのは常識だがな。
453 :
424 :2005/09/30(金) 11:09:43
>>452 ちゃんと該当部分を引用してくれないかな。
サーストンは先に挙げた文献の中(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.
とも言ってる。機械で検証する方が人間がやるより厳密だってわけだ。
まあ、その後に長いプログラムにつきもののバグを心配しはいるが。
454 :
132人目の素数さん :2005/09/30(金) 11:15:03
>>453 今残念ながら手元にない。図書館ででも探してくれ。
>機械で検証する方が人間がやるより厳密だってわけだ。
>まあ、その後に長いプログラムにつきもののバグを心配しはいるが。
プルーフチェッカーのバグの可能性は確かにあるが、
それはまだなんとかなるほうだ。問題は、形式化する
理論自体がどうしたって長大になるから、そこに
バグが混入する可能性が避けられないってことだ。
それは前提だから、チェッカでは検証できない。
455 :
132人目の素数さん :2005/09/30(金) 11:27:49
もっとも見つかりにくいパターン 設定した公理系は無矛盾であったが、実は考えていたものとは違っていた。 しかし、定理の形式的証明ができたので、万事OKと考えた。 その後、実は当初の公理系では強すぎて、排除したいものまで 証明できてしまうことがわかったので、公理系を変えたところ 証明ができなくなった。実際後で反例がみつかった。
456 :
132人目の素数さん :2005/09/30(金) 11:33:22
プルーフ・チェッカーはまだいいけど自動証明に期待をもつってのは、 AIの研究者以外では数学の出来ないやつだけだろ。 自分の代わりに機械にやってもらおうと。そんなの何の意味があるか 知らないけど。宿題やってもらうとかかw
>>456 >自動証明に期待をもつってのは・・・数学の出来ないやつだけだろ。
>自分の代わりに機械にやってもらおうと。
>そんなの何の意味があるか知らないけど。
全然ないとはいわない。証明を読んで理解したなら
それはそれで当人には意味がある。
ただ、不勉強な奴はきっと証明なんて読まないだろうけど。
458 :
132人目の素数さん :2005/09/30(金) 12:29:06
>>455 >設定した公理系は無矛盾であったが、
無矛盾の公理系からでる定理なんてつまらないものか、
マイナーな分野、例えば組み合わせ論とかの定理じゃないの。
重要な定理って大抵、実数体や選択公理などを使うでしょ。
459 :
132人目の素数さん :2005/09/30(金) 12:30:38
>>415 小島はサーストンを恐らく敬愛しているだろうから、
どう思うだろうね。
結局、「意識調査」の問題だけどさ
460 :
132人目の素数さん :2005/09/30(金) 12:33:33
こういうの困るんだよね 価値の低いどうでもいい結果なのに 一般メディアに大きく報道されて 誤解が誤解を生んでめちゃくちゃになる しょせん大衆は馬鹿だから
461 :
132人目の素数さん :2005/09/30(金) 12:35:08
>>457 >自動証明に期待をもつってのは・・・数学の出来ないやつだけだろ。
そんなことはない。頭の悪い奴に自分の証明を見せても
分からないときに、「貴方は分からないのかもしれない
けど、このプルーフ・チェッカーでは通ってるよ」、と
言える。(主張の正しさについての)肯定的な査読者が
増えたようなもの
462 :
132人目の素数さん :2005/09/30(金) 12:36:20
>価値の低いどうでもいい結果なのに >一般メディアに大きく報道されて じゃあ、価値のある結果をアピールしようぜ!
463 :
132人目の素数さん :2005/09/30(金) 12:37:39
客(納税者)を馬鹿呼ばわりするのは 止めましょう。ここは2chだからいい けど
464 :
132人目の素数さん :2005/09/30(金) 12:38:32
>>461 プルーフ・チェッカーと自動証明はちがうんだけど。
465 :
132人目の素数さん :2005/09/30(金) 12:43:06
466 :
132人目の素数さん :2005/09/30(金) 12:47:30
>>464 俺の言うプルーフ・チェックは「実用的なそれ」だからな…
こう言えばいいか、「自明な」命題の自動証明のこと。
「自動証明」って言葉は紛らわしいな
逆側の極が「まだ予想もされていない価値のある定理の
自動発見(+証明)」か
467 :
132人目の素数さん :2005/09/30(金) 12:53:18
あまり現実化は期待できないけど、
「まだ予想もされていない価値の
ある定理の自動発見」ができれば
意味あるね
>>465 に計算機を使ってる証明が
あるけど無意味だとは感じないな。
自動証明ではないけど。部分的に
何かを計算機で証明しているんだ
けどね
468 :
132人目の素数さん :2005/09/30(金) 13:02:11
>元になってる公理(集合論だろう?)に矛盾がないと >証明されてないわけだから客観的な意味で正しいか >どうかはわからない。 いや、違う。「その公理系では全ての命題が客観的に 正しい」だけだ。形式化しなければ、主観に過ぎない。 但し、多くの数学者は客観性に価値をそれほど置いて いないと思うね。だから、主観でもいいじゃない、と 言うこと ある公理系が無矛盾だろうというのも主観だし、その 公理系に意味があるというのも主観だから。ただし、 その公理系からかくかくしかじかの命題が、形式的に 証明できるのは客観だ。それに、どのくらいの価値が あるか、と思うのかは、主観だね
469 :
132人目の素数さん :2005/09/30(金) 13:05:06
>>458 >無矛盾の公理系からでる定理なんてつまらないものか、
>マイナーな分野、例えば組み合わせ論とかの定理じゃないの。
をひをひ、無矛盾でない公理系は何でも証明可能だから無意味だぞ(w
>重要な定理って大抵、実数体や選択公理などを使うでしょ。
あのなぁ、無矛盾性が証明できない=矛盾してる、ってことじゃないぞ(w
470 :
132人目の素数さん :2005/09/30(金) 13:07:51
>>468 いっとくけど、「形式化すれば客観的」とかいうのも主観だぞ。
どこまでいっても主観を排除できない。できると思うのは妄想だ。
471 :
132人目の素数さん :2005/09/30(金) 13:13:58
>>470 それじゃあ、客観はないことになるよ。とすれば、
すべてが主観なのだから、「主観と客観」という
区別自体が無効化するが…
472 :
132人目の素数さん :2005/09/30(金) 13:15:39
>>471 >それじゃあ、客観はないことになるよ。
ないと困るのか?
473 :
132人目の素数さん :2005/09/30(金) 13:16:44
例えば、 ZFCの無矛盾性=主観 かくかくしかじかの形式的命題がZFCで証明可能=客観 という区別ね。こういう区別をする、というのはあくまで 俺の意見だけど
474 :
132人目の素数さん :2005/09/30(金) 13:16:48
>>471 >すべてが主観なのだから、
>「主観と客観」という区別自体が
>無効化するが…
効果があると思ってたのか?
475 :
132人目の素数さん :2005/09/30(金) 13:18:20
>>473 要するに
有限=客観
無限=主観
ってことかな?(w
476 :
132人目の素数さん :2005/09/30(金) 13:21:24
>>472 全てが主観だったら、「それは主観である」という
主張には何の意味もなくなるよ
わざわざ矛盾した体系を使ってたら、全てが正しい
命題なんだから、「この命題は正しい」というのが
無意味になるようなもの
477 :
132人目の素数さん :2005/09/30(金) 13:23:07
>>476 > 全てが主観だったら、
>「それは主観である」という主張には
>何の意味もなくなるよ
意味があると思ってたのか?
478 :
132人目の素数さん :2005/09/30(金) 13:25:16
客観性とは、 「自分が間違ってるかもしれない」 という不安を解消するための阿片
479 :
132人目の素数さん :2005/09/30(金) 13:27:28
他者の理解は 「自分が間違ってるかもしれない」 という不安を分割して無害な程度に 小さくするためのもの
480 :
132人目の素数さん :2005/09/30(金) 13:29:58
>>478 だから、それが君の言葉使いにおける客観性だとしたら、
「君の言う客観性(=自分は間違ってるかもしれないと
いう不安を解消するための阿片)」が世の中にあるじゃ
ない
要は言葉使いの違いだよ。
481 :
132人目の素数さん :2005/09/30(金) 13:30:57
>>469 無矛盾の公理系っていうのは、引用元の言葉をそのまま使ったもの。
つまり、無矛盾と分かっている公理系という意味。
少しはスレを追えよ。
>あのなぁ、無矛盾性が証明できない=矛盾してる、ってことじゃないぞ(w
俺はそんなこと言ってないよ。勝手に見当違いな解釈すんじゃない。
482 :
132人目の素数さん :2005/09/30(金) 13:31:05
483 :
132人目の素数さん :2005/09/30(金) 13:32:19
>>481 無矛盾な公理系は無矛盾と証明されている公理系という意味じゃない。
少しは日本語をマジメに勉強しろ。
20 万行というのは思ったより少ない。何かうまいアイデアを使ったのではないか。 という感想を持った奴はいないのか?
485 :
132人目の素数さん :2005/09/30(金) 13:33:13
>>478 君は、君なりに客観性という言葉を使っていて、
そういう物(=客観性)は現に存在するわけだ。
486 :
132人目の素数さん :2005/09/30(金) 13:34:14
487 :
132人目の素数さん :2005/09/30(金) 13:35:08
>>485 君は、ユニコーンという言葉があるから
ユニコーンが存在するんだというのかい?
それとも、阿片の吸いすぎで幻覚を見たか?(w
488 :
132人目の素数さん :2005/09/30(金) 13:38:01
>>482 俺は違う意味で、客観性という言葉を使っているだけだ。
いずれにしても、区別をしている以上はあるんだよ。
どういう意味なのかは、完全には明確にはならないけど。
「この料理は旨い」と言えば、旨いものと不味いものが
ある。但し、当然ながら「完全に正確な意味」は分から
ない。
489 :
132人目の素数さん :2005/09/30(金) 13:38:20
>>484 一ページ40行として、5000ページか。
数学書何冊分に当たるか考えたくもない。
490 :
132人目の素数さん :2005/09/30(金) 13:39:07
>>487 その場合でも、幻覚の中にあると思うが…
491 :
132人目の素数さん :2005/09/30(金) 13:40:19
>>488 無責任な臆病者の自己弁護は醜いものだ。
>>486 そういう証明を一般的に可能と考えられている方法で行間を埋めようとすると、
20 万行ではとてもきかないと思うのだが。
493 :
132人目の素数さん :2005/09/30(金) 13:42:03
>>490 その意味での「在る」は幻覚を見る君の主観
ほら客観が消滅しただろ。
♪
これも主観
あれも主観
たぶん主観
きっと主観
494 :
132人目の素数さん :2005/09/30(金) 13:42:52
(少なくとも)君の考えの中では「自分は間違ってるかもしれないという 不安を解消するための阿片」があるでしょ。それとも、ないのかい? (少なくとも)俺の中で「旨い」「不味い」の区別があるようにね。
495 :
132人目の素数さん :2005/09/30(金) 13:44:33
>>494 自分の中の「旨い」「不味い」の区別が主観であるように、
自分の中の「主観」「客観」の区別は主観でしかない。
496 :
132人目の素数さん :2005/09/30(金) 13:45:17
>>493 だから、言い方を変えれば消滅するよね。言ってることが
違うんだからさ。それだけのことだ。君は勝手に言い方を
変えて「人の感想」を否定し、「自分の感想」を押し付け
ようとしてるだけだ。
497 :
132人目の素数さん :2005/09/30(金) 13:45:56
自分でないものが、正しさの根拠になることはない。 最終的には自分自身の信念が根拠。 死ねない者はそもそも生きていない。
498 :
132人目の素数さん :2005/09/30(金) 13:47:16
>>495 >自分の中の「主観」「客観」の区別は主観でしかない。
もちろん、そうだ。だから、主観的区別として、主観と
客観があるのよね。
499 :
132人目の素数さん :2005/09/30(金) 13:47:50
>>496 いや、目を開くと消滅するのだ。
君は目をつぶって自分の妄想を語り
それが妄想に過ぎないという忠告に
耳をふさいでいるだけだ。
500 :
132人目の素数さん :2005/09/30(金) 13:49:40
>>499 どうやら、君の方が妄想的になってるねw
501 :
132人目の素数さん :2005/09/30(金) 13:50:24
>>498 >主観的区別として、主観と客観があるのよね。
それは君が間違っているから。
主観的だから間違いがないということにはならない。
このスレ進行早いなあ 数学板随一のスピードだ
503 :
132人目の素数さん :2005/09/30(金) 13:51:21
>>500 >どうやら、君の方が妄想的になってるねw
いや、それは妄想だ(w
504 :
132人目の素数さん :2005/09/30(金) 13:51:39
505 :
132人目の素数さん :2005/09/30(金) 13:53:09
>>501 >主観的だから間違いがないということにはならない。
じゃ、「間違ってる」という状態が客観的にあるんだ。
506 :
132人目の素数さん :2005/09/30(金) 13:53:48
>書いてるのは2人か3人です じゃあ、二人だ。 なぜなら、議論してる二人と独立の人物なら 自分が三人目だとわかるから。
507 :
132人目の素数さん :2005/09/30(金) 13:53:59
結局、言葉使いの違いだろ。それだけ
508 :
132人目の素数さん :2005/09/30(金) 13:55:09
>>505 >>主観的だから間違いがないということにはならない。
>じゃ、「間違ってる」という状態が客観的にあるんだ。
それが間違いだ。主観的であっても矛盾からは免れない。
509 :
132人目の素数さん :2005/09/30(金) 13:56:13
>>507 >結局、言葉使いの違いだろ。それだけ
ネットでは、私が間違ってましたという言葉は
このように言い直される(w
510 :
132人目の素数さん :2005/09/30(金) 13:57:42
>>508 ただ、「単に感想レベルの話」でも、他人との対立や矛盾を
許容したくないだけでは?
>>448 >東京市内
東京市内東京市内東京市内東京市内東京市内東京市内東京市内東京市内東京市内
東京市内東京市内東京市内東京市内東京市内東京市内東京市内東京市内東京市内
東京市内東京市内東京市内東京市内東京市内東京市内東京市内東京市内東京市内
東京市内東京市内東京市内東京市内東京市内東京市内東京市内東京市内東京市内
東京市内東京市内東京市内東京市内東京市内東京市内東京市内東京市内東京市内
東京市内東京市内東京市内東京市内東京市内東京市内東京市内東京市内東京市内
512 :
132人目の素数さん :2005/09/30(金) 13:58:45
>>488 >「完全に正確な意味」
自分とは独立に「正しい意味」があると思うのは
単に自分の存在を忘れたからだろう。
513 :
132人目の素数さん :2005/09/30(金) 14:00:06
「この料理は旨い」って言葉に、正しいも間違いもないだろ だけど、この言葉には意味が含まれている
514 :
132人目の素数さん :2005/09/30(金) 14:00:34
>>511 別に間違ってない。戦前は東京市だ。
しかも35区の頃ではなく15区の頃からだ。
515 :
132人目の素数さん :2005/09/30(金) 14:01:59
>「この料理は旨い」って言葉に、正しいも間違いもないだろ 状況による。 旨いと思って言ったならそれは正しいが お世辞で嘘をついたならそれは間違いだ。 もっとも、世の中は正しければよいというものではない(w
516 :
132人目の素数さん :2005/09/30(金) 14:04:24
>この言葉には意味が含まれている 意味を否定した覚えはない。 自分とは独立だというのが間違ってるといったまでだ。
517 :
132人目の素数さん :2005/09/30(金) 14:09:03
>>515 >お世辞で嘘をついたならそれは間違いだ。
じゃあ、君はそういう人の発言を「間違いだ」と
表現するんだね。
結局、ここに戻る気がするねえ。
>ただ、「単に感想レベルの話」でも、他人との対立や矛盾を
>許容したくないだけでは?
518 :
132人目の素数さん :2005/09/30(金) 14:12:19
>>517 >君はそういう人の発言を「間違いだ」と表現するんだね。
口にだすとは限らないな。
しかし、今ここで君にお世辞をいうことで
私や君が何らかの利益を得るとは考えない。
>結局、ここに戻る気がするねえ。
戻りたがってるのは君だろう。
519 :
132人目の素数さん :2005/09/30(金) 14:13:39
>>516 「この料理は旨い」って感想は自分と独立ではない、ってのは
普通のことだろ?どうして、そんなこと盛んに言うのかなあ。
520 :
132人目の素数さん :2005/09/30(金) 14:14:21
>「単に感想レベルの話」でも、他人との対立や矛盾を許容したくない 「単に感想を述べただけ」(ここでレベルというのはおかしい) といって、他者との対立や自己の発言の矛盾を避けるのは、 君自身が卑怯だからだろう。
521 :
132人目の素数さん :2005/09/30(金) 14:14:36
>戻りたがってるのは君だろう。 もちろん、そうだが?
522 :
132人目の素数さん :2005/09/30(金) 14:15:43
>「この料理は旨い」って感想は自分と独立ではない、 >ってのは普通のことだろ? それなら「「完全に正確な意味」は知らない」という言い方はおかしい。 まさに君自身が旨いと感じたときが「完全に正確な意味」だからだ。
523 :
132人目の素数さん :2005/09/30(金) 14:18:25
形式絶対主義のおかしな点は、自分の「旨い」という感覚を 文字で表したものが、本来の正しい意味だと言い張るところ。
524 :
132人目の素数さん :2005/09/30(金) 14:18:26
>>520 やっぱり、そうみたいだね。君はそれを卑怯と表現するのか。ふ〜ん
A:俺は不味いと思う。
B:いや、俺は俺は旨いと思うけど。
これで、終わって別の話題に移るのもよし。
「どうして〜?」と互いの感想を話題にし
続けるのもよし。
互いの感想を押し付け合うとこのスレみたいになるのか......
526 :
132人目の素数さん :2005/09/30(金) 14:21:34
>>524 やっぱり君は分かっていないな
私がいってるのは例えば
TV番組の「食わず嫌い」のコーナー
のような状況。
君は自分がいってることの矛盾を認めていないから
間違っているといっているのだよ。
527 :
132人目の素数さん :2005/09/30(金) 14:22:48
528 :
132人目の素数さん :2005/09/30(金) 14:24:17
>>527 >>互いの感想を押し付け合うとこのスレみたいになるのか......
>まあ、そうだなw
二人とも馬鹿だなw
529 :
132人目の素数さん :2005/09/30(金) 14:25:50
>>483 >無矛盾な公理系は無矛盾と証明されている公理系という意味じゃない。
文脈からそういう意味で使ってるんだよ。
そう解釈しないと、俺の言ったことの意味が通らないだろ。
530 :
132人目の素数さん :2005/09/30(金) 14:27:35
>>529 >文脈からそういう意味で使ってるんだよ。
勝手にそう思い込んだだけだろ。
>そう解釈しないと、俺の言ったことの意味が通らないだろ。
君が馬鹿なだけだ。自業自得だ。
531 :
132人目の素数さん :2005/09/30(金) 14:29:53
>>528 A:お前は間違っている!
B:感想なんだから、間違ってるも何もないでしょ。
それに自分は素直に感想を述べてるつもりだし。
A:それでも、お前は間違っている!
B:他人の感想ぐらいは、認めたら?
の繰り返しですw
532 :
132人目の素数さん :2005/09/30(金) 14:31:27
ただ、「単に感想レベルの話」でも、他人との対立や矛盾を 許容したくないだけでは?
>>470 >>523 なんだ、やっぱりあちこちの基礎論系のスレでいつも同じこと書いてる人か
これが言いたいがために、話を無理矢理引っ張って誘導するんだよね
はいはい、啓蒙活動おつかれさんです
534 :
132人目の素数さん :2005/09/30(金) 14:35:50
>>533 そっか、その感想を皆に披露したかったんだね
披露できて、良かったね
535 :
132人目の素数さん :2005/09/30(金) 14:53:51
>>530 勘違いしたお前が悪い。文意を考えれば勘違いするはずないんだよ、普通はな。
536 :
132人目の素数さん :2005/09/30(金) 14:59:51
なぜ「形式的・客観的証明」というものが題材となった議論で これほどまでに主観的で曖昧な表現が飛び交うのか。 それと他人に意見を伝える気があるのなら、 レス番号でもいいので、せめて名前欄くらい埋めてから投稿して欲しい。 傍観者としても読む気が起きない。
538 :
132人目の素数さん :2005/09/30(金) 15:13:03
>なぜ「形式的・客観的証明」というものが題材となった議論で >これほどまでに主観的で曖昧な表現が飛び交うのか。 ここで行われてたのは「自分の価値観の表明」だから、 それは当然だと思うよ
もはやどんなレスに対しても
>>534 のようなレスを返すだけの
無意味なキャラに成り果てました
540 :
132人目の素数さん :2005/09/30(金) 15:47:32
哲板っぽい
541 :
132人目の素数さん :2005/09/30(金) 16:13:55
>>533-534 まあ、いいんじゃないかな。さすがに、他人から自分が
『人の感想を否定して自分の感想を押し付ける人』だと
見られていることは、分かったんじゃないの。
自分の感想を言ったり、他人の感想を聞いたりするのは、
よくあることだけどね。
542 :
132人目の素数さん :2005/09/30(金) 16:16:02
543 :
132人目の素数さん :2005/09/30(金) 17:10:23
なんか啓蒙書で生半可な知識を聞きかじって それを自分のナイーブな感覚とまぜくって 偉そうにしゃべって、つっこまれるとやれ 感想だ、オレの言葉だと馬鹿丸出しなこと いって結局自爆するいつもの馬鹿がいるね。 いい加減、もうその芸は見飽きたよ。 ちっとは新しいこと学んで違うネタみせろ
544 :
132人目の素数さん :2005/09/30(金) 17:13:05
>なぜ「形式的・客観的証明」というものが題材となった議論で >これほどまでに主観的で曖昧な表現が飛び交うのか。 そもそも形式化のプロセスは客観的でもなんでもないからさ。 そのことに気づかない素人が勝手に自分の主観的な「客観性」 をわめきちらしてしかもそれがいかに主観的で身勝手なものか 絶対に認めようとしないからみっともないことになる。 ちなみに、曖昧とかいう前に無意味だね。無意味。
545 :
132人目の素数さん :2005/09/30(金) 17:16:13
>他人に意見を伝える気があるのなら、 >レス番号でもいいので、せめて名前欄くらい >埋めてから投稿して欲しい。 ん?漏れは誰がいってるかトレースできたよ。 書いてること読めばわかるじゃん。 >傍観者としても読む気が起きない。 自分の意見ももてない傍観者は読んではいかんな。 馬鹿には無理なんだよ。考えない君のような馬鹿にはね。
546 :
132人目の素数さん :2005/09/30(金) 17:22:17
>あちこちの基礎論系のスレでいつも同じこと書いてる人か 二人いるね。 ・必ず基礎論という言葉を用いて、実に陳腐な 形式的=客観的という主張を「基礎論の初歩」 とほざくアホ ・ロジックという言葉を用いて、上記のような 陳腐な主張に必ず突っ込みを入れたがる、 玄人ぶったウザイ奴 で、だいたい前者の一見もっともらしい主張が 後者の狡猾極まりないレトリックに押されて 耐えられなくなった前者がブチ切れて終わる といういつものパターン。もう何度みたか。
547 :
132人目の素数さん :2005/09/30(金) 17:41:11
俺哲厨の見分けつくようになった おもしろくないとか ためにならないとか 価値観がどうのこうのいうやつがそう 数学やってるやつはただ本を読むのでも演習を自分でやって解く能動的な仕事を伴う だから考え方が実践的で他人の発言をよいか悪いかでは見ない 単純に正しいか間違っているかで見るし そこにはすごくシビアだ 哲厨は哲学書を自分の好き勝手に読むだけだから好き嫌いで批評する癖がついている そして大学でまともにやってるやつらじゃないから論文を書く手法も知らない ただ自分の視点からあれこれ文句をつけるだけ 数学とはその点が相容れない 数学は演習なしでは絶対に身につかねえ 初等数学でも真面目にやってるやつのほうが哲厨よりはるかに話せる 価値観なんてどうでもいいんだよ ぼけが 高度な数学的証明やってのけたやつだけがかっこいい そいつの哲学など知ったことかってのが本来の数学者のスタンスだろ 哲厨は藤原きどりかよw
548 :
132人目の素数さん :2005/09/30(金) 17:52:49
>>547 好き嫌いは、哲学ですらないんだが(w
で、
> 単純に正しいか間違っているかで見る
問題は、何をもって正しいというか、だ。
それを意識したくない人は哲学が嫌い。
哲学とは自己批判なんだよ。
549 :
132人目の素数さん :2005/09/30(金) 17:53:44
550 :
132人目の素数さん :2005/09/30(金) 17:54:45
やたらに比喩を振り回して煙に巻くとかは、数学的な議論でないよな。
厨房よ プルーフチェッカー どうなった
552 :
132人目の素数さん :2005/09/30(金) 18:03:40
プルチェックはスパコンじゃないとだめなのか? javaとかでは無理?
>>552 :
Javaでも出来るけど、プログラミングと計算時間含めて数万年かかると思う。
554 :
132人目の素数さん :2005/09/30(金) 18:11:45
プルーフチェッカーって長いから 今後はプルチェキってよぼうぜ
>>554 :
なんか微妙。。
でも確かに略したいかも。アイディアはいい。
556 :
132人目の素数さん :2005/09/30(金) 18:31:26
>>547 数学って価値観だろ。美意識に近いものが重要。
このあたりプロなら言うのもヤボなくらい先刻承知のこと。
557 :
132人目の素数さん :2005/09/30(金) 18:48:31
>>552 Mizarってのは「IBM-PC上で動作する」とされているぞ。
ソースコードが公開されているかは知らんが、スパコン云々というものではないようだ。
558 :
132人目の素数さん :2005/09/30(金) 19:28:08
良さげな結果に対する臭覚の問題 正しくてもヘボいのは全然ダメ だから主観が重要 因みに形式化のプロセスが主観的なのは当たり前。その後が客観的。 多くの数学者にとって前者の方が、重要なのも当たり前
559 :
558 :2005/09/30(金) 19:31:10
因みに、多くの数学者は普通の主観的証明で充分だと思っている
561 :
132人目の素数さん :2005/09/30(金) 19:38:25
初歩 形式体系=客観 形式体系に関する解釈=主観
562 :
132人目の素数さん :2005/09/30(金) 19:41:22
『形式体系』と『形式体系に対する解釈』の区別が できない奴が一名、紛れ込んでいるみたい
563 :
132人目の素数さん :2005/09/30(金) 20:05:20
形式主義 形式体系→客観 形式体系に対する解釈→主観 実在主義 数学的対象→客観 数学的対象に対する解釈→主観
564 :
132人目の素数さん :2005/09/30(金) 20:10:45
客観と主観は入れこ構造。これは、ただの言葉の問題
565 :
132人目の素数さん :2005/09/30(金) 20:15:48
何が客観(=価値中立)であるかというのは社会科学における イデオロギー闘争に他ならない。という訳でこの闘争にはあまり意味がない。
566 :
132人目の素数さん :2005/09/30(金) 20:45:12
数学の論文の証明が完全かというと全然そんなことはない。 ルネ・トムや佐藤幹夫の論文に書いてあることをきちんと証明した というので立派な論文になるわけだからね。 岡潔の論文の中身を定式化するためには大理論が必要になった。 意味合いがちがうことだけど、 有限単純群の分類が完成したという宣言が出たが 細かいギャップがたくさんあるそうだ。
567 :
132人目の素数さん :2005/09/30(金) 20:51:27
アレはヲタ以外は結論命じゃね?
568 :
132人目の素数さん :2005/09/30(金) 22:15:52
形式主義と実在主義 気違い以外は、両方の価値を認めている。その上で後者に、より価値を置く数学者が多い それだけのことだ
569 :
132人目の素数さん :2005/09/30(金) 22:18:47
形式主義 形式的証明→形式体系→客観 実在主義 証明→数学的対象に対する解釈→主観
570 :
132人目の素数さん :2005/09/30(金) 23:19:35
形式主義 形式的証明 ⊂ 形式体系 実在主義 証明 ⊂ 数学的対象に対する解釈
571 :
132人目の素数さん :2005/10/01(土) 00:06:50
あーあついに哲学板の出張所に
時と場所を考えないのが哲学者っぽいな
573 :
132人目の素数さん :2005/10/01(土) 00:46:25
形式主義 形式体系→客体 その解釈←主体 実在主義 数学対象→客体 その解釈←主体
574 :
132人目の素数さん :2005/10/01(土) 00:47:43
いずれにしても、客体も主体も在るのさ(w
575 :
132人目の素数さん :2005/10/01(土) 00:57:06
哲学厨は二次元ベクトルまでしか使えない だから高度な数学は理解できない
とりあえずmizarのwin32版をダウンロードして試してみました 適当な作業ディレクトリに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$ これでうまく証明できてるのかな?
>>481 +529+535
「無矛盾と分かっている」の「分かっている」は飽くまでお前が
勝手に付け加えただけだと思うぞ
>>458 を読む限り、無矛盾性が証明されている、
という意味で「分かっている」という言葉を使っているんだろうけど
一番初めの
>設定した公理系は無矛盾であったが
は、別に無矛盾である、ということが「分かっている」必要は無い
無矛盾かどうかは天のみぞ知る、ただし、実際には、誰一人人間には
証明できないにせよ、無矛盾であった、という状況で充分
>>531 A:お前は間違っている!
B:数学的な命題以外はすべてただの感想でしょ。
早く数学的な命題を述べてよ、はやくはやく。
A:こいつは莫迦だ、退散しよう。
の繰り返しだと思うぞ。
579 :
576 :2005/10/01(土) 07:43:15
jordan.miz 自体の行数はたった6802行のようです。 ただ、mizarに含まれているライブラリ(Mizar Mathematical Library)のファイルの 行数を数えてみると、183万行もある。(C:\mizar\mml\*.mizの行数を合計) このライブラリ内の定理を jordan.miz で利用しているようなので、 その部分を考慮すると20万行になるということなのでしょう。
>>536 4次元kissing numberの論文とかあるじゃん
581 :
576 :2005/10/01(土) 07:46:22
mizarのソースを探してみたけれども見つかりませんでした。 それにしても、このライブラリを記述した人達の労力を考えると、絶句・・・ですね。
582 :
132人目の素数さん :2005/10/01(土) 08:33:24
形式体系(客観) 形式体系についての解釈(主観) この区別がついてない馬鹿が紛れ込んでただけ
議論の仕方もしらない莫迦(或いは詭弁家)が約一名いるだけかと
しかもまだその話題引っ張ってんのか?
過去ログ読んだけど
>>417 の
>そしてそれが嘘であることを暴くのが形式的証明。
は全く独り善がりだと思うがな
まあ個人的意見だというのなら敢えて否定はしないけど
それなら、普通は私見だが、とか一言書くものだけどな
584 :
132人目の素数さん :2005/10/01(土) 09:04:10
議論にいちいちつまらぬ枕詞を求める馬鹿が少なくとも一名いるな。 お前さえ我慢すれば全てがまるく収まることに気づけ
585 :
132人目の素数さん :2005/10/01(土) 09:04:57
ゲーデルの第二不完全性定理を誤解している人達がいるね。それは 無矛盾性を意味すると解釈される命題で、証明図のない物がある。 実は、一方で 無矛盾性を意味すると解釈される命題で、証明図のある物がある。(ゲーデルの世界p141) まずは形式体系とその解釈の区別をつけましょう
586 :
132人目の素数さん :2005/10/01(土) 09:05:55
>『形式体系』と『形式体系に対する解釈』の >区別が できない奴が一名、紛れ込んでいるみたい それをいうなら、真偽の判定は前者ではなく 後者の問題だってことが分からない阿呆が 一名いるな。
587 :
132人目の素数さん :2005/10/01(土) 09:12:28
そのエサに食いつくのを待ってたゼ!!!(w 上記の場合、証明図の二つの形式的定義 (カット入りとカット無し)によって、 証明可能な定理の全体が等しくなるかどうか が問題となる。 これは自然数論では証明ができない。 つまり、自然数論の形式体系に合致する解釈において 反例が存在する。しかし、このような「反例」は そもそも想定されていたものではない。
588 :
132人目の素数さん :2005/10/01(土) 09:20:34
真偽を論じる上で、形式体系が 「そもそも語りたかったこと」 を語っているかどうかはもっとも 重要なポイント。
589 :
132人目の素数さん :2005/10/01(土) 09:31:52
>形式主義と実在主義 >気違い以外は、両方の価値を認めている。 本当に狂ってるのは、 「俺は客観(=価値中立)的立場に立っている」 と叫んで、自分自身を消去しようとしてる奴。 こういう奴が自殺する。
590 :
132人目の素数さん :2005/10/01(土) 09:33:14
mizarは完全な証明しか受け付けない 現在の論理体系ではあのバナハ・タルスキーのパラドクスが OKとなるがいいのだろうか
>>587 カットって何のこといってるの?
LKとかLJの話してるわけじゃないはずだが
>>590 何が困るの?
論理体系の話じゃなくて公理系の話じゃないの?
593 :
132人目の素数さん :2005/10/01(土) 10:23:25
「真偽の判定」は客体に対する主体の解釈なんだから、それが主観であるのは当たり前 だが、客体が存在する事に変わりはない それとは別に真偽判定(数学的な物に限らない)の対象にならない表現行為、という物もある 例えば「これ旨いね」 人間が行う発言の内で、真偽判定の対象になる物は非常に少ない。この少ないという発言自体がな(w
594 :
132人目の素数さん :2005/10/01(土) 10:33:40
>>593 客体(客観)は存在し、証明図は客体である
多くの発言は真偽判定の対象ではない。普通に証明できれば「適当な」形式体系で証明がある、とかもその一つ
そんな哲学の議論はどうでもよくない?
596 :
132人目の素数さん :2005/10/01(土) 11:32:31
真である(主観) 証明図がある(客観) に必ず間隙が存在する事をゲーデルは証明した。 だからと言って、証明図(客体)が消える訳じゃない。当たり前だがな(w
ある命題が真である、ということにはちゃんと数学的な定義があるんだけどな まあそれは兎も角 このスレはJordanの曲線定理の「完全証明」について話すスレじゃないのか?
598 :
132人目の素数さん :2005/10/01(土) 13:11:10
>>597 普通はない
もちろん、別の形式体系をもってきて「形式的な真」を定義することもある。「普通の真」が「形式的な真」に対応するか、
どうかが主観的な判断である以上、「普通の真」は永遠に主観的なままだ。とは言え
形式的真は普通の真の補強材料くらいにはなるから、それなりに意味はあると思うよ
>>584 こうやってただのオウム返しを繰り返しながら(本人は鋭い切り返しだと思ってるようだがw)
強引に自分が説教したい方向にスレの内容を引っ張っていくんだよね。
基礎論のスレっていつもこのパターン
600 :
132人目の素数さん :2005/10/01(土) 13:31:11
補足 形式的真により、別体系でより多くの命題が真であることが証明可能になることはある。 しかし、当たり前の事だが、全ての命題が、別体系で決定可能になる訳ではない
602 :
132人目の素数さん :2005/10/01(土) 13:42:57
切り返しって言葉を使うのは哲学厨 しかも・・・ 頼むから帰ってくれ
603 :
◆0wCTzeasu2 :2005/10/01(土) 14:05:18
ただ今一楽重雄「位相幾何学」 西川青季「幾何学」でジョルダン閉曲線定理の勉強中 証明の概略を書いていきたいと思います。
>>598 形式的証明にこだわるのは変だとは思うし、597の「真」の定義というのは所詮
数学的定義だから、いわゆる「真」ではない。しかし、チミはなにがいいたい
わけ。ご高説を滔々と述べられたらいかがですか。
605 :
132人目の素数さん :2005/10/01(土) 15:17:07
>>591 >カットって何のこといってるの?
おお、先走った。
ロッサーの方法による無矛盾性と、
カット抜きの証明の定義による無矛盾性は
別物だったな。
とはいえ、ここでは無矛盾性のようなものにも
異なる形式化が考えられ、しかもそれは体系に
よっては異なる意味をもつ場合があると考えられる
わけであるから、単純に形式化以降の話をチェック
したって「真偽判定」については無意味だってこと。
606 :
132人目の素数さん :2005/10/01(土) 15:23:10
>>593 >真偽判定(数学的な物に限らない)の
>対象にならない表現行為、という物もある
>例えば「これ旨いね」
レイ・スマリヤンの「認識論的悪夢」って話を知ってるかい?
「これは何色か?」という質問に、
「僕には赤く見えます」と答えた人が
「違う!」と反駁されてそこから延々と
議論が始まるわけだ。
そこでのもっとも重要なポイントは
「「僕には赤く見える」という発言が間違ってるなんて
他人に言えるわけがない」という発言が間違ってること。
ちなみに、上記の質問で提示された色は・・・赤!
607 :
132人目の素数さん :2005/10/01(土) 15:31:27
おまえら、皆踊らされているぞ これを発表した中村教授は今度大学院を 設立する。その話題作りの一つだ。まだ、 気が付かないのか。
608 :
132人目の素数さん :2005/10/01(土) 15:32:46
>>594 君の間違いは、真偽判定=証明探索だと思ってること。
でも実は違うんだ。つまり「これ旨いね」という発言に
何の証明がなくとも、君が旨いねと思ってそういったなら
それは真実なんだよ。
609 :
132人目の素数さん :2005/10/01(土) 15:41:14
>>597 >ある命題が真である、ということには
>ちゃんと数学的な定義があるんだけどな
それには二階論理を使う。実は二階論理は形式化できない。
ただ、数学的=形式的ではない。
>>598 >普通はない
君のいう"普通"が形式的体系でのことならその意味では正しい。
しかし、普通=形式的ではない
610 :
132人目の素数さん :2005/10/01(土) 15:46:02
>>604 追伸
>597の「真」の定義というのは所詮数学的定義だから、
>いわゆる「真」ではない。
597の定義を、無理矢理形式化してしまった
モデル理論の中で考えるならそうだろう。
しかし、数学的定義=形式的定義
だと考えるほうが実はおかしい。
中村ってのにロクのがいないな
612 :
598 :2005/10/01(土) 17:25:26
>597の定義を、無理矢理形式化してしまった >モデル理論の中で考えるならそうだろう。 「形式的な真」の定義ということは、そういうことだ。 それと、「普通の意味での真」は別物だろ もちろん、関連していると主観的に思えるように形式 化するけどな。
613 :
598 :2005/10/01(土) 17:27:46
アンカー忘れた。
>>610 > 597の定義を、無理矢理形式化してしまった
>モデル理論の中で考えるならそうだろう。
「形式的な真」の定義ということは、そういうことだ。
それと、「普通の意味での真」は別物だろ
もちろん、関連していると主観的に思えるように形式
化するけどな。
>>604 君と同じことが言いたかったんだと思われ
614 :
598 :2005/10/01(土) 17:41:00
「普通数学」(実在主義)では、「真」を定義にはしない。
ただ、数学的対象物に対する主張が正しいことを真と言い、
間違っていれば偽と言うだけだから
まあ、こんなものでも数学的定義と呼びたければ、それも
ありだと思うよ。結局、言葉の選択問題に過ぎないけどな
>>608 >君の間違いは、真偽判定=証明探索だと思ってること。
>でも実は違うんだ。つまり「これ旨いね」という発言に
>何の証明がなくとも、君が旨いねと思ってそういったなら
>それは真実なんだよ。
あーあ、やっちゃいましたか?うんうん。
君は
感想が本心であれば、正しい
感想が本心でなければ、間違っている
というように表現するんだね。俺はそんな言葉使いは
控えたいね。ところで、俺は本心から「これ旨いね」
は真偽判定の対象ではないと思っているわけだから、
俺は正しいよ。おっと、つい使ってしまったw
615 :
598 :2005/10/01(土) 17:46:06
形式主義 形式体系では真を定義できない。 しかし、そのモデル理論を形式化することにより 真が形式的に定義される。
616 :
598 :2005/10/01(土) 17:47:12
実在主義(普通数学)の場合の真については
>>614
617 :
598 :2005/10/01(土) 17:54:20
普通の(形式化されてない)モデル理論は、 形式体系を対象とした普通の実在主義数学。 しかし、そのモデル理論を形式化したもの こそが考察されるべき客体だ、と考えれば また形式主義が復活する。 形式主義は、永遠のいたちごっこ。しかし、 それが無意味だと思わない。ま、俺は普通 数学しか、やらないけどね。
618 :
132人目の素数さん :2005/10/01(土) 17:56:49
>>617 > 普通の(形式化されてない)モデル理論は、
> 形式体系を対象とした普通の実在主義数学。
完全性定理が好例か
619 :
132人目の素数さん :2005/10/01(土) 18:01:02
>>617 >形式主義は、永遠のいたちごっこ。しかし、
>それが無意味だと思わない。
というか、普通の数学にも終わりがないわけだから、
どちらにしても、数学は永遠のいたちごっこ。でも
それでいいwww
620 :
GiantLeaves ◆6fN.Sojv5w :2005/10/01(土) 18:04:24
621 :
132人目の素数さん :2005/10/01(土) 18:05:24
>>614 >>608 は結局、これだろ?
>ただ、「単に感想レベルの話」でも、他人との対立や矛盾を
>許容したくないだけでは?
622 :
132人目の素数さん :2005/10/01(土) 18:05:57
623 :
ニートドラゴン ◆Ylfrus2v8U :2005/10/01(土) 18:06:03
おい きんぐ
624 :
132人目の素数さん :2005/10/01(土) 18:14:28
>>619 形式数学も、普通数学もツマンネーよ。
数学やってる奴は皆、馬鹿。死ね死ね!
ハハハハハハ
625 :
132人目の素数さん :2005/10/01(土) 18:18:21
計算機は計算機の停止性を判定できないが、 実際には、計算機は止まるか止まらないかの二者択一しかないだろう。 同様に、真か偽ではある命題も、形式的に証明できるとはかぎらない。
626 :
ニートドラゴン ◆Ylfrus2v8U :2005/10/01(土) 18:22:57
数学者は安易に停止問題をわかったふうには語らない。 その理論的な奥深さを、自分の論理による理解として実感できるからだ。 ところが哲学厨は、微積分すらまともにできない分際で、そこらの雑学書に書かれた パラドックスや停止問題を「あたかも」自分が理解しましたというように容易に使う。 「〜は〜できないが、〜であろう」 理解していない。理解の中身なしに語れるほど数学の世界は浅はかではないさ。 ということで、哲学厨は嫌われるんだよ。 必死で努力してやってるやつらと同じレベルで語れるはずがないだろうが。
627 :
ニートドラゴン ◆Ylfrus2v8U :2005/10/01(土) 18:23:28
ワロスw
628 :
132人目の素数さん :2005/10/01(土) 18:24:35
>>625 基礎論の初歩。ただし、「証明図があれば、普通の意味で真」と
いうのも主観的判断。つまり、この形式化はおかしくないという
主観的判断。
ただし、通常はそのように期待するので、多くの場合、証明図が
あることが分かれば、普通の意味でも証明されたものと考える。
>>602 >切り返しって言葉を使うのは哲学厨
なんだそりゃ・・・そんなの聞いたこともないよ
こっちは哲学板のことなんか全然しらないってーの
ただ偶然にも、基礎論系のスレでいっつも同じことしてる人がいるようなんで
質問してみたまでだよ
631 :
132人目の素数さん :2005/10/01(土) 18:33:38
>>608 つーか、「これ旨いね」は真偽判定の対象ではないだろ。
ま、「『これ旨いね』という発言は本心である」なら、
まだ真偽判定の対象になりうるのかもな ← 本当かねw
632 :
132人目の素数さん :2005/10/01(土) 18:36:00
>>630 でもさ、普通数学では「真」の定義は存在しないし、
形式体系にも存在しない。としたら、「真」を定義
する場面ってモデル理論しかないよな
633 :
132人目の素数さん :2005/10/01(土) 18:39:42
モデル理論だって、形式体系を対象にした普通の主観的数学なのだから、 やはり「真」の定義がある訳でない。モデル理論を形式化した場合には 「形式的な真」の定義が現れる かなり、特殊な状況だぞ
634 :
132人目の素数さん :2005/10/01(土) 18:45:43
形式体系に対する「解釈」を固定化しないのが、モデル理論の特徴だと すれば、解釈ごとによって何が真になるのかが変わってくる。 ということは、真の定義はあるとも言える。ま、「解釈」を定義すると 言う方がしっくり来るが…
>>605 君は何を言ってるのかなあ、、
君が話の流れを強引に自分の持って行きたい方向に引っ張っていかない限り
カットの話なんて全く出てくるはずが無い
そもそもこのスレを何について話すスレだと思ってるんだか、、はぁ
>>598 「普通数学」って君の造語ですか?初めて聞いた
それは兎も角、そろそろ話を
>>1 と関連した話に戻しませんか?
637 :
132人目の素数さん :2005/10/01(土) 20:01:12
638 :
132人目の素数さん :2005/10/01(土) 20:02:57
>それは兎も角、そろそろ話を
>>1 と関連した話に戻しませんか?
数学板的には、面白い話題ではない。
ソフトウェア工学版にこそ相応しい。
639 :
132人目の素数さん :2005/10/01(土) 20:06:28
じゃ基礎論スレでやれよ
640 :
132人目の素数さん :2005/10/01(土) 20:08:53
いや〜、いろいろと釣りつ釣られつ、ってな感じで…
641 :
132人目の素数さん :2005/10/01(土) 20:31:35
普通者>>>(壁)>>>数学者=基礎論者
642 :
132人目の素数さん :2005/10/01(土) 20:33:08
数学やってる奴は、馬鹿。 死ね死ね死ね死ね死ね死ね 死ね死ね死ね死ね死ね死ね 死ね死ね死ね死ね死ね死ね
莫迦じゃなきゃ数学なんて出来ませんよw 死んでも出来ませんが
644 :
132人目の素数さん :2005/10/01(土) 21:40:42
>>608 あーあ、やっちゃいましたか?うんうん。 君は
感想が本心であれば、正しい
感想が本心でなければ、間違っている
というように表現するんだね。俺はそんな言葉使いは
控えたいね。ところで、俺は、「これ旨いね」は真偽
判定の対象ではないと本心で思っているわけだから、
俺は正しいよ。おっと、つい使ってしまったw
645 :
132人目の素数さん :2005/10/01(土) 21:53:36
普通の証明(主観) 形式的証明(客観) しかし、どちらも「真」であることについての 絶対的証明にはならない。これが現実
646 :
132人目の素数さん :2005/10/01(土) 21:56:11
647 :
132人目の素数さん :2005/10/01(土) 22:03:02
客観的に「○○」だ、っつーのは、 ルールに則って判断するに「○○」 だ、という程の意味だね、普通は。 絶対的にその判断が正しいという ことではない 絶対的な正しさには永遠に到達し ないのは、当たり前なんだからさ
648 :
132人目の素数さん :2005/10/01(土) 22:09:33
形式的証明が客観的だと言われるのも、 形式化された体系に則って判断するに 正しい、と言う程の意味だ。絶対的に 正しいとは、何ら言ってないのだよ。 しかし、ルールに則っての判断=絶対 という可笑しな脳内等式を持っている 奴が勘違いをすることがある訳だな。
649 :
132人目の素数さん :2005/10/01(土) 22:17:17
「何が客観的か?」という闘争は、 「ルールとして何を採用するのか ?」という闘争だ。
650 :
132人目の素数さん :2005/10/01(土) 22:19:50
「客観に逃げ込む」というのは、 自分を消すと言うことではない。 既存のルールに逃げ込むと言う 方が、適切だ。
651 :
132人目の素数さん :2005/10/01(土) 22:25:22
連投ウザイよ
ポントリャーギンの空砲
653 :
132人目の素数さん :2005/10/02(日) 00:20:29
A 旨い! B 間違ってます A そうだな。旨いじゃなくて、まいうーって感じ B 間違ってます A じゃ、ヤバイは? B 間違ってます A うめぇ〜、は? B まずいよ、これ A 君の口には合わないんだね。君にそう言われると、僕もそんな感じがしてくるなあ B …
654 :
132人目の素数さん :2005/10/02(日) 00:22:35
感想を感想として素直に受け取る奴と感想を真偽の対象にしようとする奴の会話です
655 :
132人目の素数さん :2005/10/02(日) 08:33:09
>>612-613 >関連していると主観的に思えるように形式化するけどな。
だったら、最後は形式ではなく主観で決めてんじゃん。
自分の存在を忘れるなよ(w
656 :
132人目の素数さん :2005/10/02(日) 08:41:44
客観的 客が観て受けるありよう
657 :
132人目の素数さん :2005/10/02(日) 08:57:12
>>617 >普通の(形式化されてない)モデル理論は
>形式体系を対象とした普通の実在主義数学。
>しかし、そのモデル理論を形式化したものこそが
>考察されるべき客体だ、と考えれば
>また形式主義が復活する。
君の間違いは、形式化されたものが客体だと考えていること。
実は形式化は客体ではない。客体でないからこそ、形式体系が
言い表しえるものを、モデル理論で考えるわけだ。
しかし、そのものとかいうのも、結局形式化してしまったら、
またそれが言い表しえるものを考えなくてはならない。
これは無限後退だね。
いいかい、そこで主体が責任をもつ必要があるんだよ。
君のように責任を恐れる臆病者には数学は無理なんだよ。
658 :
132人目の素数さん :2005/10/02(日) 09:07:27
哲学オタへ 集合論や論理式はあとでいいから 最低限 微積分とイデアルまではやってくれ 話が紙泡ねえ
659 :
132人目の素数さん :2005/10/02(日) 09:08:53
>>630 >普通数学では「真」の定義は存在しないし、
>形式体系にも存在しない。
>としたら、「真」を定義する場面って
>モデル理論しかないよな
その突っ込みは的外れ。
そもそも、形式体系が、いいたかったこと以外の意味も持ちえる
と示したのがモデル理論なのだから、これを形式マンセーの人が
持ち出すのは自爆である。
660 :
132人目の素数さん :2005/10/02(日) 09:12:14
>>636 >「普通数学」って君の造語ですか?
>>637 >単なる「普通の数学」の略だと思われ
余談だが、世の中にはひらがなを嫌い
漢字だけの熟語にしたほうが
カッコイイと思う馬鹿がいる。
661 :
132人目の素数さん :2005/10/02(日) 09:18:42
>>647 >客観的に「○○」だ、っつーのは、
>ルールに則って判断するに「○○」
>だ、という程の意味だね、普通は。
素人がそういう言葉遣いをするのは知っているが、
客観の本来の意味からすると間違っている。
662 :
132人目の素数さん :2005/10/02(日) 09:21:46
>>655 そんなの当たり前だっつーの
ルールに従って、判断したって事を客観的って言っているんだよ。
馬鹿め(w
それが言葉の使い方だよ
663 :
132人目の素数さん :2005/10/02(日) 09:28:06
>>647 >絶対的な正しさには永遠に到達しないのは、当たり前なんだからさ
前提条件が抜けたぞ。
「ルールに則るという行為で、絶対的な正しさを示すことはできない。」
これが正解。
しかし、正しさの判断は、常にルールに則っているわけではない。
特に、どのルールを取るか、という判断はルールに則っていない。
>>649 の「何をルールとして採用するのか?」は主観的である。
しかしだからといって必ず他人と相違するというわけではない。
哲学の人へ 客観がどうかとか、どうでもいいから Jordanの曲線定理の話をしませんか?
665 :
132人目の素数さん :2005/10/02(日) 09:29:30
>ルールに従って、判断したって事を客観的って言っているんだよ。 >馬鹿め(w 馬鹿は、常識を疑わない貴様だ。 考えないものに学問は無理だ。
666 :
132人目の素数さん :2005/10/02(日) 09:29:35
>>657 あのさ、君の言うような事はとっくに認識しているの
君の引用した所の後に、永遠のいたちごっこってあるでしょ。
だから、と言って形式体系が消えるわけじゃないよ。君の可笑しなとこだな
667 :
132人目の素数さん :2005/10/02(日) 09:30:34
>>664 >Jordanの曲線定理の話をしませんか?
君はできませんか?
ああ、できませんか。では、勉強してください。
君が知らないのなら話はできないでしょう。
668 :
132人目の素数さん :2005/10/02(日) 09:32:54
>>666 >だから、と言って形式体系が消えるわけじゃないよ。
私は形式体系が消えるとは一度もいっていないが。
君が「ルールに則る」ことに異常なエクスタシーを
感じる性癖だと感じたからその愚かさを笑ったまでだ(w
669 :
664 :2005/10/02(日) 09:34:58
>>667 何独り言言ってるんですか?
勝手に>ああ、できませんか。
とか言われても困るんですが、、
670 :
132人目の素数さん :2005/10/02(日) 09:36:32
>>669 何甘えてるんですか。
そりゃ困るでしょう。
君が無知で自分から話を始められないから
他人が話してくれるのを待って焦れてるんでしょう。
そのまんま黒焦げになってください(w
671 :
664 :2005/10/02(日) 09:38:47
>>670 主観がどうのとか客観がどうのとか延々と
関係無さそうな話を続けてる人が居るような気がしたんですけど、、
気のせいですか?
672 :
132人目の素数さん :2005/10/02(日) 09:50:47
>>659 誰が形式マンセーなの?
モデル理論があるのは「形式体系を調べる事には意味がある」と考えているから。
君のように一つの哲学的(藁)主張をしてそれで終わりじゃないし、
モデル理論という分野が出来る前から、君の言うような事は常識に過ぎない。
形式体系が絶対じゃないのは当たり前の事だが。だからと言って、無意味と言う訳でもない。当たり前だが
君の間違いは「形式化に意味があると普通に考えてる人達が
形式体系から読み取った出張は絶対だとも考えている」と君が思ってる事にある
673 :
132人目の素数さん :2005/10/02(日) 09:55:51
>>671 Jordanの曲線定理の話をしませんか?といいつつ
自分からは話できないのは無知だからでしょ?
違いますか?(wwwwwww
674 :
132人目の素数さん :2005/10/02(日) 09:58:20
規則を作り、それに則って判断することに(も)意味があると考えているからって その人達が規則は絶対だと考えてる訳じゃない事は、当たり前。 なぜなら、規則を作ったのは自分だから
675 :
664 :2005/10/02(日) 10:02:22
>>673 あのね、上のほうでは
>>1 の件について普通にレスしてたんだけど
モデル理論がどうの、とか主観がどうの、とか言う人ばかりだと
話しづらいんですよ
>君が知らないのなら話はできないでしょう。
自分はスレに沿った話題を話したいのに
回りの人間のせいでできない、みたいなこと言わないで貰えませんか?
明らかにそういう状況ではありませんので
676 :
132人目の素数さん :2005/10/02(日) 10:02:32
>>672 >一つの哲学的(藁)主張をしてそれで終わりじゃないし
一つしかない君の迷信を延々と繰り返されても迷惑だよ。
「・・・には意味がある」というのは無意味
「昔から常識」というのは誤り
「・・・が絶対じゃない」というのは苦し紛れの言い訳
単に、君自身無意識であったことを他人の指摘で
やっと気づいただけ。全ては君の軽率さによる誤り。
677 :
132人目の素数さん :2005/10/02(日) 10:05:37
>>675 >モデル理論がどうの、とか主観がどうの、
>とか言う人ばかりだと 話しづらいんですよ
では話さなければいい。
>自分はスレに沿った話題を話したいのに
>回りの人間のせいでできない、みたいなこと
>言わないで貰えませんか?
君がいっているのはそういうことだが。
>明らかにそういう状況ではありませんので
明らかにそういう状況だが、君が恥ずかしさから
認めたがらないだけ。そりゃそうだろう。ただの
教えてクンだなんていったら「ばーかばかばか」
と罵られるのがオチ。実際は罵ってるほうも、
同類のバカなんだが(w
678 :
132人目の素数さん :2005/10/02(日) 10:07:40
>>674 >規則を作ったのは自分だから
あとからこっそり相手のいってることをなぞったからといって
自分がはじめにいってたことの誤りが自分の中から消せるわけ
ではない。
679 :
132人目の素数さん :2005/10/02(日) 10:12:42
あのさ、俺は普通数学しか研究してないけど、だからと言って、形式化に意味がないとは考えてない。 もちろん、そういう事をしてない以上、そういう事をしなければいけないとも思ってない 形式化に意味があると考えるのは普通。だからと言って、形式化しなければいけないと考える気違いには 生憎、お目に掛かった事がない
680 :
132人目の素数さん :2005/10/02(日) 10:15:17
>>234 3次方程式が虚数解を持つ→グラフがx軸を1回しか交差しない→極小値が0より大きい
をヒントにがんばってみて!
681 :
132人目の素数さん :2005/10/02(日) 10:15:41
>>679 「普通の数学」しか知らないんなら、
形式化とはどういうことかなんて
分かってないだろ。
だったら知ったかぶって口挟むなよ。
みっともないんだよ。バカが
682 :
680 :2005/10/02(日) 10:16:17
すいません誤爆しました
683 :
132人目の素数さん :2005/10/02(日) 10:17:30
>>681 >>679 には>研究してない
と書いてあるようだが?
もしかして計算機による定理の証明の話には、
それを専門に研究している工学者しか話をしちゃいけないのか?
685 :
132人目の素数さん :2005/10/02(日) 10:21:06
規則に則って判断する事を客観と言う。規則を作ることは主観。 ここで主観が出て来たからと言って客観が消える訳じゃない。間違いが分かりましたか?
686 :
132人目の素数さん :2005/10/02(日) 10:29:07
形式化をしてない人間が形式(客観)化マンセーでないのは当たり前 客観に意味を認めてたら、客観マンセーなのかよ?(w
687 :
132人目の素数さん :2005/10/02(日) 10:43:36
>>681 あっ、そうか。君の周りには「形式化マンセー」って
基地外がいるのか?それを叩いてるつもりだったのか
生憎、ここは数学板。普通の数学を勉強してる人間が
中心。だから、形式化マンセー君に出会うのは難しい
のでは?普通に数学をやってる人間は形式化の意義を
認めつつ、別に絶対視してない。絶対視してないのは
それをやってないんだから当たり前なんだが
688 :
132人目の素数さん :2005/10/02(日) 10:47:45
間違い1.「意義を認めている ⇒ 絶対視している」
>>687 間違い2.「主観が出て来た ⇒ 客観が消える」
>>685
689 :
132人目の素数さん :2005/10/02(日) 11:00:16
>>661 素人がそういう意味として使っていることを知ってるなら
そういう意味として受け取ればいいんじゃないのか?
ま、知らなかったのなら、受け取りようもないがなあ
君の間違い3.他人の発言の言葉の使い方の意味を認めず、
自分の使い方の意味で解釈することに拘り、
それを押し付けようとすること
で、さ、「君の言葉の使い方」では客観はないのだろう?
で、ないものに何でそんなに拘るのかな?
ま、俺には君がどういう意味で客観という言葉を使ってる
のかが、そもそも分からないんだけどさ。
690 :
132人目の素数さん :2005/10/02(日) 11:16:59
ここは数学版だから、「客観」という言葉は素人の意味で使われる。 哲学的な「客観」について議論したいのなら、哲版に逝ったほうが いいと思われwww
691 :
132人目の素数さん :2005/10/02(日) 11:34:38
間違い4.「正しいこと」を意識してなかったら、 あるいは、相手の発言からそれが読み 取れなかったら間違いだと考えること 正しい4.「間違ったこと」を意識していたら、 あるいは、相手の発言からそれが読み 取れたら、間違いだと考えること
692 :
132人目の素数さん :2005/10/02(日) 11:34:45
693 :
132人目の素数さん :2005/10/02(日) 11:38:51
>>691 普通(素人)の意味で「客観」という言葉が使われているのに、
何だか哲版の意味でそれを解釈して、「間違っている」と判断
しただけでしょ。
客観がないとか、どうとか、繰り返してる人は。いい加減、
間違えを認めたら
694 :
132人目の素数さん :2005/10/02(日) 11:42:45
696 :
132人目の素数さん :2005/10/02(日) 12:26:01
>>691 違うな。
基地外4.「正しいこと」を意識してなかったら、
あるいは、相手の発言からそれが読み
取れなかったら間違いだと考えること
ふつう4.「間違ったこと」を意識していたら、
あるいは、相手の発言からそれが読み
取れたら、間違いだと考えること
Jordan の閉曲線定理は piecewise linear に限るもの、微分可能曲線に限るもの 一番一般的なものなど、ありますが、どの証明がなされたのでしょうか? また、証明検証の問題がからむと、一般的な定理の方が必ずしも簡単にはならない ということもおきると思われます。 このような話題も色々あると思いますがね、、、。
698 :
132人目の素数さん :2005/10/02(日) 13:38:04
>>689 >で、さ、「君の言葉の使い方」では客観はないのだろう?
>で、ないものに何でそんなに拘るのかな?
>ま、俺には君がどういう意味で客観という言葉を使ってる
>のかが、そもそも分からないんだけどさ。
おい、お前はバカか?
「客観」は存在しないのだから、理解する必要もないだろが
>一般的な定理の方が必ずしも簡単にはならない そうですかね まあ証明が簡単になるための条件をゴタゴタくっつけた方が簡単にはなるんでしょうが
700 :
132人目の素数さん :2005/10/02(日) 13:40:08
哲学君は存在しないものについて議論するのさ。 話がまとまるわけがないw
いずれにせよ、今回の報道で個人的に一番許せないのが 「完全証明」って言葉なんだよな 自分の業績を過大評価させるために大げさな言葉を使う まあ良くあることではあるがいくらなんでもやり過ぎだと思うけどな
702 :
132人目の素数さん :2005/10/02(日) 13:42:36
703 :
132人目の素数さん :2005/10/02(日) 14:04:43
そういえば黒木さんの掲示板も最近は寂れてるねえ
705 :
132人目の素数さん :2005/10/02(日) 14:10:27
706 :
132人目の素数さん :2005/10/02(日) 14:15:10
>>697 >どの証明がなされたのでしょうか?
なぜ、自分で証明を読まないのでしょうか?
もしかして読めないのでしょうか?
707 :
132人目の素数さん :2005/10/02(日) 14:15:34
夫馬です。 「完全証明」という言葉で、今までの数学的証明が不十分だったと 印象操作して(強い主張)、それを非難されれば「形式的証明」と いう意味だ、と批判をかわします。このようなことはポモに限った ことでなく、数学的な分野でもあることです。まずは自分の身近な 分野から叩こうぜ、な >そういえば黒木さんの掲示板も最近は寂れてるねえ 私がやってやりました!
708 :
132人目の素数さん :2005/10/02(日) 14:18:49
>>684 >計算機による定理の証明の話には、
>それを専門に研究している工学者しか
>話をしちゃいけないのか?
なぜ形式的証明の意義という数学の哲学の話に
いきなり工学者がでてくるんだ?唐突だろ?
709 :
132人目の素数さん :2005/10/02(日) 14:21:24
>>685 >規則に則って判断する事を客観と言う
>>687 >素人がそういう意味として使っていることを知ってるなら
>そういう意味として受け取ればいいんじゃないのか?
素人はいつでも傲慢だ。自分が間違ってるときは考えない。
考えないことによって間違いを意識せずにごまかす。
>>706 20万行も読む気力と暇の有る人は少ないかと
711 :
132人目の素数さん :2005/10/02(日) 14:23:02
>>707 >まずは自分の身近な分野から叩こうぜ、な
U沢さんのことか?w
712 :
132人目の素数さん :2005/10/02(日) 14:24:47
>>701 >いずれにせよ、今回の報道で個人的に一番許せないのが
>「完全証明」って言葉なんだよな
形式的=客観的っていってる人は
形式的証明=完全証明っていってるように聞こえるが、どうか?
違うなら、客観のどこが完全でないか説明してちょ?
>>708 だからここは哲学板でもないし、数学の哲学のスレでも無いよ、というのはまあ別の話として、
「俺は普通数学しか研究してないけど」に対して
それなら口を挟むな、というレスがあったわけで、
それなら形式的証明に関して研究している人
(そういう人を工学者と呼ぶか数学者と呼ぶかはまあ呼び方の問題ね
中村教授が工学部の人であるのは間違いないけど)
しかレスするな、と言ってるのかな?と疑問を持つのは自然な事だと思いますが
715 :
132人目の素数さん :2005/10/02(日) 14:30:15
>>713 だから、客観の普通(素人)の意味は、
ルールに則ってという程の意味だって
言ってるじゃんか、ね
>>714 普通の証明と形式的証明の違いを論じるのは数学の哲学だよ。
知らなかった?知らなかったなら知って。今すぐ。
>「俺は普通数学しか研究してないけど」に対して
>それなら口を挟むな、というレスがあったわけで、
数学の哲学をバカにするような無知蒙昧な輩に
口を挟むなというのは当然じゃない?
君はチーマーのオヤジ狩りに賛同するわけ?
狂ってるね。人間としてさ。
717 :
132人目の素数さん :2005/10/02(日) 14:31:28
>形式的証明に関して研究している人 >しかレスするな、と言ってるのかな? 形式的証明に関して研究している人が 形式的証明の意義を議論するにふさわしい とは限らないな。 数学を研究している人が 数学の意義を議論するに ふさわしいわけではないように。
719 :
132人目の素数さん :2005/10/02(日) 14:36:11
>>717 哲学的な客観ってないんだよね。ないんなら、知らなくても
いいと思うだけど、違うの?哲学って奥が深いや。うんうん
そういう深い事が分かるなんて、君は凄い人なんだ。僕には
難しくて分からないや。ごめんね
720 :
132人目の素数さん :2005/10/02(日) 14:38:29
>>718 してもいいだろ?そうじゃない人も、もちろんしていい。
そんなことに客観的「資格」を求めるのか?w
>>716 このスレは飽くまで信州大の人がJordan曲線の定理を計算機で証明しましたよ、
というニュースのスレであって、「数学の哲学」の観点から語らないといけない、
という縛りはないよ(君の脳内にはあるのかもしれないが)
別に普通の数学研究者の観点から今回の証明を評価するのも自由だ
>>679 のどこが数学の哲学を莫迦にしてるんだ?
哲学のての字も書いて無いし、普通の数学研究者の実感を表明してるだけに見えるんだが
それをチーマーのオヤジ狩り呼ばわりする君のほうが狂ってるね。人間としてさ。
それとも「数学の哲学」では形式化に意味がある、だけでは飽き足らず
形式化しなければいけない、と極端なことを言わなきゃ無知蒙昧呼ばわりされるのかね?
それじゃほとんど宗教じゃないですか
722 :
132人目の素数さん :2005/10/02(日) 15:06:25
>>719 いや、君と違って頭のいい人なら、哲学的な「客観」の意味も
それが存在しないことも理解できるんだよ、きっと。
頭のいい哲学さんに、君は見捨てられるのさ
>哲学さん
啓蒙活動、もっとよろしく!俺、むちゃ理解したいよ♪
723 :
132人目の素数さん :2005/10/02(日) 15:35:58
以上、素人くんと哲学さんの対話を要約すると 次のようになります。 653 :132人目の素数さん :2005/10/02(日) 00:20:29 A 旨い! B 間違ってます A そうだな。旨いじゃなくて、まいうーって感じ B 間違ってます A じゃ、ヤバイは? B 間違ってます A うめぇ〜、は? B まずいよ、これ A 君の口には合わないんだね。君にそう言われると、僕もそんな感じがしてくるなあ B …
>>699 一般的な定理が成立しているとして、具体的な場合に成立することを示すには、その
具体的な場合が定理の条件を示す必要がある。これは、べつに計算機で検証できる証明
にかんしたことでなくても大変なことはよくある。計算機での検証を考えると具体的
な場合というのは、その対象の表現の問題もあるので、かなり面倒なのではないで
しょうか?
一般的な定理は、定理の条件が証明に合わせて提示されている場合、証明をつくること
が簡単ということはありえる。どちらにしても数学での証明とは異なったところの工夫
が必要なはずだが、ともかく、piecewise linear 版なんですか、それとも一般版なん
ですかね。こんなことも話題にならないとすると、ニュースが Wiles の定理の証明だ
ったとしても、おんなじようにやり合うわけなんだ。
725 :
132人目の素数さん :2005/10/02(日) 15:41:39
>>723 Bが本当に欲しい反応は、このレストラン
駄目じゃん、というものなのです。まあ、
一生かかっても、無理でしょう。
726 :
132人目の素数さん :2005/10/02(日) 15:43:47
> こんなことも話題にならないとすると、ニュースが > Wiles の定理の証明だったとしても、おんなじよう > にやり合うわけなんだ。 そう思われwww
単なる新聞ネタ 杉村太蔵と同レベル
728 :
132人目の素数さん :2005/10/02(日) 16:27:21
>>716 なかなか楽しかったよ、オヤジ狩り。
言っとくけどな、俺たちはチーマーじゃねえ
カラーギャングだ。今度、チーマー呼ばわり
したらぶっ殺すからな。覚えとけw
729 :
132人目の素数さん :2005/10/02(日) 16:39:48
用語解説 オヤジ=哲厨 チーマー=形式数学者 ギャング=普通数学者
730 :
132人目の素数さん :2005/10/02(日) 16:44:25
前回までのストーリー ギャングを見て、「チーマーだ。怖い」とオヤジが言ったのに 切れたギャング達が、オヤジに襲い掛かって、ぼこぼこにする。 最後に「俺たちはチーマーじゃねぇ」と捨て台詞を吐き捨てる。 オヤジは、ギャングが切れた理由を考えるのだが…
>>721 「信州大の人がJordan曲線の定理を計算機で証明しましたよ」
というニュースに対して、どういう議論をしようと自由だが、
普通の証明と形式的証明との差異に対して、ルール順守が客観だ
とかいうナイーブな態度を強制するのは間違っている。
そういう狂信家は出て行くべきだ。
732 :
132人目の素数さん :2005/10/02(日) 17:45:10
> 普通の証明と形式的証明との差異に対して、ルール順守が客観だ > とかいうナイーブな態度を強制する 強制はしてないだろ。「客観」という言葉の意味を説明しているに 過ぎないからな
>>723 まったく要約になっていない。なぜなら中身が異なるから
A「俺が”旨い”といったとき、これは真偽とは無関係だ」
B「なぜ?君が旨いと思って”旨い”といったなら、それは真実だろう」
A「しかし、お前には俺がどう思ってるか分かるまい」
B「そりゃ僕には分からんよ。しかし僕に分からないからといって
真偽とは無関係だということにはならないよ。」
A「ハァ?真か偽か分からないのに真偽を云々するなんてバカだろ」
B「おや、君は自分でも旨いと思ってないのに旨いって言ってるのかい?」
A「俺にわかっても、お前にわからないんなら意味がないだろ」
B「そんなことはない。真偽は結局主観的判断だよ。
それがたまたま君と僕の間で一致したからといって、
主観とは独立な客観の存在を考える必要はないだろ?」
>>725 まったく見当違い。
Bは、Aの真偽と証明に関する杓子定規な態度に対して、
その盲点をついてナンセンスさを指摘したまで。
しかしながらAは自分の主観性と向き合うことを恐れて
ナンセンスさを認めるに至っていない。
735 :
132人目の素数さん :2005/10/02(日) 17:56:46
だから、君は、君なりに「哲学的な客観」とやらの言葉の説明から スタートすればいいのだ 普通(素人)の言葉では「客観」とはルールに則って、という意味 なのだから、勝手な解釈で素人の発言を捻じ曲げるのを、止めれば いい それに普通(素人)の言葉の意味では、「主観>客観」も「客観> 主観」もどちらも出て来はしない。人が客観という言葉を使うとき 「客観>主観」と考えているという思い込みをしているようだが、 そんなのは「客観的=絶対的」という脳内等式でも持ってなければ 出て来ない。生憎、そういう基地外には数学版では出会えないから 出会いたければ、哲版に逝ったほうがいいw
>オヤジ=哲厨 >チーマー=形式数学者 >ギャング=普通数学者 実際には、哲厨は「見かけはオヤジだが、実は元暴走族のヘッド」 だったりする(w
737 :
132人目の素数さん :2005/10/02(日) 18:03:01
>>733 違うな。まじめに言おう
A 俺が”旨い”といったとき、これは真偽とは無関係だ
B なぜ?君が旨いと思って”旨い”といったなら、それは真実だろう
A その場合は「旨いと思っている」ということが真実だ。「旨い」と
いうのは真偽判定の対象でないことに変わりはないよ。
「旨い」という言葉と「旨いと思っている」という言葉は別物。君は
すぐに勝手な言い替えをする。因みに、「旨いと言った」というのも
ある。全て、別物だが。
>>735 君は普通という言葉で強制をしてるね。
それは捻じ曲げだから止めればいい。
素人の普通は大抵間違ってる。
なぜなら考えてないから。
自分のスカスカな脳味噌の中が全てだと思ってる。
739 :
132人目の素数さん :2005/10/02(日) 18:05:58
1.旨い 2.旨いと思う 3.旨いと言った 1は論外。2は旨いと思っていれば真実、思っていなければ嘘。 3は言ったのなら真実、言わなかったのなら嘘。当たり前だが。
740 :
132人目の素数さん :2005/10/02(日) 18:08:53
>>738 じゃあ、どうぞ、どうぞ。貴方の普通(哲学)の客観を
説明したらいい。
741 :
132人目の素数さん :2005/10/02(日) 18:12:50
哲学さんの世界では、「旨い」=「旨いと思う」という脳内等式がある ようです。 哲学さんの世界は、素人くんの世界と違って奥が深いのです
742 :
132人目の素数さん :2005/10/02(日) 18:15:24
1.も〜、駄目、死んじゃう 2.も〜、駄目、死んじゃうって感じたの 3.も〜、駄目、死んじゃう、なんて叫んじゃった 全て別物ですw
743 :
132人目の素数さん :2005/10/02(日) 18:18:05
1.答えはAだ 2.答えはAだと思う 3.答えはAだと言った 全て別物だけど…
744 :
132人目の素数さん :2005/10/02(日) 18:27:55
>>738 早く。哲学(普通)の客観の意味と、それが存在しないことを
教えてー!興味津々なのー。それが分かったら、私も一人前に
なれる気がするわ。
745 :
132人目の素数さん :2005/10/02(日) 18:34:20
>>728 >>736 用語解説(改訂版)
オヤジ(元暴走族のヘッド)=哲厨
チーマー=形式数学者
ギャング=普通数学者
746 :
132人目の素数さん :2005/10/02(日) 18:36:07
早く、早く。客観ってなーにー 待ちきれないよー
747 :
132人目の素数さん :2005/10/02(日) 18:40:52
>>730 >>745 予告
次回は、ギャングに復讐を誓ったオヤジが
昔の暴走族(哲厨)仲間を集めるために、
お郷(哲版)に帰るシーンからになります。
748 :
132人目の素数さん :2005/10/02(日) 18:49:10
>>746 哲版から仲間を集めてるんだ、待っててやれ。
それでも我慢できないなら、オヤジと一緒に
哲版まで逝ってきなさい。いろいろ、教えて
くれるよ、きっと。それに、皆に気に入られ
れば君も鉄柱仲間に入れてもらえるかも知れ
ないぞ!
749 :
132人目の素数さん :2005/10/02(日) 18:57:57
1.鳥 2.鳥を思う 3.鳥を見た 4.鳥と言う 全て違うな…
750 :
132人目の素数さん :2005/10/02(日) 19:03:52
ここら辺りで、別の意味の客観(=客体)を出して見ようかw こっちの方が、鉄柱的には食いつきがいいのでは? 普通数学 3(客体)、9(客体)3×3(客体) 3×3=9(客体に関する解釈) 形式数学 3×3=9(客体)証明図A(客体) Aは3×3=9の証明図である(客体に関する解釈)
751 :
132人目の素数さん :2005/10/02(日) 19:14:57
素人(ナイーブ君)は、生まれながらの可能世界意味論者。 生半可な鉄柱では太刀打ちできないね。
752 :
132人目の素数さん :2005/10/02(日) 19:16:01
数学屋は、無自覚の可能世界意味論者。 生半可な鉄柱では、太刀打ちできない。
753 :
132人目の素数さん :2005/10/02(日) 19:44:15
基礎論の招待講演者だそうです Rod 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
754 :
132人目の素数さん :2005/10/02(日) 19:45:10
アメばっか、なんだけど… 大学が
755 :
132人目の素数さん :2005/10/02(日) 20:26:29
>>750 形式数学では
証明図「A」(客体)は、真偽判定の対象ではない。
「Aは証明図である」(客体に関する解釈)は真偽
判定の対象だ。
「君」という物体(客体)、「旨い」という文字、
音声、或いは‘感覚’(客体)のいずれも真偽判定
対象外だな。
「君は旨いと感じている」、「君は旨いと言った」
(客体に関する解釈)は真偽判定対象だ。
756 :
ニートドラゴン ◆Ylfrus2v8U :2005/10/02(日) 20:34:38
もうわけわからんよ 次スレは絶対に哲学板でやってくれ。 立てたら荒らす。
757 :
132人目の素数さん :2005/10/02(日) 20:36:39
>>733 基地外5.「客体」と「客体に関する主体の解釈」の区別が
できない。
>>755 &
>A 俺が”旨い”といったとき、これは真偽とは無関係だ
>B なぜ?君が旨いと思って”旨い”といったなら、それは真実だろう
>A その場合は「旨いと思っている」ということが真実だ。「旨い」と
> いうのは真偽判定の対象でないことに変わりはないよ。
旨いという「感覚」(あるいは音声、文字etc.)は客体だ。
客体に対する主体の解釈ではない。感覚と解釈の区別ができ
ないのかい?
人間の発言行為の多くは、解釈の表現ではないのだ。感覚の
表現。この「多く」のという発言自体がな
ここら辺りで食い付いて来てね!
758 :
132人目の素数さん :2005/10/02(日) 20:42:36
760 :
132人目の素数さん :2005/10/02(日) 20:47:38
鉄柱さんへ 早く帰って来て、熱弁を振るってくれ!
762 :
132人目の素数さん :2005/10/02(日) 21:00:09
>>761 俺は普通数学屋だよ。数学版にまで来てくれた鉄柱と
心の触れ合いを楽しむために、彼と同類の振る舞いを
しているんだ。コミュニケーションしよう
彼と同類の存在に堕ちた、と言ってくれ
764 :
132人目の素数さん :2005/10/02(日) 21:02:46
基礎論系の(話題に持っていけそうな)スレには、毎回必ず
「お前らは形式化されたものこそ正しいと思っている!
お前らは形式化されたものこそ論理だと思っている!
だがそれは間違いだ!
お前ら形式化マンセー野郎共の認識を俺様が改めてやる!」
という決意に燃えて啓蒙活動に励む人が現れます。
「スレ違い」「話題を無理矢理そっちに持っていくな」「脳内敵とのバトルはよそでやれ」
などと注意しても、
>>664-677 みたいに脊髄反射で悪態をついて、しつこくスレに居座り続けようとします。
766 :
132人目の素数さん :2005/10/02(日) 21:27:32
餌だよ。餌
>>757 のネタ
> 言語と行為
> J.L.オースティン (著), 坂本 百大 (翻訳)
767 :
132人目の素数さん :2005/10/02(日) 21:28:56
別のところでは、これも使ってるよ。状況によって使い分けてるから >名指しと必然性―様相の形而上学と心身問題 >ソール・A.クリプキ (著), 八木沢 敬 (翻訳), 野家 啓一 (翻訳)
768 :
132人目の素数さん :2005/10/02(日) 21:33:55
>>767 ごめん。こっちの方がいいかも…
>ウィトゲンシュタインのパラドックス―規則・私的言語・他人の心
>ソール・A.クリプキ (著), 黒崎 宏 (翻訳)
いわゆる「数学の哲学」の人って 知ってる数学が非常に特殊なんだよね 基礎論関係か、あとは高校レベルか 計数工学科の学部生ほどの知識があれば 彼らの中では物凄い博学、ということになるんだろうけどw
770 :
132人目の素数さん :2005/10/02(日) 21:41:31
>>769 佐々木力だ(禿
じゃなくて(藁
>夫馬でした。
771 :
132人目の素数さん :2005/10/02(日) 21:49:05
> 実在論と科学の目的 > K・ポパー (翻訳), 小河原 誠 (翻訳), 蔭山 泰之
772 :
132人目の素数さん :2005/10/02(日) 21:52:20
加藤先生の「ゼータさんを見つけようと思って日本昔を買ってきて 読んだんですが、無駄でした。」って結構、受けてたな 俺はイマイチついていけなかったよ >夫馬でした
たしかに受けるかもw
774 :
132人目の素数さん :2005/10/02(日) 21:56:42
>>773 夫馬です。
ICMの総合講演でも、これを期待されているらしいよ
早く来ないかな、鉄柱…
775 :
132人目の素数さん :2005/10/02(日) 22:09:46
>>769 夫馬です
いや、鉄柱は「数学の哲学」の人ではない。俺が
ネタに使ったのは、その分野の基礎文献だから。
それも見抜けてない
776 :
132人目の素数さん :2005/10/02(日) 22:14:57
基礎論初歩について少し本を読んだのも 数学の哲学に関して少し本を読んだのも、 ずっと昔のことで、あんまり良く覚えて ないんだがな 夫馬
777 :
132人目の素数さん :2005/10/02(日) 22:15:51
あぼ〜ん
778 :
132人目の素数さん :2005/10/02(日) 22:52:08
>>777 ラッキー
779 :
132人目の素数さん :2005/10/03(月) 07:14:46
>鉄柱さんへ 早く、哲学的な「客観」という言葉の意味を説明してくれよ。
780 :
132人目の素数さん :2005/10/03(月) 07:15:47
>>779 あいつ、駄目だろ。「数学の哲学」の初歩も知らないんだから
781 :
132人目の素数さん :2005/10/03(月) 08:03:12
782 :
132人目の素数さん :2005/10/03(月) 08:14:52
783 :
132人目の素数さん :2005/10/03(月) 09:18:26
前のほうで、数学の(非形式的)証明は厳密な形式的証明に書き換えることが出来る とか、かならずしもそう言えないとかとあったけど。そう言えないといった人 に聞きたいんだけど、書き換えることが出来ない数学の推論って例えばどんな ものがあるんだろう? 数学の(正しくかつ広く認められた)証明の推論というのは 単純かつ明らかな推論の積み重ねだと思うんだけど。
784 :
Euclid.Anal.Expert ◆wRpISOr80k :2005/10/03(月) 10:13:06
推論でなくても、幾何学的な性質や線形から導かれる実際の数学的構造から明らかになる場合もあるだろ。 俺の場合はそういうのがしっくりくる。数列の性質の証明問題なんかはどっちかといえば苦手だ。
785 :
132人目の素数さん :2005/10/03(月) 10:23:31
>>784 幾何学的って言っても高次元幾何だと直感はあてにならないんで、
厳密に論理に従うしかないんじゃないの?
786 :
132人目の素数さん :2005/10/03(月) 10:24:25
推論が「適切に」形式化されている の適切にが今の所マジックワードで 残ってるから、まずはそこを何とか せねば 実は、真であるにも関わらず普通の意味で証明できない命題があるかという段階で 証明がマジックワードになっているんだけどね
787 :
Euclid.Anal.Expert ◆wRpISOr80k :2005/10/03(月) 10:25:28
>>783 すごく簡単にいえば、命題にとって必要十分になる全ての場合を数え上げて表にでもできるなら完全証明。
それができそうにないなら、完全証明は難しいってことだろ。
πにまつわるエトセトラが一番わかりやすい例かも。
788 :
132人目の素数さん :2005/10/03(月) 10:47:16
(適切な)形式的証明に書き換えることが出来る証明=十分な証明 出来ない証明=不十分 と定義をすれば、十分な証明は適切な形式証明に書き換えることが できる。 ところで、形式証明には「厳密」と「厳密でない」の区別がない。
789 :
132人目の素数さん :2005/10/03(月) 10:57:05
>>788 当たり前というか、無意味。AはAであると言ってるのと同じ
790 :
132人目の素数さん :2005/10/03(月) 11:00:34
>>787 >πにまつわるエトセトラが
そのエトセトラの1つを具体的に上げてみてくれないか。
なるべく簡単な例を
791 :
132人目の素数さん :2005/10/03(月) 11:11:48
>>789 なら、定義じゃなくても、「性質」としては認める?
最初の問題はこれを認めるか、認めないかの価値観の
問題。
792 :
132人目の素数さん :2005/10/03(月) 11:13:54
>>789 結局、結論を得ようとすると当たり前の話になるということか…
793 :
132人目の素数さん :2005/10/03(月) 11:16:35
>>788 「十分」、「適切」が双方ともに感覚の問題だからな。
近いけれどもちょっと違う、というのが本音。
794 :
132人目の素数さん :2005/10/03(月) 11:19:05
>近いけれどもちょっと違う、というのが本音。 中には 全然、違う! とか言う奴もいるかもなwww
795 :
132人目の素数さん :2005/10/03(月) 12:29:46
数学の偏差値が代ゼミで30なんですけども、赤チャやっても意味無いですよね? だけど先生が言うんですよ、「俺は赤チャを薦めるぞ」って もうアフォかとバカかと俺は偏差値30なんだと、あんなもんわからないと、 だから先生に言ってやったんです。「買ってみたんですけど全然わかりません」 そしたら先生が「アフォか!あの程度もわからないのか、じゃ黒大数やれよ」 それで僕は先生のいうとおり黒大数を買ったのです。 「すいません、黒大数も全然わからなかったんですけど・・・」 「はぁ?お前はどうしたいわけ?俺を困らせたいのか?それ以前にお前はたぶんで物を語るな!!だからお前は彼女に振られるんだよ!!」 それでついに僕は切れたんです 「ってかテメー俺は糞バカだって知ってるだろ!!偏差値30、わかる?30だよ30! 数学の偏差値30って言ったら哲学科のレベルだぞ!哲学科レベルの奴があんなもんできるわけねーだろ!!」 その後に少し沈黙があって、 「・・・そんな言葉口にしちゃいけない、やつらはいくら頑張っても数学は出来るようにならないんだ、お前はまだ可能性があるけどな」 「先生すいません。つい」 「いいんだ。ただしこれからは“哲学科”と“数学”の関係を口にしてはいけない、これは差別用語だからなわかったか?」 「はい」
796 :
132人目の素数さん :2005/10/03(月) 13:47:08
797 :
132人目の素数さん :2005/10/03(月) 14:44:08
798 :
132人目の素数さん :2005/10/03(月) 15:49:10
>>757 >感覚と解釈の区別ができないのかい?
主体と客体の区別をしちゃうのかい?(w
オースティンのチンカスは旨いかい(w
799 :
132人目の素数さん :2005/10/03(月) 15:53:52
>>775 ヴィトゲンシュタインは哲学書を読まないことで有名だった。
800 :
132人目の素数さん :2005/10/03(月) 16:05:23
>>769 知ってるのは算数だけだ(w
しかし全て算数で書ける、とゲーデルはいっている(w
(いや、本当はゲーデルはそうはおもってなかったんだが
クリプキともう一人の人がそれを示しちゃったんで
ゲーデルは心底驚き呆れたらしい)
801 :
132人目の素数さん :2005/10/03(月) 16:58:41
>主体と客体の区別をしちゃうのかい?(w それはポパー?
802 :
132人目の素数さん :2005/10/03(月) 17:06:10
改めてご紹介に預かりました夫馬(ヒロ)です。 総合司会をさせて頂く事になりました。 さてっ、皆様お待ちかねの鉄柱が帰って来ました! まずは、哲学的な客観の意味の説明が始まります。 我々に、どんな熱弁をふるってくれるのでしょう。 わくわく、わくわくw
このスレ、数学の素人ばかりだなw
804 :
132人目の素数さん :2005/10/03(月) 20:58:55
次スレは哲版に立てろ!ゴルァ
>>800 >全て算数で書ける
なんのこと?これじゃ良く意味が分からないんだが?
ブール・エルだっけ?
807 :
132人目の素数さん :2005/10/05(水) 14:16:20
どうしたのかなぁ、鉄柱… ショボン
808 :
132人目の素数さん :2005/10/05(水) 14:16:57
遊ぼうよ
809 :
132人目の素数さん :2005/10/05(水) 14:28:54
お前ら鉄中スキなのか。
810 :
132人目の素数さん :2005/10/05(水) 14:53:28
鉄中狩り
>ブール・エルだっけ? プール・エルだ。
812 :
132人目の素数さん :2005/10/05(水) 15:58:14
鉄柱さんは躁鬱病質なんで、躁状態のときしか活動できないのれす
814 :
132人目の素数さん :2005/10/05(水) 17:27:36
>>812 >アスペクトというのは,別のアスペクトが
>ありうる場合にのみあるものなのである.
客観という言葉をどう捉えるているか?
私はこう捉えているということは、別の
捉え方もあることを知っているからだ。
815 :
132人目の素数さん :2005/10/05(水) 17:31:06
1は数ではない
816 :
132人目の素数さん :2005/10/05(水) 17:33:18
夫馬って、何?
817 :
132人目の素数さん :2005/10/05(水) 17:36:15
夫馬って、何て読むの?
「ピューマ」です。かっこいいでしょう
819 :
132人目の素数さん :2005/10/05(水) 18:08:38
ほう 意味は ピューマにたべられた馬ですか
820 :
132人目の素数さん :2005/10/05(水) 18:18:20
358 :今年のAAを振り返る :04/12/29 09:28:40 ↓無職の引き篭もりのキモヲタの精神障害者フマ 〜∞ /⌒⌒ ̄ ̄ ̄\ 〜∞ / \ 〜〜〜〜〜 | ____丿ノノ.__| つ〜ん | /U ._) ._) プゥ〜ん | | ( 〜〜〜 | ノ(6 ∵ ( 。。) ) _______ U ) 3 .ノ / ________ / \ ヽ ,,_ U ___,,ノ / / \,,______,ノ \/ / _____ ./ / /| .. ./ / ./ .| 「殺人的ブスいないかなぁ?僕ちゃんブス大好き☆」
800ってプール・エルのことで良いんかいな
822 :
132人目の素数さん :2005/10/06(木) 11:51:30
>>814 >「コンピューターは規則に従い損ねない」と言ったが,
>これは,コンピュータに「アスペクト」がないからである.
つまり、ここの自称素人のいう客観は
実は「アスペクト盲」の状態なのであり
「アスペクト」の違いが問題となる場合
には何の意味も持たない。
823 :
132人目の素数さん :2005/10/06(木) 16:22:40
> 実は「アスペクト盲」の状態なのであり まさに、それは「コンピュータ」って。 てな訳で「形式証明=客観」なんだよw 「アスペクト」の違いを問題にしない。
824 :
132人目の素数さん :2005/10/06(木) 16:23:26
825 :
132人目の素数さん :2005/10/06(木) 16:26:16
あえて「アスペクト盲」たる事を客観という。 君も、あえて「アスペクト盲」である「コン ピュータ」を使ったりするよね?
826 :
132人目の素数さん :2005/10/06(木) 16:29:21
アスペクト盲>非アスペクト盲 非アスペクト盲>アスペクト盲 どちらかの不等式が常に成り立つ訳ではないんだよ 時と場合によって、適切さは変わるのさ ところで「客観がない」というときの客観の説明を 早くしてくれないかな?w
827 :
132人目の素数さん :2005/10/06(木) 16:43:20
哲学厨の文章って、どう見ても電波にしか読めん。 数学ではまともに話ができるkingの貴重さがよくわかる。
828 :
132人目の素数さん :2005/10/06(木) 16:45:05
>>827 つまり、 King>>>>>>夫馬 って訳だw
829 :
GiantLeaves ◆6fN.Sojv5w :2005/10/06(木) 16:45:14
talk:
>>827 私は仮にも日本語暦2・年だぞ。
830 :
GiantLeaves ◆6fN.Sojv5w :2005/10/06(木) 16:45:46
いけね、間違えた。「日本語歴」ね。
831 :
132人目の素数さん :2005/10/06(木) 16:46:42
Kingよ。夫馬と遊んでやれ
832 :
132人目の素数さん :2005/10/06(木) 16:47:29
鉄柱の相手はキングに任せよう。
833 :
GiantLeaves ◆6fN.Sojv5w :2005/10/06(木) 16:54:01
囲碁にも「鉄柱」がある。
834 :
132人目の素数さん :2005/10/06(木) 16:57:09
835 :
132人目の素数さん :2005/10/06(木) 17:16:27
>>823 >> 実は「アスペクト盲」の状態なのであり
>まさに、それは「コンピュータ」って。
>てな訳で「形式証明=客観」なんだよw
>>825 >あえて「アスペクト盲」たる事を客観という。
「ボク、コンピュータ」の幼稚な発想に逃げ込んだか(w
> 君も、あえて「アスペクト盲」である
>「コンピュータ」を使ったりするよね?
しかし、君のように自分を機械だとおもう
馬鹿な真似はしないが(w
836 :
132人目の素数さん :2005/10/06(木) 17:21:53
>>826 >アスペクト盲>非アスペクト盲
>非アスペクト盲>アスペクト盲
>どちらかの不等式が常に成り立つ訳ではないんだよ
>時と場合によって、適切さは変わるのさ
時と場合を全く明らかにできない君の言明は
まったく不適切なものだね。
>「客観がない」というときの客観の説明を
>早くしてくれないかな?w
肝心なことを忘れているな。
「コンピュータには「アスペクト」がない」
という言明の証明は?
837 :
132人目の素数さん :2005/10/06(木) 18:45:32
king 種女と闘え
839 :
132人目の素数さん :2005/10/06(木) 19:15:06
コンピュータは規則通りに動く、と想定されています かつ、そうであることを期待されています 早く客観の意味とその非存在を説明してくれよ(w
840 :
132人目の素数さん :2005/10/06(木) 19:17:41
キングよ。電波の鉄柱どもに お前の力を見せ付けてやれ!
想定されています かつ、そうであることを期待されています 想定と期待の違いは?
842 :
132人目の素数さん :2005/10/06(木) 19:56:56
「客観がない」って言ってる奴って、「厳密性」に随分と拘るんだな。
843 :
132人目の素数さん :2005/10/06(木) 19:57:45
844 :
132人目の素数さん :2005/10/06(木) 19:59:46
845 :
132人目の素数さん :2005/10/06(木) 20:28:19
King>>>>>>鉄柱
846 :
132人目の素数さん :2005/10/06(木) 20:28:56
鉄柱どもは、 KING以下!
847 :
132人目の素数さん :2005/10/06(木) 20:47:47
kingなら鉄柱に勝てる
848 :
132人目の素数さん :2005/10/06(木) 21:03:59
鉄柱、ガンガレ! Kingなんかに負けるな!
849 :
132人目の素数さん :2005/10/07(金) 08:45:50
数学は死ね!
850 :
GiantLeaves ◆6fN.Sojv5w :2005/10/07(金) 08:55:03
851 :
132人目の素数さん :2005/10/07(金) 08:57:31
>>839 >コンピュータは規則通りに動く、と想定されています
>かつ、そうであることを期待されています
それは主観だね。
期待や想定ぬきの証明を早く!早く!!早く!!!
できるといったじゃないか!!!君。
>>840 鉄柱がデムパなら、Kingはさしずめスカラー波(w
>「客観がない」って言ってる奴って、 >「厳密性」に随分と拘るんだな。 素人って二重基準なんだな(w
855 :
132人目の素数さん :2005/10/07(金) 09:14:07
感覚の違いだろ?
856 :
132人目の素数さん :2005/10/07(金) 09:17:16
君の間違い.「主観が出てきた ⇒ 客観がない」 君の脳内等式1.「あ、うん」=「あ、うんと思う」 君の脳内等式2.「コンピュータ」=「コンピュータに対する期待」
857 :
132人目の素数さん :2005/10/07(金) 09:17:51
厳密性に拘るのは哲学さん、君だろ?
858 :
132人目の素数さん :2005/10/07(金) 09:20:21
君の間違い.「証明図」=「証明」 別物なんですけど…
>君の脳内等式1.「あ、うん」=「あ、うんと思う」 なるほど、君は 命題P⇔命題Pが真 には反例があるというんだね? どんな反例だい?いってごらん?ん?どうした?(w
860 :
132人目の素数さん :2005/10/07(金) 09:21:43
君の間違い.「客観」=「客観に対する期待」
>君の脳内等式2.「コンピュータ」=「コンピュータに対する期待」
これは839の脳内の等式だろ(w
>>860 も同様。
862 :
132人目の素数さん :2005/10/07(金) 09:24:05
君の間違い.「あ、うんが真」=「あ、うんが真と思う」 「あ、うんが真」=「あ、うんと思う」 「あ、うんが真」=「あ、うん」
>君の間違い.「証明図」=「証明」 どんどんぶっ壊れるねえ。君(w じゃあ、聞くけど 「証明図で示せない証明」 って何なの?
>>862 君の間違い
「あ、うんが真」=「あ、うんが証明できる」
865 :
132人目の素数さん :2005/10/07(金) 09:26:43
じゃ、コンピュータに対する期待が主観だからといって、 それとコンピュータ自体は別だな。 お前はバカだから、しょうがないよ
866 :
132人目の素数さん :2005/10/07(金) 09:28:48
>>863 駄目だ。お前
何にも分かってない。一から出直せ
>>865 >じゃ、コンピュータに対する期待が主観だからといって、
>それとコンピュータ自体は別だな。
そもそも「コンピュータ自体が存在する」という考えが主観だな。
どこまでいっても、主観抜きの客観はない。
バカの君は考えないからこのことに気づかない。
868 :
132人目の素数さん :2005/10/07(金) 09:29:50
「証明図」=「証明」 だと思っていたんだ。へー、www
869 :
132人目の素数さん :2005/10/07(金) 09:30:40
また出てきたねw 脳内等式.「主観抜きの客観がない」=「客観がない」
>>866 そうか、ダメか君。
何も分かってない。ゼロから出直せ。
いいか、イチじゃないゼロだぞ。
イチがあると思ったから失敗したんだ。
ゼロからイチへのもっとも困難な壁を乗り越えろ
871 :
132人目の素数さん :2005/10/07(金) 09:31:45
いい加減、下らない脳内等式で議論しても 無駄だよ。おバカさんw
872 :
132人目の素数さん :2005/10/07(金) 09:32:38
「証明図」と「証明」って、違うものなんだよ
>>869 引っかかったぜ!このバカが!
>>859 を見ろ
>君の脳内等式1.「あ、うん」=「あ、うんと思う」
今お前は
「客観」=「オレが客観だと思う」
という等式をつかったんだぞ!(w
お前はお前自身を否定するのか?(w
874 :
132人目の素数さん :2005/10/07(金) 09:35:12
>>873 頭の悪い君の脳内等式.「主観抜きの客観がない」=「客観がない」
> 「証明図」と「証明」って、違うものなんだよ でもどう違うか言えない。 なぜ言えないか?言ったら 「実は証明って主観なんだぜ」 と認めることになるから。 それは自分の首をかき切るから言えない。 図星だろ?(w
876 :
132人目の素数さん :2005/10/07(金) 09:36:23
君の間違い.「主観抜きの客観がない ⇒ 客観がない」
877 :
132人目の素数さん :2005/10/07(金) 09:37:31
>>875 「実は証明って主観なんだぜ」
え、そうだけど。これって、当たり前のことなんだけど
878 :
132人目の素数さん :2005/10/07(金) 09:38:07
「証明」(主観)、 「証明図」(客観)
>>874 バカな君の脳内等式
「客観」=
「オレが客観だと思ってるが、
「オレが」とは思ってない」
880 :
132人目の素数さん :2005/10/07(金) 09:38:48
「実は証明って主観なんだぜ」 認めるも何も、当たり前のことなんだが…
>>877 おやおや、都合が悪くなると寝返るんですね。
これから君を小早川クンと呼びましょう(w
882 :
132人目の素数さん :2005/10/07(金) 09:40:15
>>880 「実は」は不自然だな。
『当たり前だが、証明は主観』
>「証明」(主観)、 >「証明図」(客観) ただの図とアスペクトが分離できると思うくらいバカな発想だ。
884 :
132人目の素数さん :2005/10/07(金) 09:42:50
>>881 は?お前は勘違い。どうせ、数学のことを分かってない連中(底辺高校の
数学教師とか)が「証明は客観」とか言うの聞いて、数学者もそう思って
いるとか勘違いした訳だw
885 :
132人目の素数さん :2005/10/07(金) 09:45:12
だから、証明図と証明は別物なんだよ。矛盾した形式体系で 証明図があっても証明とは認めないよw
886 :
132人目の素数さん :2005/10/07(金) 09:46:21
勘違いし過ぎ。議論の前提が勘違いだから、どうにもならないよ
887 :
132人目の素数さん :2005/10/07(金) 09:49:37
頭の悪い君の脳内等式.「主観抜きの客観がない」=「客観がない」
888 :
132人目の素数さん :2005/10/07(金) 09:50:17
早く客観の意味とその非存在を説明してくれよ(w
889 :
132人目の素数さん :2005/10/07(金) 10:02:31
数学者の世界で重要なのは、価値観(主観)。 当たり前過ぎて、改めて言うのも恥ずかしい。
890 :
132人目の素数さん :2005/10/07(金) 10:03:24
数学者の世界は、主観の戦場
891 :
132人目の素数さん :2005/10/07(金) 10:55:04
完全証明というのがいまだによくわからないんだが、これ以前は 「平面を曲線の内と外に分けない閉曲線」 が発見される可能性はあったの?
892 :
132人目の素数さん :2005/10/07(金) 11:44:56
>>891 これがわかるかわからないかで、数学できるかできないかが区別できるな。
毎日数学の問題解いてるやつなら、この意味はすぐにわかる。
893 :
132人目の素数さん :2005/10/07(金) 14:16:51
>>892 で、その意味は?
あ、よく読めば、お前が「できる」側だとは一言も言ってないな、スマソ。
894 :
132人目の素数さん :2005/10/07(金) 14:43:58
客観テストの意味は? 答え:採点の仕方が規則的(=客観的)という意味。 その結果による順位の評価(=価値観)が客観的と いう意味ではありません。当たり前だがな ところで、哲学的な客観の意味とその非存在を早く 説明してくれないかなあw
895 :
132人目の素数さん :2005/10/07(金) 14:45:21
>>894 「機械的」の方がイイ感じだな
答え:採点の仕方が機械的(=客観的)という意味。
その結果による順位の評価(=価値観)が客観的と
いう意味ではありません。当たり前だがな
896 :
132人目の素数さん :2005/10/07(金) 14:46:30
わーい、わーい、鉄柱だ! チュキ、チュキ、鉄〜柱♪
897 :
132人目の素数さん :2005/10/07(金) 14:53:31
機械的な採点方法(客観テスト)は、大量の受験生を 効率的に捌くには便利だ
898 :
132人目の素数さん :2005/10/07(金) 14:54:26
鉄柱にチュー♪チュキ、チュキ
899 :
132人目の素数さん :2005/10/07(金) 15:19:50
>>893 鉄柱の典型的特長
「意味」を尋ねたがる。
自分で証明問題を練習してみれば、すぐに気づくことなのに、努力はしない。
いいか、数学は、意味でわかるようになるものじゃない。
数学は知識や情報じゃない。
情報を扱う能力なのさ。アビリティ!アビリティ!
努力なしで理解することはできず、自ら証明問題を解くこともせず語ることもできん。
鉄柱、だらけた夢みてんなよ。
900 :
132人目の素数さん :2005/10/07(金) 15:56:24
主観と客観をどう区別するかも主観的にならざるを得ないわけだし、 じゃあ主観てなんなの?という問いへの答えも主観的にならざるを得ない。 つまりこの世はオール主観! 問題は「Aさんの主観」と「Bさんの主観」が同値がどうかってことでしょう。 え、同値かどうかも主観で決まるって?そりゃないよ‥‥
901 :
132人目の素数さん :2005/10/07(金) 15:57:50
鉄柱は厳密性に拘りますwww
902 :
132人目の素数さん :2005/10/07(金) 16:00:51
>>900 相変わらず、頭悪いな
主観的に「主観と客観」を区別する。主観的に「主観と客観」がある。
このことと「客観がある」ことが。何で矛盾するんだ?訳分からんw
903 :
132人目の素数さん :2005/10/07(金) 16:02:32
「客観テスト」と「客観テストでないテスト」の区別は主観的。 そうしたら、「客観テスト」がなくなるのかよ?頭、わり〜w
904 :
132人目の素数さん :2005/10/07(金) 16:03:14
主観/客観バトルに一石を投じますよ。 すべての人間にとって遠くのものは小さく見えますよね。 では自分から遠ざかるほど物体は小さくなるか?っていうとそうでもない。 しかし主観オンリーなら上記は成り立つわけです。。。
905 :
132人目の素数さん :2005/10/07(金) 16:03:55
「客観テスト」と「客観テストでないテスト」の区別は主観的にしても、 「客観テスト」はなくなりませんよw
906 :
132人目の素数さん :2005/10/07(金) 16:06:44
>>904 うだな
鉄柱の基地外等式.「小さい」=「小さく見える」
結局、こればっかw
907 :
132人目の素数さん :2005/10/07(金) 16:07:02
哲学を語るくせに、ヴィトゲンシュタインの主観と数学についての研究すら知らないのか。 やはり、哲厨。 オタの悲しさか。
908 :
132人目の素数さん :2005/10/07(金) 16:08:53
主目は統合失調症のようだ。
909 :
132人目の素数さん :2005/10/07(金) 16:09:55
ところで、哲学的な客観の意味とその非存在を早く 説明してくれないかなあw
910 :
132人目の素数さん :2005/10/07(金) 16:13:07
数学はせいぜい人工言語、間主観、合意の体系・・・って所でいいじゃないですか。 何を揉めているのかわからん。
911 :
132人目の素数さん :2005/10/07(金) 16:19:32
バカな哲学ヲタは、証明と証明図くらいは区別しろよ。 バカな鉄ヲタの脳内等式.「証明」=「証明図」 鉄ヲタの推論 → 「証明」は主観。だから「証明図」も主観www
912 :
132人目の素数さん :2005/10/07(金) 16:20:59
機械的な採点方法(客観テスト)は、大量の受験生を 効率的に捌くには便利だ
どうも「客観」という言葉がきわめておおざっぱに使われているようだな。
914 :
132人目の素数さん :2005/10/07(金) 16:25:52
915 :
132人目の素数さん :2005/10/07(金) 16:28:39
大体、厳密であれば厳密であるほどよい、とか客観的であれば客観的であるほどよい、
ってのは誰の価値観なんだ。
>>25 でも一度書いたが、「厳密さは時代の関数」と言った
偉い数学者がいたと思ったよ。
916 :
132人目の素数さん :2005/10/07(金) 16:46:13
>>915 客観テストは受験生を効率的に捌くのに便利です! by 大手私大w
917 :
132人目の素数さん :2005/10/07(金) 16:47:34
> 客観的であれば客観的であるほどよい、 > ってのは誰の価値観なんだ 答え:大手私大
918 :
132人目の素数さん :2005/10/07(金) 16:48:56
919 :
132人目の素数さん :2005/10/07(金) 16:48:56
>>916 そりゃせいぜい創造性をまったく評価されないような人間を
おおざっぱに扱うのに効率がよいという程度の二次的な価値じゃないか。
大手私大だって創造性の高い生徒を育てることができるという評判が立てば
評価が上がるとおもわれるよ。
920 :
132人目の素数さん :2005/10/07(金) 16:51:47
>>919 財務上、効率性は非常に高い価値があります by 大手私大&マクド
921 :
132人目の素数さん :2005/10/07(金) 16:54:15
>>920 そりゃそうだが、同時にイノベーションを続け、陳腐化しないような
付加価値を付け加え続けなければ競争には勝てないのであって。
922 :
132人目の素数さん :2005/10/07(金) 16:56:14
>>921 だから、人材を区切って使い分けています。
923 :
132人目の素数さん :2005/10/07(金) 16:57:42
924 :
132人目の素数さん :2005/10/07(金) 16:58:58
>>920 私大は受験料収入&入学金(すべり止め確保用)が
重要な収入源だからねw
925 :
132人目の素数さん :2005/10/07(金) 17:00:43
客観性は数学にあまり関係がありませんが、 私大経営や受験産業とは大いに関係します。
じゃあ、この(「客観性」の)話題は受験板の話題だね。
927 :
132人目の素数さん :2005/10/07(金) 17:04:07
>>925 鉄柱の勘違い.数学=客観=敵
正しくは、「私大経営&受験産業=客観=敵」
客観性を攻撃するなら学歴版の方が相応しいぞ
928 :
132人目の素数さん :2005/10/07(金) 17:04:55
929 :
132人目の素数さん :2005/10/07(金) 22:18:14
プルーフ・チェッカーが実用化されると 大学入試で証明問題が客観テストになり まつ
930 :
132人目の素数さん :2005/10/07(金) 22:18:56
932 :
132人目の素数さん :2005/10/08(土) 01:17:54
933 :
132人目の素数さん :2005/10/08(土) 06:11:21
プルーフチェッカーと客観性は何の関係もない。 自分で証明問題を解けばすぐわかること。
934 :
132人目の素数さん :2005/10/08(土) 07:18:01
客観的=採点方法が機械的!
935 :
132人目の素数さん :2005/10/09(日) 15:56:35
平面内で連続で自己と交わらない閉曲線。 ここで、連続というだけであるからとても難しい。 長さが定義できないような連続曲線だとか、任意の点のどれだけでも 近いそばを通る曲線だとか、とても絵に書けないようなものでも、 それが連続曲線に含まれている以上は扱われていなければならない。
936 :
132人目の素数さん :2005/10/09(日) 19:09:30
(1)数学は数学者(屋)の考える意味で厳密である (2)数学は約一名の哲厨の考える意味では厳密でない 約一名の哲厨も含めて、このスレの大半の人は(1)も(2)も認めてる。 そして、「このスレの大半の人は(1)も(2)も認めてる」という事を 1. このスレの大半の人は認めていて、 2. 約一名の哲厨は認めていない、 という構図。 脳内に仮想敵を作って 「君らは俺の考える意味で数学が厳密じゃない事を理解できないバカ(w」 とか言って仮想敵を煽られても、妄想乙としか言いようがないな。
937 :
132人目の素数さん :2005/10/09(日) 22:03:59
鉄柱はまず紙と鉛筆を用意しろ。 そして、√4が有理数である証明を書け。 中学生でもできる。 次に、√2が有理数ではない証明をしてみろ。 その仮定で、証明とは何か、数学的帰納法がなぜ必要か、そして完全証明とは何なのかがわかる。 自分で頭を動かさずに、想いだけ飛ばしてるのが鉄柱。 だからオナニーなんだよ。カスが。
938 :
132人目の素数さん :2005/10/09(日) 23:48:36
>>935 豆知識: 任意の a<1 に対して, [0,1]×[0,1]内のジョルダン閉曲線で,
そのルベーグ測度が a 以上なものが存在する.
>>936 非常に分かりやすい解説をありがとう. おまいアタマいいな.
940 :
132人目の素数さん :
2005/10/10(月) 10:10:39 自分で腰を動かさずに、精子だけ飛ばしてるのが鉄柱。 だからオナニーなんだよ。カスが