無限に付いて語る。実無限VS可能無限

形式的言語を上手く設計して，その体系の中で理論を表現すれば，
ゲーデルの方法によって，それを自然数の中にコード化できる。
このとき，ある原始帰納的述語Ｆを，
F(P,T)が真⇔Ｔが命題のゲーデル数でＰがその証明のゲーデル数
となるように作ることができる。これがメタ数学の証明論の立場。
対角線論法によって，自分自身の証明不能性をあらわす命題を
構成すれば，不完全性定理が導ける。
もし形式的言語の「意味」をすてて記号列の操作とのみとらえれば
すべての定理はこのもとで，自然数に関する命題に還元される。

しかしこれは，実際には，数学的理論が完成し，さらにある定理
の証明がみつかってから後にそうできるということで，
理論それ自体をどう作り，ある定理がなりたちそうであると見通したり
様々な知識や直感に導かれてその証明をみつけるという
実際の営みはそれ以前になされていなければならない。
ＺＦの元での，選択公理と連続体仮説の無矛盾性と独立性が
証明されたあとも，ゲーデル自身は実在論者で，
連続体問題に決着がつけられるための，集合論の新しい公理
を生涯にわたって求め続けたのは有名な話だ。