クライゼルの注意

　第二不完全性定理によると、ペアノ算術を含む再帰的に公理化可能な理論 \(T\) は、形式的に無矛盾ならその無矛盾性は形式的に証明できません。しかし、ある種の論理式に関しては、無矛盾性が証明できるように見えることがあります。ここでは、理論 \(T\) において、その無矛盾性を証明できるように見えるクライゼルの注意について説明します。オリジナルのクライゼルの注意は、ロッサーの可証性述語を用いますが、ここではより直感的で分かりやすい方法を紹介します。また、理論 \(T\) の無矛盾性を証明するのに \(T\) 自身ではなくペアノ算術 PA を用いるものとします。こうすると、クライゼルの注意が本当は無矛盾性の証明にならないことが分かります。

　説明に使う用語の意味は、こちらのページで定義したものを使いますので、最初の方を予め読んでおいてください。

【無矛盾性述語】

　まず、無矛盾であることを表す述語を定義しましょう。この述語が証明可能であれば無矛盾性が証明できることになります。

　それには、ゲーデル数が \(x\) の閉論理式の形式的証明のゲーデル数は \(y\) であるという原始帰納的述語 \(P(x,y)\) を使って、ゲーデル数が \(x\) の閉論理式が証明できないことを表す述語 \(D(x)\) を以下のように定義します。

\[ \newcommand{\neg}{\mathrm{neg}} D(x):=\exists y.P(\neg(x),y)\lor\forall y.\lnot P(x,y) \]

　ここで、\(\neg(|f|) = |\lnot f|\) です。

　素朴に考えると証明できないことを表す述語は \(\forall y.\lnot P(x,y)\) ですが、\(D(x)\) には、さらに \(\exists y.P(\neg(x),y)\) が論理和で加わっています。つまり、反証できるなら証明できないということです。これは公理を用いない推論システムの拡張になっており、 \(D(x)\) に無矛盾性を組み込むことに相当します。ただし、理論 \(T\) が形式的に無矛盾であることを前提にしています。

　\(P(x,y)\) が素朴な証明述語の場合、\(\forall y.\lnot P(x,y)\) は計算するのに無限の時間がかかりますが、 \(\exists y.P(\neg(x),y)\) が加わると、反証できる場合は有限の時間で証明できないことが判定できます。

　\(D(x)\) を使うと無矛盾性を表すと思われる述語は以下のようになります。

\[ D(|1=0|) \]

　つまり、矛盾は証明できないという述語が無矛盾性を表すはずだというわけです。

【見かけ上の無矛盾性】

　第二不完全性定理によると、理論 \(T\) はその無矛盾性を形式的に証明できないはずです。しかし、上記で定義した無矛盾性を表す述語 \(D(|1=0|)\) は形式的に証明できます。つまり、以下の式が成り立ちます。ここで、\(P_0(x,y)\) はペアノ算術の証明述語です。

\[ \exists y.P_0(|D(|1=0|)|,y) \]

　これは、\(\exists y.P(\neg(|1=0|),y)\) が真理値が真の\(\Sigma_1\)論理式であるためです。つまり、\(\Sigma_1\)完全性により証明できます。このような現象がクライゼルの注意と呼ばれています。

　なぜ、こんなことが起こったのでしょうか。種を明かすと、\(D(x)\) には見かけ上の無矛盾性が組み込まれているからです。実は \(D(|1=0|)\) は、理論 \(T\) が実際には矛盾している場合でも、それとは無関係に成り立ちます。つまり、\(D(|1=0|)\) が証明できても、理論 \(T\) が無矛盾であることの保障にはなりません。

　ようするに、理論 \(T\) が矛盾している場合、つまり、公理が矛盾している場合は、 \(D(x)\) は証明できないことを表す述語ではないのです。証明できないという判定が公理から決まるのではなく、 \(D(x)\) の形から決まるからです。その形を用いる根拠に、理論 \(T\) の無矛盾性が仮定されています。なので、無矛盾性が成り立たない場合はうまく機能しないわけです。

【ロッサーの証明述語】

