https://www.jstage.jst.go.jp/article/sugaku1947/57/2/57_2_113/_article/-char/ja/ を見ると, その魔境具合を体感できます.
ゲンツェンやばい. そして折角なので後者のを軽く眺めてみた.
事実, 後に Hilbert の 第 10 問 題 (Di0phantus 方程式の可解性の決定) の Matijasevic-Robinson-Davis-Putnam による否定的解決により, CON (T) は Diophantus 方程式が自然数解を持たない $\forall \vec{x} \in \mathbb{N} \left[ p (\vec{x}) \neq 0 \right]$ という命題と同値である.
P.2 の記述なのだが, Diophantus, そんなにやばい問題だとは知らなかったので, まずそこで驚いた.
同じく P.2 の無限降下法, 名前が格好いいので一度は使いたいと思いつつ使ったことがない学生生活だった.
ひとは詩しく思うかもしれない:ここで言う構成的とはいかなる謂か? 数学的に正確に定義されているか? 例えばある公理系 T で形式化できることが構成的てあるための必要十分条件となるような T があるのか? これに答えて曰く:Hi1bert'spr0gram のような grandprogram において, その開始以前にこのようなことを問うことは単なる怯儒というべきである. 何が構成的か, あるいは得られた証明が構成的か否かは, 証明が得られてから吟味すればよいし, その価値は得られた洞察から判断するほうが生産的である.
それはそうなのだろうが, (基礎論の) 素人の素朴な感覚としては, やはり真っ先に考える.
P.3 の次の記述がよく分からなかった. 明らかなのか.
この簡易化のステップが終了して $0=1$ の数学的帰納法なしの証明が得られたら, 矛盾. なぜなら数学的帰納法なしの矛盾に至る証明があり得ないことは明らかだから.
あと, 次の一文, かなり切れていると思う.
このステップの有限性を保証するのに超限順序数を導入する.
有限性を保証するのに超限何とかを担ぎ出すとか並大抵の発想ではない. もちろん, 言葉の上で有限の対として無限があるのだから当たり前といえば当たり前ではあるが, 改めて言われると衝撃を受ける.
P.6
直感を欠いたままで組合せ論的につくられたものが, 後に発見された集合論的直観を先取りしていたのは驚きである.
何かびびっと来るものを感じたので抜き出しておく.
P.7
ところで, このような集合の定義の仕方は, 数学では Borel 集合族 $\mathscr{B}$ の定義が典型的である.
戦慄した. あと. この辺からもう何を言っているのかほぼ完全に分からなくなっている.
P.9
竹内外史の (brutal な) テーゼに従おう
これ, 無駄に格好いい一文だ
P.12
6 結 語 しかしなにより謎なのは, 何故 Gentzen (そして竹内外史) は, 不完全性定理の後に無矛盾性証明に挑んだのか, ということだ. 不完全性定理のために, そのような証明がいかなるものであれ, その認識論的価値は大幅に減じたことが確かなのに.
胸に来る一文だ.
結論からいうと, 新井敏康先生は面白い文章を書く人だったということが分かった.
数学, 数学基礎論, 証明論, 順序数
Previous: Turing 次数理論の Martin 予想をめぐる対話 Next: チャーハニスト鈴木と tri_iro さんによるランダムネス対話の記録 back to top