自分自身の無矛盾性が証明できる強い自然数の理論体系

通常言われるゲーデルの第2不完全性定理の内容はこうだ。

ある程度強い(正確にはロビンソン算術を含む)自然数(をコードできる)体系は自分自身の無矛盾性を証明できない

今日は、非常に強い自然数の理論体系(数理論理学の用語で「算術」と呼ばれる)で、自分自身の無矛盾性を証明できるものを与える。もちろん、上と矛盾しないように仕掛けがしてあるのだが、言いたいことは、第2不完全性定理の成立には体系の強さが問題であるかのような言い方は問題がある、ということだ。

2階論理と竹内予想

まず2階論理というものを導入する。これは通常の一階述語論理が量化(すべての〜について・ある〜が存在して)の範囲が個体であるのに対し、2階述語論理は個体の他に性質に対する量化が存在する。つまり

  1. 個体変数 x_1, x_2, \ldots
  2. 述語変数 X_1, X_2, \ldots
  3. 個体量化子 \forall^i, \exists^i
  4. 述語量化子 \forall^p, \exists^p

と関数記号、プリミティブな述語から命題が構成される。例えば、\forall X \forall x \forall y\ x = y \implies Xx \iff Xyなど。ただし、量化子の上のpiは今後省略する。

さて、推論規則はシーケント計算を用いるが、述語量化子については次のようにルールを変える。

\phi(\lambda x.\psi(x)/X)の意味は、φの中のどんなXtもψ(t)に置き換える、という意味だ。

2階算術の無矛盾性証明と竹内予想

さて、2階論理を推論に使う算術を2階算術と言う。2階算術はたいへん強い体系と考えれている。例えば2階算術は「古典的」な数学(集合論に訴えない19世紀的な数学)をそのままコードできる。また、証明論(証明の機械的操作について研究する分野)による解析能力をほぼ超えた理論であると考えられている。

2階算術の特徴は、数学的帰納法を明示的に公理としておく必要がないところだ。なぜかと言うと、次のような命題を定義する。

N(x) \equiv \forall X~[X0 \land \forall n(Xn \implies X(n+1)) \implies Xx]

この命題は、任意の0を含み、+1という操作で閉じている性質Xにxが含まれている、と言っている。このようなxに対して数学的帰納法を用いることができるのはすぐに分かるだろう。よって、ある自然数論の命題、例えばx+y = y+xN(x) \land N(y) \implies x+y = y+xと書き直すことによって、数学的帰納法を公理として立てなくても用いることができる。

さて、シーケント計算にはカットルールというルールがある。

名称未設定

一階述語論理では、このルールは不要だ。つまり、このルールがあってもなくても証明できることは変わらない。ただし、この性質(カット除去定理)の証明はそれなりに難しいため、最初はカットルールを入れておくことが通例である。

では、2階論理ではカット除去定理はなりたつだろうか。つまり、2階論理でもカットルールがあってもなくても証明できることは変わらないのだろうか。2階論理でのカット除去定理を竹内外史が予想したことから竹内予想と呼ぶ。

竹内予想は次のような意義がある。まず、\mathbf{Ax}をすべての算術の公理を∧で結んだものとしよう(ただし数学的帰納法は除く)。もし2階算術が矛盾していたとすると、\neg\mathbf{Ax}が純粋な2階論理の定理である。ところで、カットなしで2階論理を定式化できたとする。すると、証明の途中に現れる命題に述語量化子が含まれたとすると、それはその後除去することができない。一方、\neg\mathbf{Ax}は個体量化子しか持っていないのでそれはありえない。つまり、\neg\mathbf{Ax}は1階述語論理の定理となる。よって、1階算術がすでに矛盾しているはずである。

つまり、竹内予想は2階算術の無矛盾性を1階算術の無矛盾性に還元する。1階算術の無矛盾性は(頑張る必要があるが)2階算術の中で証明できる一方で、もちろん2階算術の無矛盾性は2階算術では証明できない。よって、竹内予想に2階算術の無矛盾性証明の難しさが含まれていることになる。

竹内予想はW. Taitにより証明されている(W. Tait, A non constructive proof of Gentzen’s Hauptsatz for second

order predicate logic, Bull. Amer. Math. Soc. 72(1966), 980-983.)ので成立する定理であるが、今でも竹内予想といわれることが多い。

カットなし2階算術とその無矛盾性

ここで、最初からカットルールなしの2階論理を使って証明を行う算術を考えよう。これをカットなし2階算術と呼ぶことにする。竹内予想により、カットなし2階算術は通常の2階算術と同じ定理を持つ。一方で、上の議論からカットなし2階算術が矛盾すると、1階算術も矛盾する。このことは2階算術の中で簡単に証明できる。一方、1階算術の無矛盾性は2階算術で証明できる。カットなし2階算術は通常の2階算術と同じ定理を証明するから、カットなし2階算術の無矛盾性はカットなし2階算術で証明できる。つまりカットなし2階算術は自分自身の無矛盾性が証明できる算術の体系である。

なぜ第2不完全性定理がなりたたないか

これは第2不完全性定理に反しているように見える。しかし、第2不完全定理は第1不完全性定理から、対象の理論TがLöbの条件と呼ばれる3条件

  1. T \vdash \phiならばT \vdash \mathrm{Prov}(\lceil \phi \rceil)
  2. T \vdash \mathrm{Prov}(\lceil \phi \to \psi \rceil) \land \mathrm{Prov}(\lceil \phi \rceil) \to \mathrm{Prov}(\lceil \psi \rceil)
  3. T \vdash \mathrm{Prov}(\lceil \phi \rceil) \to \mathrm{Prov}(\lceil \mathrm{Prov}(\lceil \phi \rceil) \rceil)

を満たしていることを仮定して導かれる。カットなし2階算術はこのうち2.が成り立っていない。細かく言うと、T \vdash \ldotsの右側は真なのだが、カットなし2階算術では証明することができない。というのは、\phi \to \psiの証明と\phiの証明から\psiの証明を得る簡単なやり方はカットルールを使うことだが、カットなし2階算術はカットルールを持たないためこのやり方が使えないからだ。カットルールを使わずに\psiの証明を得る方法は、実質的に竹内予想の証明と同じである。

教訓

最初に述べたが、第2不完全性定理は次のように紹介されることが多い。

ある程度強い(正確にはロビンソン算術を含む)自然数(をコードできる)体系は自分自身の無矛盾性を証明できない

これは誤りではないのだが、上記のように使う論理の定式化に手を加えると「強さ」を保ったまま第2不完全性定理が成り立たないようにできる。他方、「弱い」体系で不完全性定理が成り立たない例としてPresburger算術(足し算のみの算術)が挙げられる。Presburger算術は完全(その言語で記述できる任意の定理が証明可能)である。しかし、これは第1不完全性定理が成り立たないことに過ぎない。第2不完全性定理はPresburger算術でも成り立たない。というのは、掛け算を使わずにゲーデル数化を行うことはできず、Presburger算術の言語では無矛盾性をコードすることすらできないからである。

よって、第2不完全性定理の成立にその体系の「強さ」が問題であるかのように考えるのは不適切である。では他にゲーデルの第2不完全性定理を特徴づける簡単な性質がないかというと、「自己言及」しかないように思う。実際、自分自身の証明概念をコードしそれについての最小限度の性質が証明できる(自己言及ができる、と言っても良い)体系であれば、強さにかかわらず第2不完全性定理が示せる。そういう意味で、よく言われる「ゲーデルの不完全性定理は自己言及の限界を示している/自己言及により数学の限界を示した」はそれほど的はずれな主張ではない。