不完全性定理の説明の備忘録

　ここでは、私が思いついたアイディアを忘れないために書いておきます。つまり、正しいかどうか分からないし、記号の説明なども十分ではありませんが、備忘録なのでご了承ください。

　この備忘録の本文はこちらです。興味がわいたら読んでみてください。用語や記号の意味も、その一部は本文で解説してあります。

【ゲーデル・ロッサーの定理】

　本文では、自然数論を含む再帰的に公理化可能な理論が健全なら不完全であることを示しました。一般には、多少制限を緩和した\(\Sigma_1\)健全であることを仮定します。そして、第一不完全性定理の最も汎用的なバージョンは、さらに緩い条件の形式的に無矛盾という仮定で成り立ちます。これをゲーデル・ロッサーの定理と言います。ここでは、ゲーデル・ロッサーの定理を、筆者が思いついた独自の方法で証明します。対象となる理論 \(T\) は再帰的に公理化可能で形式的に無矛盾な自然数論であり、 \(\Sigma_1\)健全ではないものとします。

　それでは証明を始めます。まず、理論 \(T\) の通常の証明関数 \(p(x)\) を、ゲーデル数が \(x\) の閉論理式の形式的証明のゲーデル数は \(y\) であるという原始帰納的述語 \(P(x,y)\) を用いて以下のように定義します。

