Inter-universal geometryとABC予想(シン応援スレ) 92 (607ﾚｽ)
上下前次1-新
抽出解除 ﾚｽ栞
532(5): 07/26(日)15:34 ID:jgtmOrU+(5/12) AAS
>>531
>証明論に限らず数学の形式化が進んでるから
>昔みたいなことはもう起きないよ
たぶん 違うんじゃ無いかな
１）まず、下記の 渕野先生が書いている
”厳密性を数学と取りちがえるという勘違い”
２）さらには、形式化の限界
これは、下記ゲーデル不完全性定理の話（下記）
”証明できない真実: 第一不完全性定理により、内容としては正しい（真である）にもかかわらず、その体系の中のルール（公理）だけでは「正しい」と証明できない命題が必ず存在することが示されました”
要するに、数学とは IUTのLean形式化の失敗をのり超えて 進んでいくものだと思う
省31
534(3): 07/26(日)16:03 ID:jgtmOrU+(6/12) AAS
>>532 補足
(引用開始)
>証明論に限らず数学の形式化が進んでるから
>昔みたいなことはもう起きないよ
たぶん 違うんじゃ無いかな
(引用終り)
意味が分らないだろうから、ABC予想の歴史を振りかえろう
１）昔々 フェルマーさんが、フェルマー予想を出した。証明を得たが、余白が狭いという名言を書いた
外部ﾘﾝｸ:ja.wikipedia.org
２）みんな挑戦したけど、最終解決にならない状態で 数百年
省24
535(1): 07/26(日)16:52 ID:q7nx5Qo2(3/11) AAS
>>532
>１）まず、下記の 渕野先生が書いている
>”厳密性を数学と取りちがえるという勘違い”
数学は厳密でなくてもよいと勘違いしてるのがおまえ。
>２）さらには、形式化の限界
> これは、下記ゲーデル不完全性定理の話（下記）
> ”証明できない真実: 第一不完全性定理により、内容としては正しい（真である）にもかかわらず、その体系の中のルール（公理）だけでは「正しい」と証明できない命題が必ず存在することが示されました”
それは数学そのものの限界であって形式化の限界ではない。
数学で論ずる対象は「何を仮定すると何が結論できるか」つまり相対的真理であって絶対的真理ではない。形式化はそのことを明らかにした。
>要するに、数学とは IUTのLean形式化の失敗をのり超えて 進んでいくものだと思う
省2
540: 07/26(日)19:15 ID:3b2MGiGr(3/6) AAS
>>532
＞”証明できない真実: 第一不完全性定理により、
＞内容としては正しい（真である）にもかかわらず、
＞その体系の中のルール（公理）だけでは
＞「正しい」と証明できない命題
＞が必ず存在することが示されました”
誤り
「内容としては正しい（真である）にもかかわらず、」が嘘
「内容として、正しい（真である）としたら」が正しい
「正しいとしたら、正しいことが証明できない命題」が正解
省2
549(2): 07/26(日)21:43 ID:q7nx5Qo2(7/11) AAS
>>532
＞”証明できない真実: 第一不完全性定理により、
＞内容としては正しい（真である）にもかかわらず、
＞その体系の中のルール（公理）だけでは
＞「正しい」と証明できない命題
＞が必ず存在することが示されました”
完全性定理の反例があると言ってる？
554: 07/26(日)22:40 ID:q7nx5Qo2(9/11) AAS
>>549
もちろん反例なんて無いから、間違ってるのは>>532。
PAで考える。ゲーデル文「ゲーデル文は証明できない」をGと書く。
不完全性定理から¬Gは証明できない。・・・(1)
(1)と完全性定理から¬Gが偽となるモデルが存在する。・・・(2)
仮に標準モデルで¬Gが真とすると任意のモデルでも真であるはずだから(2)と矛盾。背理法により標準モデルで¬Gは偽、すなわちGは真。
真なのは標準モデルでであって、任意のモデルでではない。それが>>532の間違い。
上下前次1-新書関写板覧索設栞歴
ｽﾚ情報 赤ﾚｽ抽出 画像ﾚｽ抽出 歴の未読ｽﾚ AAｻﾑﾈｲﾙ
ぬこの手 ぬこTOP 0.845s*