不完全性定理(3) - エレファント・ビジュアライザー調査記録

『不完全性定理とはなにか (ブルーバックス)』の不完全性定理の証明をプログラミング言語を使って書き直していきます。しかし、すべてプログラミング言語のようにはできないので、まずはデータをプログラミング言語の式のように表すことを考えます。

不完全性定理の証明

この本の流れに沿って書き直していきます。

【ステップ1】すべての命題 $f(i, v)$ の一覧表を作る。

この本では「1変数の命題 $F(y)$ を網羅した一覧表を作る」だったのですが変更します。

命題や証明は(プログラミング言語の式のように構造を持った)「式」として表します。命題の式を論理式、証明の式を証明式と呼ぶことにします。無限個使うことができる変数名、数値はプログラミング言語のリストのように表します。構造の上位の要素が演算子のとき、その直下の要素は、有限個の決まった個数のその演算子の被演算子とします。構造の上位の要素が変数名を表す記号のとき、その直下の要素は、変数名の次の文字とします。変数名に使える文字は有限個とします。構造の上位の要素が数値を表す記号のとき、その直下の要素は、数値の次の文字とします。数値に使える文字は有限個とします。

式のある部分を考えると、その部分の最上位の要素の種類は有限個となります。その直下の要素は最大で演算子の被演算子の最大の個数となります。よって、式の「深さ」が有限とすると、式の個数は有限となります。

この式を長方形の表の形で表します。表の右方向には式の下位の要素、下の方向には被演算子を順に記入していくとします。演算子の被演算子が複数あるときは、2個目の被演算子以降は上位の要素は空白として表を作ることができます。下位の要素がないときも空白とします。これはプログラミング言語の式を表の形で表すような方法です。この表全体を文字列と考えて、その順序によって式に順序を導入することができます。たとえば、表の横方向の並びを1つの文字列と考え、それを縦方向にすべて連結した文字列を考えます(「次元」に関する辞書式順序の並び)。その文字列に辞書式順序を導入します。これによって式の「深さ」が決まった有限の値である式の全体は、有限全順序集合となります。これを式の「深さ」が小さいものから順に並べると、すべての式に番号をつけることができます。

逆に番号を指定すると、構造を再現することができます。

論理式、証明式と番号の対応を表すため、プログラミング言語の関数定義のような記法を導入します。プログラミング言語でできることだけをやっていって、全体をプログラミング言語で記述できるようにします。これを説明するため、プログラミング言語の関数のような関数を「言語関数」、その引数を「言語関数引数」と呼ぶことにします。

$i$ 番目の論理式を $e(i)$ とします。論理式 $x$ の番号を $e^{-1}(x)$ とします。

$e(i)$ の $e$ は「言語関数」、 $i$ は $e$ の「言語関数引数」です。 $e(i)$ (「言語関数定義」と呼ぶことにします)の $i$ に自然数または論理変数(論理式で使う変数) $s$ を指定した $e(s)$ は、 $e(i)$ に現れる「言語関数引数」 $i$ をすべて $s$ に置き換えたものを表します。論理変数は大文字で表すことにします。

$e^{-1}(x)$ の $e^{-1}$ は「言語関数」、 $x$ は $e^{-1}$ の「言語関数引数」です。

論理式 $x$ に現れるすべての自由変数(式のある部分だけで使われる変数(束縛変数)ではない論理変数) $V$ を論理変数または自然数 $s$ に変更した式を $x[V \mapsto s]$ と表すことにします。

この手順は以下のようになります。論理式の一部が $\forall V (P)$ または $\exists V (P)$ の形になっているとき、その部分のすべての論理変数 $V$ を新しい変数 $W$ に置き換えます。これを式の下位の部分から順に、 $\forall V (P)$ または $\exists V (P)$ の形の式に論理変数 $V$ が現れなくなるまで行います。その後すべての論理変数 $V$ を $s$ に置き換えます。式に現れる変数は有限個で、変数は無限個あるので、プログラミング言語でこの手順を記述することができます。これは公理系から成り立つとします。

$f(i, s) = e(i)[V \mapsto s]$ とおきます。

$k$ 番目の証明式を $g(k)$ とします。証明式 $y$ の番号を $g^{-1}(y)$ とします。 $g(k)$ の $g$ は「言語関数」、 $k$ は $g$ の「言語関数引数」です。 $g^{-1}(y)$ の $g^{-1}$ は「言語関数」、 $y$ は $g^{-1}$ の「言語関数引数」です。

