有限wwプギャーm9(^Д^)

「お前ら公理系作って再帰的に無限の定理を手に入れたと思ってるみたいだけど所詮は有限の脳味噌には有限のことしか扱えませんからプギャーm9 (^Д^)」
ということですね。分かります。

メタマス!―オメガをめぐる数学の冒険

• １：公理系をプログラムに焼直し、推論規則を使って枝分かれを順番に網羅して全ての定理を順番に吐き出すプログラムを作れる。「真理鉱山」自動探索 (グレッグ・イーガン『ディアスポラ』ISBN:4150115311)
• ２：その定理自動生成プログラムがNビットで書けるとする。そしてたとえばその１００倍の長さの100Nビットのデータすべての集合を考える。そのなかで公理系が何かを言えるデータは割合として０に近い。ほとんどのデータは圧縮をかけてもサイズがへらない=100Nより短いビットのプログラムではそのデータを生成できない=定理生成マシンも例外ではない
• ３：だから無限に長いビットで表される実数の集合なんて、どんな数学作っても扱えない。

プログラムに関する公理系ってこんなんかな。

• ＊＊はプログラムである。
• ＊＊がプログラムの時、＊△＊はプログラムである。などなど。これで可能なプログラムを全て列挙。
• プログラム＊＊の初期状態は■■である。
• 状態は■■のプログラムは次に状態□□になる。

こういう感じでチューリングマシンみたいなのを考えればいいのかな。停止という状態も定義しておけば、これで「プログラム＊＊は○ステップ後に停止する」といった定理も出てくる。定理を全て吐き出すプログラムは、あらゆるプログラムを長さ順に並べて、i番めのプログラムのjステップ目を計算したら次にi+1番めのプログラムのj-1ステップ目を計算する、というように i,j の表を、有理数が可算であることを示す場合みたいに斜めに埋めていく。