\[ p(x) = \left\{ \begin{array}{cl} 1 & (~\exists y~P(x,y)~) \\ 0 & (~\forall y~\lnot P(x,y)~) \end{array} \right. \]

　\(p(a)=1\) ならゲーデル数が \(a\) の閉論理式が形式的に証明可能で、 \(p(a)=0\) なら証明不能です。

　次に、以下のように定義される \(P_c(x,y)\) を用いて

\[ P_c(x,y):=\mathrm{std}(y)=1\land P(x,y) \]

　\(p_c(x)\) を以下のように定義します。

\[ p_c(x) = \left\{ \begin{array}{cl} 1 & (~\exists y~P_c(x,y)~) \\ 0 & (~\forall y~\lnot P_c(x,y)~) \end{array} \right. \]

　\(p_c(x)\) を標準モデルと互換性のある証明関数と呼ぶことにします。

　ここで、\(\mathrm{std}(y)\) の超準モデルにおける代表的な実装は、 \(y\) が標準モデルの自然数なら、つまり有限の数なら \(1\) を返し、 \(y\) が超準モデルの自然数なら、つまり無限大の数なら \(0\) を返すというものです。

　\(\mathrm{std}(y)\) を考えると、もともとの公理系に対して \(\mathrm{std}(y)\) を定義する公理が付け加わるため、理論 \(T\) を拡大することになりますが、確認しようとしていることが、証明も反証もできない論理式があることなので、拡大理論で確認すれば、もともとの理論 \(T\) でも証明も反証もできないことになるので大丈夫です。

　さて、標準モデルと互換性のある証明関数は、理論 \(T\) が無矛盾なら、引数 \(a\) が閉論理式のゲーデル数である場合に、形式的証明において標準モデルと同様に振る舞います。そのため、以下の関係が成り立ちます。

\[ \begin{eqnarray} p(|p_c(a)=1|)=1 & \Rightarrow & p(a)=1 \\ p(|p_c(a)=0|)=1 & \Rightarrow & p(a)=0 \end{eqnarray}\tag{関係◇1} \]

　何故ならば、標準モデルで \(p(a)=0\) ならば、 \(y\) が公理で存在を保証された無限大のとき、超準モデルで、\(\mathrm{std}(y)=0\) となり、 \(\exists y~\mathrm{std}(y)=1\land P(a,y)\) は偽となるので、 \(p_c(a)=1\) は成り立ちません。よって、無矛盾性により \(p(a)=0 \Rightarrow p(|p_c(a)=1|)=0\) であり、その対偶を取ると \(p(|p_c(a)=1|)=1 \Rightarrow p(a)=1\) が成り立ちます。

　また、標準モデルで \(p(a)=1\) ならば、明らかに \(p_c(a)=0\) が成り立たない超準モデルがあります。よって、無矛盾性により \(p(a)=1 \Rightarrow p(|p_c(a)=0|)=0\) であり、その対偶を取ると \(p(|p_c(a)=0|)=1 \Rightarrow p(a)=0\) が成り立ちます。

　ここでは、理論 \(T\) が無矛盾ならモデルを持ち、論理式 \(f\) が形式的に証明できるなら、そのモデルにおいて \(f\) は真であるという性質を用いました。実際にはその対偶をとって、無矛盾のとき、\(f\) が偽となるモデルがあるなら \(f\) は形式的に証明できないという性質を用いました。

　次に、上記の \(p_c(x)\) を使って、論理式 \(G(z)\) を以下のように定義します。

\[ G(z):=p_c(s(z,z))=0 \]

　そして、\(g\) を \(G(z)\) の論理式番号とするとき、 \(G(g)\) を修正ゲーデル文と呼ぶことにします。 \(s(g,g)=|G(g)|\) なので以下の関係が成り立ちます。

\[ \begin{eqnarray} p(|G(g)|)=1 & \Leftrightarrow & p(|p_c(|G(g)|)=0|)=1 \\ p(|\lnot G(g)|)=1 & \Leftrightarrow & p(|p_c(|G(g)|)=1|)=1 \end{eqnarray}\tag{関係◇2} \]

　修正ゲーデル文を使うと、理論 \(T\) の不完全性を証明することができます。

　まず、修正ゲーデル文が形式的に証明できる仮定します。つまり、\(p(|G(g)|)=1\) だと仮定します。すると(関係◇2)より、以下のように \(p(|p_c(|G(g)|)=0|)=1\) が成り立ちます。

\[ p(|G(g)|)=1 \Leftrightarrow p(|p_c(|G(g)|)=0|)=1 \]

　すると(関係◇1)より、以下のように \(p(|G(g)|)=0\) が成り立ちます。

\[ p(|p_c(|G(g)|)=0|)=1 \Rightarrow p(|G(g)|)=0 \]

　これは矛盾なので、仮定が間違いであり \(p(|G(g)|)=0\) が成り立ちます。よって、修正ゲーデル文は形式的に証明することはできません。

　次に、修正ゲーデル文は形式的に反証できると仮定します。つまり、\(p(|\lnot G(g)|)=1\) と仮定します。すると(関係◇2)より、以下のように \(p(|p_c(|G(g)|)=1|)=1\) が成り立ちます。

\[ p(|\lnot G(g)|)=1 \Leftrightarrow p(|p_c(|G(g)|)=1|)=1 \]

　すると(関係◇1)より、以下のように \(p(|G(g)|)=1\) が成り立ちます。

\[ p(|p_c(|G(g)|)=1|)=1 \Rightarrow p(|G(g)|)=1 \]

　これは形式的に矛盾です。理論 \(T\) は形式的に無矛盾のはずなので、仮定が間違いであり \(p(|\lnot G(g)|)=0\) が成り立ちます。よって、修正ゲーデル文は形式的に反証することもできません。

　以上より、自然数論を含む再帰的に公理化可能な理論 \(T\) は、形式的に無矛盾で\(\Sigma_1\)健全でないなら不完全です。 \(\Sigma_1\)健全な場合にも不完全性は証明できるので、結局、形式的に無矛盾なら不完全ということになります。

【健全性と証明関数】

　本ページでは、健全性という性質に頻繁に言及してきました。しかし、実は健全性という言葉は、数理論理学では２通りに解釈されます。まず１つ目、述語論理における健全性を仮に第一健全性と呼ぶことにしますと、それは以下のように表すことができます。

\[ \mathbb{N}\vDash p(|f|)=1\Rightarrow\mathbb{M}\vDash f \]

　つまり、証明関数が１なら、想定しているモデルで真になるということです。

　これに対して、本ページで主に用いられてきた健全性を第二健全性と呼ぶことにすると、それは以下のように表すことができます。

\[ \mathbb{N}\vDash p(|f|)=1\Rightarrow\mathbb{N}\vDash f \]

　つまり、証明関数が１なら、標準モデルで真になるということです。不完全性定理が語られるような文脈では、こちらの健全性が想定されていることが多いようです。理論が標準モデルを持つ場合は２つの健全性は同じになります。私は始め、この２つの健全性の区別がよく分からず、随分と悩みました。

　証明関数 \(p(x)\) は、一般には第一健全性を満たします。第二健全性が成り立たない場合も、無矛盾ならば第一健全性は成り立っています。ならば、発想を逆転させて、第一健全性を証明関数の定義にしてしまえば良いのではないかと思います。実際、形式的に証明できたのに想定しているモデルで偽になる証明関数なんて、使い物になりませんよね。

　第一健全性を証明関数の定義としたとき問題になるのは、第一健全性を満たす関数が存在し得るかという点です。ゲーデルさんのすごいところは、第一健全性を満たす関数を具体的に構成してみせたところではないかと思います。これができてしまえば、その後の不完全性の証明はある意味簡単と言えます。リシャールのパラドクスや対角線論法を知っていれば、ゲーデルさんでなくとも思いついたのではないでしょうか？

　事実、不完全性定理の解説本では、証明関数の具体的構成は省略されていることが多いようです。例外的に数学ガールの不完全性定理版では、証明関数(実際には可証性述語)の具体的構成が書かれています。興味のある人は読んでみることをお勧めします。いかに面倒臭いか分かるでしょう。

【自己言及性パラドクスと形式的体系】

　嘘つきのパラドクスやリシャールのパラドクスは、自己言及によりパラドクスを引き起こしています。そして、不完全性定理もこの自己言及性パラドクスを用いて証明されます。そこでここでは、自己言及性パラドクスに対して掘り下げてみましょう。

　不完全性定理を証明するには、実は以下の関係が重要な役割を果たします。

\[ T\vdash f\Leftrightarrow\mathbb{N}\vDash p(|f|)=1 \]

　まず第一に、左辺の \(f\) が形式的に証明可能という概念が、右辺の証明関数 \(p(x)\) を使った論理式で算術化されています。つまり、形式的証明の可能性を具体的な論理式で定義しています。これで証明するとはどういうことかが決まります。

　次に、論理式 \(f\) がそのゲーデル数 \(|f|\) に翻訳され、証明関数の引数に渡されてその証明可能性が判断されることに注目してください。 \(p(|f|)=1\) 自身が論理式ですから、\(p(|f|)=1\) のゲーデル数を考えれば、証明するという概念自身を証明の対象にできることをこの関係は表しています。つまり、証明に関する自己言及を可能にするわけです。例えば、ゲーデル文は

\[ G(g)\Leftrightarrow\lnot(p(|G(g)|)=1) \]

　という証明に関する自己言及的な再帰的論理式です。

　このように、ゲーデル数(および論理式番号)を使うと、証明に関する自己言及性パラドクスを起こすことが可能になりますが、このような体系を非形式的な有限の立場と言います。一方で、形式的証明の対象となる体系は形式的体系と呼ばれています。

　え？何だか混乱して来たって？そうですね、不完全性定理の証明は非形式的な有限の立場で行われますが、不完全性定理の成り立つ論理式は形式的体系の論理式なんです。ややこしいですね。

　非形式的な有限の立場は、形式的体系の上に構築されています。例えばゲーデル数ですが、これは論理式を自然数に対応させる関数です。これが形式的体系の中で使えるためには、予め形式的体系の文法で、論理式を自然数に対応させる関数が扱えないといけません。しかし、自然数論の文法では自然数を自然数に対応させる関数しか許されませんので、自然数論の形式的体系の中ではゲーデル数が扱えません。そのためゲーデル数を扱うには、形式的体系のさらに上にゲーデル数を扱える階層を作ります。

　また、形式的体系の論理式の定義では、自分自身を定義に含む再帰的論理式の定義は許されません。そのため、自己言及するためにはゲーデル数が必要になります。一方で、関数の定義には自分自身を定義に含むことができます。そのため、形式的体系では関数に自己言及する再帰的関数が使えるわけです。

　ところで、非形式的な有限の立場と形式的体系には他にも重要な違いがあります。例えば \(p(|f|)=1\) という論理式ですが、非形式的な有限の立場では、 \(f\) という論理式が形式的に証明可能であることを表します。 \(p(x)\) が証明可能性を表すという意味を解釈しています。一方、形式的体系では意味は解釈しません。 \(p(x)\) が証明可能性を表すなどということは形式的体系の中では分かりません。 \(|f|\) というゲーデル数も、何らかの自然数という以上の意味は持ちません。ゲーデル数を解釈することで初めて記号の意味が解釈できるようになるのです。

　ゲーデル数が使えるか否かの違いは、些細な違いのように思えるかもしれませんが実は大問題です。ゲーデル数の利用を許すと、高階関数の利用が可能になります。しかも、ゲーデル数化できる式に制限を設けないと、無制限に高階な関数の利用が可能になります。高階関数とは、関数や論理式を引数に取り、何らかの値を返す関数ことです。非形式的な有限の立場で不完全性が証明できるのは、この高階関数のお陰です。

　このように、形式的体系はかなり制限の強い体系です。論理式のゲーデル数は使えませんし、記号の意味を用いてはなりません。高階関数も使えません。第二不完全性定理により形式的証明では無矛盾性の証明はできませんが、これは対象となる形式的体系の制限が厳しいからとも考えられます。しかしそれでも、数学のほとんどの分野は、形式的体系を使って形式化できるそうです。

　形式的体系の例としてコンピュータがそうじゃないだろうかと思う人も多いでしょう。確かに、コンピュータは AI でもなければ普通記号の意味を解釈したりせず、定められたルールに従ってのみ計算を進めるので形式的体系のように見えます。しかし、コンピュータにはゲーデル数の概念が始めから備わっています。ソースコードやファイル、アドレスやポインタといった仕組みで、実行中のシステムのコードを参照することが可能です。つまり、自己言及的です。そして、高階関数も使い放題です。コンピュータで形式的体系をエミュレーションしようと思うなら、注意深く自己言及を可能にする仕組みや高階関数の利用を制限する必要があります。

　コンピュータの分野で自己言及性パラドクスと言えば、チューリングマシンの停止性問題が有名ですね。

【プログラマ的視点による第二不完全性定理その１】

　ここでは、プログラマ的視点から第二不完全性定理を直感的に解説します。細かい条件は一切無視しますので、厳密さは諦めてください。また、本来の第二不完全性定理と違い、標準モデルを持つ理論 PA で無矛盾性が形式的に証明できないことを証明します。無矛盾性を表す式は、標準モデルで解釈しないと無矛盾性を保証できないと筆者は考えるからです。

　まず、対象とする理論 \(T\) は、数学的帰納法を扱える自然数論を含む再帰的に公理化可能な理論であり、形式的に無矛盾であるとします。そして、その証明関数を以下のように定義します。

\[ p(x) = \left\{ \begin{array}{cl} 1 & (~有限時間で判定可能で、ゲーデル数が~x~の閉論理式が形式的に証明可能~) \\ 0 & (~有限時間で判定不能で、ゲーデル数が~x~の閉論理式が形式的に証明不能~) \end{array} \right.\tag{式♪} \]

　\(p(x)\) は証明を実行し、証明可能性を判定するインタプリタです。証明不能なときに有限時間で判定不能なのは、証明できる可能性を全て調べ尽くすことで証明できないと判定するからです。

　何でもないような定義ですが、有限時間で判定可能または判定不能というあたりが重要な役割を果たします。有限時間で判定可能なのは証明可能な場合に限り、有限時間で判定不能なのは証明不能な場合に限ります。この証明関数を用いる限り、証明不能な閉論理式を有限時間で証明不能と判定するショートカットは存在しません。

　具体的には、ゲーデルさんの作った証明関数がこの条件に合致します。数式で表現すると、ゲーデル数が \(x\) の閉論理式の形式的証明のゲーデル数は \(y\) であるという原始帰納的述語 \(P(x,y)\) を使って以下のように表せます。ただし、\(p(x)\) に無矛盾性を組み込んではいけません。つまり、\(p(|\lnot f|)=1\Rightarrow p(|f|)=0\) という関係を推論に用いてはいけません。

\[ p(x) = \left\{ \begin{array}{cl} 1 & (~\exists y~P(x,y)~) \\ 0 & (~\forall y~\lnot P(x,y)~) \end{array} \right. \]

　次に、\(p(|1=0|)\) の値を判定することを考えます。 \(1=0\) は矛盾ですから、理論 \(T\) が無矛盾なら形式的には証明できないはずです。つまり、\(p(|1=0|)=0\) ですが、(\(式♪\))の定義より、そのことは有限時間では判定可能ではありません。

　人間は \(p(|1=0|)=0\) が正しいことを有限時間で判定できていますが、これは無矛盾性の仮定を用いているからです。 \(p(x)\) には \(p(|1=0|)=0\) が正しいことは有限時間では分かりません。 \(p(x)\) の推論規則には無矛盾性を組み込んでいないからです。ここでは無矛盾性を証明できるかを確認したいので、無矛盾性を推論規則に組み込んだ証明関数を使うのは本末転倒なのです。

　今、無矛盾性が証明可能と仮定しましょう。だだし、その証明には標準モデルを持つ理論 PA の証明関数 \(p_0(x)\) を用います。何故ならば、\(p(|1=0|)=0\) が無矛盾性を表すのは標準モデルにおいてだからです。一般には、\(p(x)\) が標準モデルの証明関数になる保証はありません。なので、\(p(x)\) の中では \(p(|1=0|)=0\) が無矛盾性を表しているとは限りません。

　ここで、\(p_0(x)\) の定義も(\(式♪\))と同様とします。

　さて、無矛盾性が証明できるなら、\(p_0(|p(|1=0|)=0|)=1\) が成り立ちます。すると、\(p_0(x)\) の定義よりこの論理式は有限時間で証明が終了します。さらに、PA が健全であることより \(p(|1=0|)=0\) が成り立つことになるので、有限時間で \(p(|1=0|)=0\) が判定可能になります。注意すべき点は、 PA の健全性を用いたので、PA の無矛盾性を用いたことになりますが、理論 \(T\) の無矛盾性は用いていないところです。

　一方で、先に示したように \(p(|1=0|)=0\) には、有限時間で判定可能なショートカットは存在しません。よって、\(p_0(|p(|1=0|)=0|)=1\) は矛盾であり、 \(p_0(|p(|1=0|)=0|)=0\) が成り立ちます。つまり、理論 \(T\) が無矛盾なら、その無矛盾性を(\(式♪\))の証明関数を使って表現した \(p(|1=0|)=0\) は、 PA では形式的に証明することはできません。

　以下は補足です。PA は健全なので \(p_0(|p(|1=0|)=1|)=1\) なら、\(p(|1=0|)=1\) が成り立つことになるため、\(p(|1=0|)=0\) と矛盾します。したがって、\(p_0(|p(|1=0|)=1|)=0\) となります。つまり、\(p(|1=0|)=0\) は PA では形式的に反証することもできません。 \(p(|1=0|)=0\) は PA のゲーデル文になっています。

【プログラマ的視点による第二不完全性定理その２】

　上記で、数学的帰納法が扱える自然数論を含む再帰的に公理化可能な理論 \(T\) が無矛盾のとき、その無矛盾性を表す \(p(|1=0|)=0\) は標準モデルを持つ理論 PA では形式的に証明できないことが分かりました。しかし、本来の第二不完全性定理は、 \(T\) 自身で無矛盾性が証明できないというものであり、上記の証明では自分自身の無矛盾性が証明できないことを言ったことになりません。

　ここでは、標準モデルを持たないような一般の理論 \(T\) においても、自分自身の無矛盾性が証明できないことを示します。

　まず、以下の条件を満たす \(p_c(x)\) を標準モデルと互換性のある証明関数と呼ぶことにします。

\[ \begin{eqnarray} p(|p_c(a)=1|)=1 & \Rightarrow & p(a)=1\\ p(|p_c(a)=0|)=1 & \Rightarrow & p(a)=0 \end{eqnarray} \]

　\(a\) は任意の閉論理式のゲーデル数です。詳しい定義はゲーデル・ロッサーの定理を参照してください。超準モデルでは \(p(x)\) の性質が変化して、証明関数でなくなることがありますが、\(p_c(x)\) はそのような場合でも、証明関数であることを維持しています。互換勢のある証明関数を使うと、理論 \(T\) で無矛盾性が形式的に証明できるという論理式は以下のようになります。

\[ p(|p_c(|1=0|)=0|)=1 \]

　今、この論理式が成り立つと仮定します。形式的に証明可能ですので、有限時間で判定可能です。 \(p_c(x)\) は互換性を持つように定義されているので、 \(p_c(x)\) の有限な自然数を用いて計算する部分が有限時間で計算可能となります。 \(p_c(x)\) の有限な自然数を用いて計算する部分は、理論 \(T\) に含まれる標準モデルを持つ理論の中で最大の理論で計算します。しかし、そうした理論では \(p_c(x)\) を有限時間で計算できませんでした。結局、以下の関係が成り立ちます。

\[ p(|p_c(|1=0|)=0|)=0 \]

　ようするに、互換性のある証明関数によって表される無矛盾性 \(p_c(|1=0|)=0\) は、 \(p(x)\) では形式的に証明することはできません。すなわち、理論 \(T\) が形式的に無矛盾なら、自分自身の無矛盾性を形式的に証明することはできません。

　注意すべき点は、\(p(x)\) の定義は(\(式♪\))でなければならないということです。それ以外の証明関数の定義を用いると、クライゼルの注意のところで述べた現象が起こる可能性があります。

　以下は補足です。\(p(|p_c(|1=0|)=1|)=1\) と仮定すると、互換性から \(p(|1=0|)=1\) が成り立ち \(p(|1=0|)=0\) と矛盾します。したがって、\(p(|p_c(|1=0|)=1|)=0\) が成り立ち、 \(p_c(|1=0|)=0\) は \(p(x)\) で形式的に反証することもできません。つまり、\(p_c(|1=0|)=0\) は、理論 \(T\) のゲーデル文になっています。

【プログラマ的視点による第二不完全性定理その３】

　さて、上記では(\(式♪\))の証明関数による無矛盾性は、標準モデルでは証明不能なことを示しました。しかし、(\(式♪\))の証明関数でないのなら、\(p_0(|p(|1=0|)=0|)=1\) となることもあります。つまり、\(p(|1=0|)=0\) が証明される有限な手順が存在する証明関数もあります。クライゼルの注意などがそれです。クライゼルの注意では、無矛盾性を組み込んだ証明関数を用いるため、無矛盾性が証明できるのは半ば当然です。しかも理論 \(T\) が矛盾しているときでも無矛盾性が証明できてしまうことがあるので、無矛盾性を正しく証明しているとは言えません。クライゼルの注意を回避して、正しく無矛盾性を証明することはできないのでしょうか？ここでは、その可能性を探ってみます。ただし、証明関数 \(p(x)\) は\(\Sigma_1\)論理式で定義されることとします。

　クライゼルの注意を回避するには、証明関数に無矛盾性を組み込まなくとも、理論 \(T\) の無矛盾性を証明でき、矛盾するときには無矛盾性を証明できないなら OK です。

　まず準備をします。\(p(|1=0|)=0\) は、ゲーデル数が \(x\) の閉論理式の形式的証明のゲーデル数は \(y\) であるという原始帰納的述語 \(P(x,y)\) を使うと、\(\forall y~\lnot P(|1=0|,y)\) と表せます。以下で使うので覚えておいてくださいね。

　次に、形式的に矛盾するときを考えます。無矛盾性を組み込まないなら、矛盾するとき全てが証明できるので \(\forall y~\lnot P(|1=0|,y)\) は偽であり、 \(\Pi_1\)健全性の対偶より、\(p_0(|\forall y~\lnot P(|1=0|,y)|)=0\) となり、無矛盾性が証明できないことが分かります。したがって、正しい無矛盾性の証明の条件の半分はクリアしました。

　残りの半分、形式的に無矛盾なとき無矛盾性を証明できるか調べて見ましょう。 \(\lnot P(|1=0|,y)\) を \(Q(y)\) で表すと、理論 \(T\) が無矛盾なら \(Q(0),~Q(1),~Q(2),\ldots\) は全て正しく、\(Q(y)\) が原始帰納的であることから \(Q(0),~Q(1),~Q(2),\ldots\) は全て形式的に証明可能なはずです。第二不完全性定理とは、それにも関わらず \(\forall y~Q(y)\) は形式的に証明できないというものです。単に、\(Q(0),~Q(1),~Q(2),\ldots\) の証明をつなげるだけでは、その形式的証明の長さが無限大になってしまって正しい証明ではなくなるからです。

　しかし、\(\forall y~A(y)\) の形の閉論理式が常に形式的に証明できないのかというとそんなことはなく、 \(\forall y(y=y)\) は証明可能です。つまり、\(y\) に具体的自然数を代入しなくとも \(A(n)\) という任意定数 \(n\) を含む論理式が証明可能な場合は \(\forall y~A(y)\) は証明できます。果たして、クライゼルの注意を回避して無矛盾性を正しく証明できるでしょうか？

　ここからは推測ですが、 \(Q(n)\) が証明できるためには無矛盾性が組み込まれている必要があると思います。つまり、クライゼルの注意を回避して無矛盾性を証明しようとしても、結局は無矛盾性を組み込むことになって、無矛盾性の証明としては不適切なものになると思われます。

　無矛盾性が証明できるなら、どうあがいても \(1=0\) のような反証できる論理式が与えられた場合に、それが証明できないことが有限時間で判定可能になるからです。これは、無矛盾性を表す式 \(p(|\lnot f|)=1\Rightarrow p(|f|)=0\) を証明関数の推論規則に組み込むことと同値です。

　一方、先に述べたようにクライゼルの注意も、証明関数に無矛盾性を組み込んでいるから無矛盾性が証明できるのであって、理論 \(T\) が無矛盾だから無矛盾性が証明できるわけではありません。なので、クライゼルの注意も理論 \(T\) の無矛盾性の証明としては適切ではありません。

　まとめると、無矛盾性が形式的に証明できるのは、例外なく証明関数の推論規則に無矛盾性を組み込んでいる場合ということになります。つまり、無矛盾性が形式的に証明できる場合は、その証明はすべて無矛盾性の証明としては不適切ということです。

【真の無矛盾性と仮の無矛盾性】

　クライゼルの注意を分析すると、無矛盾性には、真の無矛盾性と仮の無矛盾性の2種類の無矛盾性があるようです。

　ゲーデル数が \(x\) の閉論理式の形式的証明のゲーデル数は \(y\) であるという原始帰納的述語 \(P(x,y)\) で、証明関数 \(p(x)\) 以下のように定義するとき、

\[ p(x) = \left\{ \begin{array}{cl} 1 & (~\exists y~P(x,y)~) \\ 0 & (~\forall y~\lnot P(x,y)~) \end{array} \right. \]

　一方で仮の無矛盾性が証明可能とは、 \(\forall y~Q(y)\) が形式的に証明可能になることです。 \(Q(0)\land Q(1)\land Q(2)\land\cdots\) が無限に長い式であったのと違い、仮の無矛盾性は有限の式で表されます。これは、\(p(|\lnot f|)=1\Rightarrow p(|f|)=0\) という無矛盾性を表す関係を証明関数に組み込むということです。無矛盾性を組み込んだ証明関数は、理論 \(T\) が無矛盾な時には証明関数ですが、理論 \(T\) が矛盾するときは証明関数ではなくなります。そのため、理論 \(T\) が実際には矛盾するときでも \(p(|1=0|)=0\) を形式的に証明できることがあります。つまりこの場合、無矛盾性を組み込んだ \(p(x)\) は、実際には証明関数ではないということです。したがって、仮の無矛盾性が証明できても、実際には矛盾しているかもしれず、真の無矛盾性を正しく証明したことにはなりません。

　さて、こう考える人もいるかもしれません。真に無矛盾なときのみ証明関数に無矛盾性を組み込めば、真に無矛盾なときのみ無矛盾性を形式的に証明できるのではないだろうか？しかし、真の無矛盾性を判定するには無限に長い証明が必要です。つまり、この方法では仮の無矛盾性の証明も無限に長くなってしまうということです。これは形式的には証明できないことを意味します。