証明式は推論規則の論理式とします。論理式は、証明式で変換することができます。変換した結果は「推論の要素」の論理式となります。結果が真のとき、その証明式はその論理式を真にする証明式と呼ぶことにします。

論理式を真にする証明式が存在するとき、その論理式は真であるとします。

以上のことは公理系から成り立つとします。この本の証明は(詳しく書かれていないのでわかりませんが)ペアノ算術の公理系に基づくと考えられますが、ここではこの公理系に関する不完全性を示します。

この本では番号は(詳しいことはわかりませんが)飛び飛びとなっていますが、ここでは番号はすべての自然数とします。式として成立しないものも含んでも良いとします。

【ステップ2】「 $f(i, s)$ を真にする証明式が存在する」という論理式を $r(i, s)$ とおく。

$p(k, i)$ を「 $k$ 番目の証明式 $g(k)$ は $i$ 番目の論理式 $e(i)$ を真にする証明式である」という論理式とします。

$r(i, s) = \exists k ( p(k, e^{-1}( f(i, s) )))$ とおきます。

$r(i, s) \iff i$ 番目の論理式 $e(i)$ の自由変数 $V$ をすべて論理変数または自然数 $s$ で置き換えた式 $f(i, s)$ を真にする証明式が存在する

$\lnot r(i, s) \iff i$ 番目の論理式 $e(i)$ の自由変数 $V$ をすべて論理変数または自然数 $s$ で置き換えた式 $f(i, s)$ を真にする証明式が存在しない

となります。

【ステップ3】「言語関数定義」 $r(i, s)$ の $i$ と $s$ を論理変数 $V$ に置き換え、否定にした論理式 $\lnot r(V, V)$ がある。これは、ステップ1で作った一覧表のどこかにある。それが $n$ 番目の論理式だったとする。つまり、 $f(n, V) = \lnot r(V, V)$

$r(i, s)$ の「関数引数」 $i$ と $s$ は論理変数に置き換えることができ、置き換えると論理式になるものでした。 $r(i, s)$ の $i$ と $s$ を論理変数 $V$ に置き換えると論理式 $r(V, V)$ になります。この否定の論理式 $\lnot r(V, V)$ の番号を $n$ とおきます。 $n = e^{-1}(\lnot r(V, V))$ です。

【ステップ4】 $f(n, V) = \lnot r(V, V)$ の論理変数 $V$ に(自分自身の番号) $n$ を代入する(「言語関数定義」 $f(i, s)$ の $i$ を $n$ 、 $s$ を $V$ で置き換える)。すなわち、 $f(n, n) = \lnot r(n, n)$

$e(n) = \lnot r(V, V)$ であるから

$f(n, n) = e(n)[V \mapsto n] = (\lnot r(V, V))[V \mapsto n] = \lnot r(n, n)$

が成り立ちます。

【ステップ5】ステップ4で作った論理式 $f(n, n) = \lnot r(n, n)$ の右辺の内容は、(ステップ2を思い出せば)「 $f(n, n)$ を真にする証明式が存在しない」となる。それは、 $f(n, n)$ が証明できない、ということだ。でも、左辺を見れば、それは $f(n, n)$ にほかならない。すなわち、「この論理式は証明できません」という論理式 $f(n, n)$ ができてしまった

$f(n, n)$ が何なのか考えてみます。

自由変数のない論理式は真または偽
論理式を真にする証明式が存在するならばその論理式は真
自由変数のない論理式を真にする証明式が存在しないならばその論理式は証明できない

とします。

$f(n, n)$ は $f(n, s)$ の「関数引数」 $s$ を自然数 $n$ で置き換えたものなので、自由変数のない論理式となっています。 $f(n, n)$ が偽であるとすると、「 $f(n, n)$ を真にする証明式が存在する」ということになります。すると $f(n, n)$ は真ということになって $f(n, n)$ が偽であることに矛盾します。よって $f(n, n)$ は真でなければなりません。 $f(n, n)$ が真ならば「 $f(n, n)$ を真にする証明式が存在しない」ということになって $f(n, n)$ は証明できないということになります。よって $f(n, n)$ は真であり証明できないということになります。

$f(i, s)$ を表にしたときに対角線に現れるものの1つが $f(n, n)$ となります。
$\begin{matrix} f(1, 1) & f(1, 2) & \cdots & f(1, n) & \cdots \\ f(2, 1) & f(2, 2) & \cdots & f(2, n) & \cdots \\ \vdots & \vdots & \ddots & \vdots & \\ f(n, 1) & f(n, 2) & \cdots & f(n, n) & \cdots \\ \vdots & \vdots & & \vdots & \\ \end{matrix}$