　ここでは、オリジナルのクライゼルの注意を理解するために、ロッサーの証明述語について説明します。対象とする理論 \(T\) は形式的に無矛盾であるとします。ロッサーの証明述語とは以下の式で定義される \(P_R(x,y)\) のことです。

\[ P_R(x,y):=P(x,y)\land\forall z\lt y.\lnot P(\neg(x),z) \]

　この証明述語を用いると、ロッサーの証明関数(本来は可証性述語)は以下のように定義できます。

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

　理論 \(T\) が無矛盾なら、ゲーデル数が \(a\) の論理式が証明できるとき、その形式的証明のゲーデル数を \(b\) とすると、 \(P(a,b)\) は真となり、無矛盾性より \(\forall z\lt b.\lnot P(\neg(a),z)\) も真になります。つまり、\(p_R(a)=1\) です。また、全ての \(y\) に対して \(P(a,y)\) が成り立たないとき、つまり、ゲーデル数が \(a\) の論理式が証明できないときは \(p_R(a)=0\) となるので、\(p_R(x)\) は証明関数になっています。ただし、ここでは標準モデルで解釈しています。

　クライゼルの注意は、ロッサーの証明述語を用いても証明できます。それには、証明できないことを表す述語 \(D_R(x)\) を以下のように定義します。

\[ D_R(x):=\forall y.\lnot P_R(x,y) \]

　中身を見ると \(D_R(x)\) は以下のようになります。

\[ D_R(x)\Leftrightarrow \forall y.(~\lnot P(x,y)\lor\exists z\lt y.P(\neg(x),z)~) \]

　ゲーデル数が \(a\) の論理式が反証できる場合、標準モデルの自然数 \(b\) が存在して \(P(\neg(a),b)\) が成り立ちます。したがって、\(b\lt y\) なら、 \(\exists z\lt y.P(\neg(a),z)\) は成り立ちます。 \(y\) が超準モデルの自然数でもよいことに注意してください。

　また、理論 \(T\) は無矛盾であることから \(\lnot P(a,y)\) は \(y\) が標準モデルの自然数なら成り立ちます。

　この２つを重ね合わせると、\(D_R(a)\) が成り立ちます。それも、理論 \(T\) のあらゆる超準モデルで成り立ちます。すなわち、\(D_R(a)\) が形式的に証明できます。したがって、\(D_R(|1=0|)\) も証明できることになり、ロッサーの証明述語を用いても、クライゼルの注意が引き起こされることが分かります。引き起こされる理由は、やはり、 \(D_R(x)\) に見かけ上の無矛盾性を組み込んでいるからです。

【〇×式の試験と論理的必然性】

　上記で説明した \(D(|1=0|)\) は、その理論が矛盾しているときにも形式的に証明できました。そのため、その理論が無矛盾であることの保証にはなりませんでした。しかし、ロッサーの証明述語で作った \(D_R(|1=0|)\) は、その理論が矛盾するとき、ゲーデル数の定め方を工夫すると \(p_R(x)\) が全ての論理式を証明可能となり、形式的に証明できなくなります。これは、\(D_R(|1=0|)\) が無矛盾性の正当な証であることを意味するのでしょうか？

　もし、ロッサーの証明述語が本当に形式的証明の手順を論理的に実現しているのなら、ゲーデル数の定め方を変えたとしても、 \(p_R(x)\) による証明の可否が変化することはないはずです。ゲーデル数の定め方は実装の詳細であって、形式的証明のインターフェイスには影響しないはずだからです。したがって、ゲーデル数の定め方で証明の可否が変化するということは、ロッサーの証明述語が本当は証明述語ではなく、偶然、証明述語のように振る舞っているだけと考えられます。

　これは、〇×式の試験を考えてみると理解できると思います。問題の解き方を知っている人は当然この試験に正解します。しかし、問題の解き方を知らない人や誤解している人が、正解できないかと言うとそうではありません。偶然正解してしまうことはあります。ロッサーの証明述語もまさしく偶然正解しているわけです。よって、\(D_R(|1=0|)\) は無矛盾性の正当な証とはなりません。