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

通常言われるゲーデルの第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不完全性定理が示せる。そういう意味で、よく言われる「ゲーデルの不完全性定理は自己言及の限界を示している/自己言及により数学の限界を示した」はそれほど的はずれな主張ではない。

5分でわかる直観主義数学

今日は直観主義数学について5分で分かるように解説する。

直観主義数学とは何か?

直観主義数学とは、オランダの数学者ブラウアー(1881-1966)によって提唱された「直観主義」という立場に基づく数学である。直観主義は通常の数学(古典数学とここでは呼ぶことにする)を批判し、独自の数学を展開する対抗数学である。

直観主義数学は排中律(任意の命題Pについて「PであるかPでないかどちらかである」とする主張)を否定する数学と紹介されることがあるが、排中律を否定するのはその主張の一部であって、他の古典数学の主張も否定されたり、古典数学とは相容れない独自の主張がなされることもある。また、気まぐれに排中律を否定しているわけではなく、その背景には理由付けが存在する。

直観主義数学にもさまざまな立場がある。狭義にはブラウアーの展開した数学を指すが、ブラウアーの数学は難解かつ独自性が強い。例えば、ブラウアーは古典数学と対立する原理を積極的に採用する。一方で、直観主義数学は、広義には構成的数学と呼ばれる立場全体全体を指す。今日は後者の立場を取りたい。なお、マルティン・レーフの直観主義的型理論(ITT)が、現在における直観主義数学の定式化の主流であるように筆者は思っている。ITTにもどのような公理を認めるかでバリエーションがあるが、バリエーションがある事自体は直観主義の立場からは何も問題はない。

なお、古典数学の立場に立ちながら、直観主義数学の体系を古典数学の対象として研究することが可能である。このような立場の数学者も多いが、私は直観主義数学を古典数学に対して全く新しい数学理念を提示するものと捉えている。

直観主義数学は大雑把に言って「具体的に操作可能なもの」だけを対象とする。よって計算機科学と親和性が深く、実際、定理支援証明系の理論的な基盤になったり、プログラミング言語理論に影響を与えたり、検証付きのプログラム生成手法の理論になったりしている。

直観主義数学が大切にするもの – 証明

直観主義数学が古典数学と最も違うのは、直観主義数学で基本となる概念が「証明」であることだ。古典数学でも「証明」は基本のように思うかもしれないが、古典数学では数学の命題が「証明できるかどうか」とは独立に「真偽」が決まっていて、証明は真偽を確立する手段である。例えば、

命題P「4以上の偶数は2つの素数の和でかならず書ける」

は今のところ証明も反証もないが、真か偽かのどちらかであることは決まっていると考える。

一方、直観主義数学では、命題Pは証明も反証も未だないので、命題Pの真偽は定まっていないと考える。というより、人間が行う証明という活動を離れた命題の真偽というものは意味がないのである。しかし、直観主義数学の証明とはそもそも何か、疑問に思うかもしれない。答えは「直観主義数学においては、証明は命題を意味づけるプリミティブな概念である」というものである。もう少し詳しく言うと、例えばITTでは命題を一般化した「判断」とその証明は相互再帰的に定義される。

そうすると排中律

PまたはPではない

が真でないことが(すくなくとも素直に「または」を解釈する限り)分かる。上の命題が真であるのは、Pが真であるか、「Pでない」が真であるかのどちらかである。しかし、Pの証明もPの反証も知られていない。よって、上の排中律は真ではない。実は純粋に論理的な部分だけに限って言うと、直観主義数学の論理は古典論理から排中律を除いたものになっている

直観主義数学はそんなに弱くない

しかし、排中律が成り立たないとすると、直観主義数学はとても証明能力が弱い数学ではないだろうか。というのも、排中律は背理法を成り立たせるために必要で、背理法は頻繁に数学の中で使われるからだ。

しかし、実はそうでもない。否定による解釈というものが知られていて、古典論理で証明可能な命題Pをある別の命題P’に翻訳すると、P’が直観主義の論理で証明できる。否定による解釈はたくさんのバリエーションがあるが、ここではゲーデルが考えたものを紹介する。

  • 原子命題(「ならば」などの論理結合子を含まない、それ以上分析できない文)pを二重否定文\neg \neg pに置き換える
  • または「a \lor b」を「\neg (\neg a \land \neg b)」に置き換える
  • 存在する「\exists xA(x)」を「\neg \forall \neg xA(x)」に置き換える

こうすると、解釈の前の命題が古典論理で証明できれば、解釈の後の命題は直観主義論理で証明できる。

特に、算術(自然数についての形式的な体系のことを数理論理学ではこう呼ぶ)では、証明は複雑なので略すが、原子命題について\neg \neg p \to pが成り立つ。直観主義論理ではp \to \neg \neg pが成り立つので、算術では原子命題についてはp\neg \neg pが等価である。よって実際には、上の解釈は単に「または」と「存在」を解釈し直したものとなる。また、算術の公理系には「または」や「存在」は明示的には含まれていない。よって、算術の公理に否定による解釈をほどこしても、やはり算術の公理になっている。

結局何がわかったかというと、Aが算術の古典論理による定理だとすると、Aの否定による解釈A’は算術の直観主義論理による定理になっている。A’はAと古典論理のなかでは等価であることに注意しよう。つまり、算術の範囲では、直観主義数学は古典数学と等価で、むしろそこにより細かい区別(構成的な選言と存在)を持ち込んだとみなすことができる。

同様の操作は高階の算術についても成り立つので、いわゆる19世紀的な古典的数学は直観主義数学で問題なくコードできる。(9/27追記:嘘です。)

ただし、20世紀的な集合論に基づく数学は、このような操作は少なくともそのままではうまくいかない。というのも、公理に存在「∃」が含まれているからだ。このあたりうまく行かせることはできないか、面白い研究テーマだと思う。

更に興味のある人は

直観主義数学の基本的な考え方は

  • Per Martin-Löf, On the meanings of the logical constants and the justifications of the logical laws
  • Per Martin-Löf, Intuitionistic type theory

を。後者は直観主義的型理論の解説でもある。

否定による解釈は論理学の教科書ならば載っていることが多いが、例えば

集合論の直観主義数学による解釈については

  • Peter Aczel, The type theoretic interpretation of constructive set theory

ZFの構成的バージョンであるCZFがITTで解釈できることを示している。CZFに排中律を加えるとZFになることも示しており、CZFの中で排中律がどこまで解釈できるか研究すると興味があるかもしれない。

直観主義数学の計算機科学への応用については

とか良い?