■

久しぶりに行った神保町で、前原昭二著「数学基礎論入門」なる本を1000円で買ってきた。
不完全性定理の証明にゲーデルの論文をほぼそのまま使っているのがこの本のポイント。
今までまじめに不完全性定理の証明なんて読んだことなかったので、まじめに読んでみるが難しい…

まず、自然数を含む公理系と推論規則を作る(形式的な自然数＋論理式)。
普通の数学の自然数（たとえばプリンピキアマテマチカ＋ペアノ）みたいな体系(内容的な自然数)に関する命題が形式的な論理式で表現できるかどうかが難しいところ。

という式の読み方で非常に苦労した。
細いほうの文字と右矢印は内容的な体系の自然数と「左ならば右」をあらわしていて、太いほうの文字と├は形式的な体系での「細いほうの同じ文字」に対応する形式的な自然数と「証明できる」をあらわしている。
ということなので、この式は「内容的な自然数m, n が等しければ、「対応する形式的な自然数m, n が等しいことが証明できる。」」と読む。

この証明が簡単だからと省略されてたおかげで、かなり困った。これだけでも丁寧に解説してくれてれば楽だったんだけど…

これをどう証明するかというと、m, n が等しいとして「対応するm, n が等しいことが形式的に証明できる」ことを証明すればよいわけだ。

というわけで、対応するm, nを実際に書き下してみると
(succ は m 個並べる)
(succ は n 個並べる)
となるわけだが、m と n は等しいので、succ は同じ数だけ並んでいる。よって、上の対象式はどちらも同じ形をしているので、定理

により証明終わり。

ここで重要なのは、内容的な自然数mとnを決めるごとに異なる形式的な論理式を証明しないといけないということだ。

でも、異なっているのは自然数を形式的な論理式で置き換える部分だけで、二項関係Eq(x,y)だけを見ると、内容的と形式的で同じ形をしている。よって、問題はどういう関係が形式的な体系でも同じ形で表現できるかってことになる。

表現可能であるための条件を再帰的に適用していけば、表現可能な関係はたくさん構成できるのだが、不可能なものを構成するのは容易ではない。例えば内容的な一項関係R(x)が形式的な関係FR(x)で表現できても、内容的な∀x R(x)の表現が∀x FR(x)であるとは限らないということがある。

うまくFR(x)を作ってやると、形式的には

がすべて証明できても

は証明できないということを内容的に証明できる。証明できないことをどうやって証明するのかというと、
がすべて真であることと

が証明できないことが同値になるように作ったかららしい…