Σ 1健全性による不完全性定理
まえがき
このページでは、\(\Sigma_1\)健全性による不完全性定理の証明を解説します。 専門書による解説とは一味違う素人っぽさが売りです(^^; 何せ、筆者は不完全性定理をそれほど理解しているわけではありませんので。 でも、逆に言うなら、同じような素人には専門書より分かりやすいかもしれません。 とりあえず、不完全性定理を分かったつもりになりたい人は是非読んでみてください。
本ページで用いる記号の意味等は、 こちらのページ の定義を流用しますので、まずそちらを読んでおいてください。 また、以下のような約束や定理を用います。
- \(\Sigma_1\)健全性が成り立てば、形式的な無矛盾性も成り立つ。
- 標準モデルで計算可能な関数や述語は、形式的自然数論にも存在する。
【Σ1論理式とその形式的完全性】
ゲーデル数 \(x\) の閉論理式が形式的に証明可能という述語は \(p(x)=1\) と表すことができます。 ここで、\(x\) の形式的証明のゲーデル数は \(y\) であるという述語を \(P(x,y)\) とすると以下の関係が成り立ちます。
\[ p(x)=1\Leftrightarrow \exists y P(x,y) \]\(P(x,y)\) は原始帰納的に作ることが可能なのですが、 このように、原始帰納的述語に１回だけ存在量化子「\(\exists\)」 を適用して作られる論理式を\(\Sigma_1\)論理式と言います。 一般には、\(A(x,y)\) を原始帰納的述語とすると、 \(\exists y A(x,y)\) を\(\Sigma_1\)論理式と言います。 つまり、\(p(x)=1\) は\(\Sigma_1\)論理式です。 また、\(A(x,y)\) に全称量化子「\(\forall\)」を１回だけ適用して作られる論理式 \(\forall y A(x,y)\) を\(\Pi_1\)論理式と言います。次の関係が成り立つので、
\[ \lnot\exists y A(x,y)\Leftrightarrow \forall y\lnot A(x,y) \]\(\Sigma_1\)論理式の否定は\(\Pi_1\)論理式であり、 \(\Pi_1\)論理式の否定は\(\Sigma_1\)論理式です。
ところで、\(\exists y A(x,y)\) は自由変数 \(x\) を持ちますが、 自由変数を持たない\(\Sigma_1\)閉論理式や\(\Pi_1\)閉論理式もあります。 今、\(\Sigma_1\)閉論理式の全てと\(\Pi_1\)閉論理式の全てを合わせた集合を \(F_1\) とします。すると、\(F_1\) は否定の演算に対して閉じていることになります。
一方、\(F\) を自然数論の閉論理式全ての集合とすると、 形式的完全性は以下の条件で表されました。
\[ \forall f\in F(p(|f|)=1\lor p(|\lnot f|)=1) \]これに対して、議論する論理式の範囲を \(F\) の部分集合である \(F_1\) に限定すれば、 \(F_1\) の形式的完全性を議論することができます。 \(F_1\) は否定の演算に対して閉じているからです。
\[ \forall f\in F_1(p(|f|)=1\lor p(|\lnot f|)=1) \]【Σ1健全性とΠ1健全性】
こちらのページ では、自然数論の閉論理式の集合 \(F\) に対して健全性を仮定しました。 ここでは、議論の範囲を \(F_1\) に限定して、健全性をより弱い仮定に置き換えます。 それが、\(\Sigma_1\)健全性と\(\Pi_1\)健全性です。 つまり、以下の関係が成り立つと仮定します。
\[ \forall f\in F_1(~p(|f|)=1\Rightarrow f~) \]\(\Sigma_1\)健全性だけだと、\(f\) が\(\Sigma_1\)論理式の場合、 \(p(|\lnot f|)=1\Rightarrow\lnot f\) を考える時に困ってしまいます。\(\lnot f\) は\(\Pi_1\)論理式だからです。
ただし専門書では、 \(\Sigma_1\)健全性だけしか仮定していないことが多いと思います。 実は、自然数論を展開できるような公理系、 つまり、ペアノ算術から数学的帰納法の公理を取り除いた理論の拡大理論では、 \(\Pi_1\)健全性は成り立ちます。 なので、\(\Pi_1\)健全性は仮定する必要がないのです。
【限定された自然数論の不完全性】
さて、\(F_1\) に範囲を限定した自然数論が形式的に完全で、 \(\Sigma_1\)健全かつ\(\Pi_1\)健全だと仮定しましょう。 すると、 \(F_1\) の範囲で証明不能と反証可能が同値になりますので以下の関係が成り立ちます。
\[ \forall f\in F_1(~p(|f|)=0\Leftrightarrow p(|\lnot f|)=1~) \]すると、以下の関係が成り立ちます。
\[ \forall f\in F_1(~f\Leftrightarrow p(|f|)=1~) \]つまり、\(F_1\) の範囲で \(p(|f|)=t(|f|)\) となって、 \(F_1\) に範囲を限定した万能論理式 \(u_1(m,n)\) を考えることができます。
\[ u_1(m,n):=p(s(m,n))=1 \]今、\(f(n):=\lnot u_1(n,n)\) と置くと、 \(f(n)\) は\(\Pi_1\)論理式です。 なぜなら \(p(x)=1\) が\(\Sigma_1\)論理式だからです。 よって、\(f(n)\in F_1\) であり、適当な \(m\) を選ぶことにより、 以下の関係が成り立ちます。
\[ u_1(m,n)\Leftrightarrow f(n)\Leftrightarrow\lnot u_1(n,n) \]ここで、入力 \(n\) を \(n = m\) と置くとリシャールのパラドクスが起こります。 したがって、\(F_1\) に範囲を限定した自然数論は、 \(\Sigma_1\)健全かつ\(\Pi_1\)健全であるなら形式的に完全ではありません。 範囲を限定した自然数論で既に完全ではないのですから、 それを含むより大きな自然数論は完全にはなり得ません。
また、\(\Sigma_1\)健全かつ\(\Pi_1\)健全と仮定すると、 こちら で行ったゲーデル文による不完全性の証明がそのまま通用します。 \(G(y)\) は\(\Pi_1\)論理式で、\(\lnot G(y)\) は\(\Sigma_1\)論理式だからです。
【Σ1完全性とΣ1健全性による不完全性】
先に、\(\Sigma_1\)健全性と\(\Pi_1\)健全性により不完全性を証明しましたが、 \(\Pi_1\)健全性の代わりに\(\Sigma_1\)完全性を用いても不完全性は証明できます。 専門書が採用しているのは、こちらの方法ですね。ちょっとやってみましょう。
\(\Sigma_1\)完全性とは、\(f\) を\(\Sigma_1\)閉論理式とするとき、 以下の関係が成り立つことを言います。
\[ f\Rightarrow p(|f|)=1 \]つまり、「Σ1閉論理式は正しいなら形式的に証明できる」 ということです。 \(\Sigma_1\)完全性は、自然数論を展開できるような公理系なら成り立ちます。 なので、普通はいちいち仮定しません。
では、不完全性を証明しましょう。 まず、\(\Sigma_1\)健全性より、ゲーデル文 \(G(g)\) は以下の関係を満たします。
\[ \begin{eqnarray} p(|\lnot G(g)|)=1 &\Leftrightarrow& p(|p(s(g,g))=1|)=1 \\ &\Rightarrow & p(s(g,g))=1 ~~\cdots \Sigma_1健全性より \\ &\Leftrightarrow& p(|G(g)|)=1 \end{eqnarray} \]次に、上の証明を逆からたどって、\(\Sigma_1\)完全性より、 ゲーデル文 \(G(g)\) は以下の関係を満たします。
\[ \begin{eqnarray} p(|G(g)|)=1 &\Leftrightarrow& p(s(g,g))=1 \\ &\Rightarrow & p(|p(s(g,g))=1|)=1 ~~\cdots \Sigma_1完全性より \\ &\Leftrightarrow& p(|\lnot G(g)|)=1 \end{eqnarray} \]両方合わせると、
\[ p(|G(g)|)=1 \Leftrightarrow p(|\lnot G(g)|)=1 \]となります。\(\lnot G(g)\) が\(\Sigma_1\)論理式という事実を用いました。
\(A\Leftrightarrow B\) という関係は、 \(A\land B\) または \(\lnot A\land\lnot B\) と同値です。 もし、形式的に完全ならば、 \(p(|G(g)|)=0\land p(|\lnot G(g)|)=0\) という選択は許されません。 すると、\(p(|G(g)|)=1\land p(|\lnot G(g)|)=1\) となり形式的に矛盾します。 \(\Sigma_1\)健全なら形式的に無矛盾のはずなので、 これは、形式的に完全であるという仮定に問題があるということです。 よって、\(p(x)\) は形式的に不完全です。 したがって、ゲーデル文は証明も反証もできません。
【Σ1完全性の直感的解釈】
ここでは、\(\Sigma_1\)完全性の直感的解釈を説明します。 \(\Sigma_1\)完全性は、量化子を陽に表して書くと以下のようになります。 ただし、\(A(x)\)は原始帰納的述語です。
\[ \exists x A(x)\Rightarrow p(|\exists x A(x)|)=1 \]標準モデルの自然数で考えると、\(\exists x A(x)\) が真なら、 有限な自然数 \(n\) が存在して \(A(n)\) が真になるはずです。 \(A(x)\) は原始帰納的ですので、\(n\) の値が具体的に分からなくとも、 \(x = 0,1,2,\ldots,n\) と確認していくと、 有限なステップ数で \(A(n)\) が証明できることは明らかです。 つまり、\(p(|\exists x A(x)|)=1\) ということです。
【Π1健全性の直感的解釈】
ここでは、\(\Pi_1\)健全性の直感的解釈を説明します。 \(\Pi_1\)健全性は、量化子を陽に表して書くと以下のようになります。 ただし、\(A(x)\)は原始帰納的述語です。
\[ p(|\forall x A(x)|)=1\Rightarrow \forall x A(x) \]\(p(|\forall x A(x)|)=1\) の \(p(~)\) の中では、 超準モデル、すなわち無限大の数で証明できる場合も考える必要があります。 超準モデルで \(\forall x A(x)\) が証明できるなら、 \(x\) には全称量化子が付いているので、 標準モデルの自然数の範囲に制限しても証明できるのは明らかです。 \(A(x)\) は原始帰納的なので、 \(n\) を有限な自然数の任意定数とすると、\(A(n)\) が証明できることになり、 標準モデルにおいて \(A(n)\) は真になります。 つまり、標準モデルで \(\forall x A(x)\) ということです。 ただし、 \(\Pi_1\)健全であることを確実に保証するには無矛盾であるという条件が必要です。
【Σ1健全性の直感的解釈】
ここでは、\(\Sigma_1\)健全性の直感的解釈を説明します。 \(\Sigma_1\)健全性は、量化子を陽に表して書くと以下のようになります。 ただし、\(A(x)\)は原始帰納的述語です。
\[ p(|\exists x A(x)|)=1\Rightarrow \exists x A(x) \]\(p(|\exists x A(x)|)=1\) の \(p(~)\) の中では、 超準モデル、すなわち無限大の数で証明できる場合も考える必要があります。 \(\exists x A(x)\) が、\(x\) が無限大の数でしか証明できない場合、 標準モデルの自然数の範囲で \(\exists x A(x)\) が成り立つ保証はありません。 つまり、\(\Sigma_1\)健全性は、 自然数論が展開できる公理系なら無条件に成り立つわけではないのです。 そのため、不完全性を証明する場合の前提として仮定されます。
【Π1完全性の直感的解釈】
ここでは、\(\Pi_1\)完全性の直感的解釈を説明します。 \(\Pi_1\)完全性は、量化子を陽に表して書くと以下のようになります。 ただし、\(A(x)\)は原始帰納的述語です。
\[ \forall x A(x)\Rightarrow p(|\forall x A(x)|)=1 \]\(p(|\forall x A(x)|)=1\) の \(p(~)\) の中では、 超準モデル、すなわち無限大の数で証明する場合も考える必要があります。 標準モデルの自然数で \(\forall x A(x)\) が真でも、 超準モデルの数全てで \(A(x)\) が証明できる保証はありません。 また、標準モデルに限っても、 その全てを証明するのに必要なステップ数は有限にはなりません。 \(p(x)\) による証明の長さは有限でなければなりません。 つまり、自然数論では\(\Pi_1\)完全性は成立しません。 \(\Pi_1\)完全性が成立しないことは、 \(F_1\) が形式的に不完全であることの原因になっています。 もし、\(\Sigma_1\)完全性と\(\Pi_1\)完全性が共に成り立つと、 あらゆる \(F_1\) の論理式が証明あるいは反証可能となって、 \(F_1\) が形式的に完全になります。