無矛盾な体系で 0=1 を導出する方法
テッド・チャンは私の好きなSF作家の一人で、短編集「あなたの人生の物語」はかなり評価が高いようですが、この短編集の中の「ゼロで割る」は最悪の短編だと思います。これは、自然数論から矛盾が導出できることを発見した女性数学者が精神的な健康を失っていくのを夫の視点から眺める話で、この話において自然数論に矛盾を発見したということは、今まで自分がやってきたことが無価値であることを発見した中年女性の失望（と夫の無理解）のメタファーでしかありません。ここでは、「自然数論が矛盾している」という（フィールズ賞ものの）大ニュースをが単なる不安のメタファーとして矮小化されており、非常に残念な感じがします。
ところで、「矛盾を導出する」とは、自然数論の場合、具体的には「文 『0=1』が定理として証明できる」 ことをさす、というのが分かりやすいのでよく使われます。従って、文 0=1 が導出できれば、その体系は矛盾していることになります。というか、そうチャンは書いていました。でも、本当にそうなのでしょうか。
いや、もちろん0=1 が（正しい意味で）導出できればその体系は矛盾しているのですが、でも見かけ上、無矛盾な算術の体系で0=1 が導出されることも起こりえます。本エントリーでは、それをご紹介したいと思います。
PA+ ¬Con(PA)のモデル
さて、枠組みとしては ペアノ算術(PA)を採用します。とりあえず、出発点としてPAが無矛盾である*1と仮定しましょう。そして Con(PA) で「PAは無矛盾である」という文を表します。ご存知のように、第二不完全性定理より、PAから Con(PA) を証明することも、その否定 ¬Con(PA) を証明することもできません。つまり、言い換えれば、（PAが無矛盾なので）理論 PA を拡張して PA+ Con(PA)を考えても、PA+ ¬Con(PA) を考えても、どちらも無矛盾であるということです。両方とも無矛盾であるので、当然モデルを持ちます。前者、PA+ Con(PA)のモデル M0として、いわゆる標準モデルを取ることが可能です。
それでは、後者 PA+ ¬Con(PA) のモデル M1 の中では、何が起きているのでしょうか。それを知るために、Con(PA)という文が何を意味しているのかを復習しましょう。
Con(PA)とは、当たり前ですが、「どんなPAの証明も、最終的に『0=1』という結論を導かない」という意味です。PAで証明を扱うためには、論理式も証明も全てゲーデル数化をつかって自然数にコードします。従って、Con(PA)は「どんな自然数 n をとってきても、n が PA の証明のコードであれば、nで表現される証明の結論は文『0=1』ではない」という文章になります。従って、 ¬Con(PA) の意味は、「ある自然数 m が存在し、m はあるPAの証明をゲーデル数化によってコードしたものであり、その証明はPAの公理から出発して、PAと古典論理によって許された式変形のみを行い、最終的に『0=1』という結論を導く」という意味のはずです。
で、ちょっと待てと、M1（PA+ ¬Con(PA)のモデル）では、 ¬Con(PA)を仮定している以上、「0=1」という文を結論として導く証明（とそれをコード化した自然数 m)が存在しているじゃないか。このことはPAが無矛盾であることと矛盾しないのか、少なくとも PA+ ¬Con(PA) が無矛盾であるという不完全性定理の結果と矛盾していないのだろうか、という点が疑問として出てきます。
「0=1」に至る「無限の長さの」証明
まず、M1 の中の「0=1」という結論に至る証明は、M0 の中では証明として認められないだろう、ということに注意してください。M0では、仮定Con(PA)より、「0=1」に至る証明を表現するような自然数が存在しないからです。つまり標準モデルM0の中に、M1における自然数 m が存在しない、つまり m は超準的自然数であると考えることができます。平たくいえば、m はM0の意味では「無限に大きい」自然数である*2、つまり任意のM0の自然数 x はM1の自然数でもある（と見なせる／というかM0の自然数はM1に埋め込める）が、M1において x
- それぞれの証明では、有限個の仮定から有限個の結論を導出することになっているが、M1では「超凖数個（M0の意味では無限個の）の仮定から結論を導出してよい」
- それぞれの証明では、証明の長さは有限だということになっているが、M1では「超準数の長さの証明」（M0の意味では無限の長さの証明）も許される。
という点です。つまり、M1は、M0の意味での無限の長さ（証明ステップ数）と幅（仮定の数）の証明を許すため、M1の算術はM0より証明力が格段に跳ね上がり、従ってM0では証明できなかった「0=1」という文まで証明できるようになってしまったということになります。
そして、このM1のアホみたいに強い証明力は、PAの公理系が保証するものではありません。PAは¬Con(PA)を証明できない、ということをPAが証明しているからです。この意味でPA+ ¬Con(PA)はPAより本質的に証明力が強くなっています。
言い換えると、
- PAをメタ理論としたとき「体系 PA が文『0=1』を導出する」ということを証明できません（PA が矛盾することはPAでは示せません：不完全性定理）。
- そして、PAをメタ理論にしたとき（PAの標準モデルの中では）、「体系 PA+ ¬Con(PA) が存在を認めるPAの公理から始まり文『0=1』に至る証明」はPAの意味で証明ではない（標準モデルの意味で長さが無限になってしまう）ので、PA+ ¬Con(PA)が(PAの意味で)矛盾を導出したとはいえず、従ってPAの意味でPA+ ¬Con(PA)は無矛盾であるということになります*3。
- ですが、PA+ ¬Con(PA)をメタ理論とすれば（PA+ ¬Con(PA)のモデルの中では）、PAの公理から始まり文「0=1」に至る証明が存在することがいえます。つまりPA+ ¬Con(PA)をメタ理論とすればPAは矛盾しています。当然 PA+ ¬Con(PA) をメタ理論とすれば PA+ ¬Con(PA) も矛盾していることになります。
・・・えーと、書いている方も混乱してきました。間違っている点をご指摘いただければ幸いです。
証明の長さと矛盾の導出
さて、PA+ ¬Con(PA)のモデルM1では、（標準的自然数の意味で）有限の長さと幅の証明では矛盾を証明することはできません。Woodinの言葉を借りれば、M1の中の世界の住人は、Turing Machineをずっと動かしていても、「0=1」という文を導出することはできないわけです。人間には、超準数（標準モデルの意味で無限）の長さの証明なんて無理ですから、その意味で、たとえ人間がM1の中に住んでいても、その世界で人間が矛盾を導出することはできないことになります。ある意味、算術の体系が無矛盾である必要はなく、矛盾が導出されるにしても、その導出が人間に取り扱えないぐらい長ければ、それでいいのではないでしょうか（実効的に無矛盾である、という言い方をしてもいいかもしれません）。
そう考えたのがParikhです。彼は、PAを拡張して、砂山のパラドックスについて矛盾の導出を許すものの、非常に長い証明でないと矛盾が導出できない体系を考えました。そのアイディアの元は、確実にPA + ¬Con(PA)のモデルの分析だと思われます。また、Woodinも"Towers of Hanoi"において、似た状況を考察しています。
ところで、モデル M1 の中の仮想的住人についてもうちょっと考えてみましょう。彼（もしくは彼の Turing Machine）は、標準的自然数の長さのステップの証明を行う能力しかないため、このモデルでは¬Con(PA)を証明できることを知らないかもしれません。というか、PAの全ての公理はそのまま保持されているため、通常の日常的な算術を行う上で何の困難も持ちません。その意味で、 彼は、自分の住んでいる世界がPAのモデルであると知っていたとしても、そこが標準モデルか、超準モデルか、区別することはできません。区別するためには
- メタ理論（この場合はZF）の視点を持つ
- （標準モデルの意味で）無限的な、超人的計算能力を持つ
などの能力が必要となります。そして、標準数と超準数の区別ができないという意味で、不完全性定理は、有限概念について深刻な問題をもたらします。
「無矛盾性」という言明のレベルの違い
この議論では最初に「PAが無矛盾である」と仮定し、一方でM1では ¬Con(PA) が成立するモデルM1を考えました。このことは、素朴な言い方をすれば、 「PAが無矛盾である」という言明と Con(PA) という言明のレベルの違いを強調します。
今回の話の定式化では、「PAが無矛盾である」という言明は、メタ理論的な言明であり、構文論的な（もしくは特定のモデルを超えた）性質です。一方、 ¬Con(PA) の方は、モデル相対的な、特定のモデルに関する性質です。その意味で、「PAが無矛盾である」は真／偽の範疇ではない（PAの公理が真／偽の範疇を超えた存在であるように）ですが、 Con(PA)は真理値を付加することができる存在です。
話がここで終わればいいのですが、話はもっとややこしくできます。PAの特定のモデル M でPAを解釈することを考えると、そのレベルでは「PAが無矛盾である」という言明は Con(PA) として解釈され、解釈された文には（Mの意味で）真理値も付加できます。さらに M の中で、算術的にPAのモデルを構成することができます。つまり、例えばPA+Con(PA)のモデルをMの内部で構成できるわけで・・・と、上記の話をそっくり繰り返すことができます。このように、算術化のおかげで、どのレベルで（何をメタ理論として、どのモデルの中で）何を議論しているのかが分かりにくくなるのが算術の怖さです。
よく、不完全性定理について、「ゲーデルは明らかに真なのに証明できない命題があることを証明した」という人がいます。彼らは、真だが証明できない命題の例として「PAは無矛盾である」をあげます。しかし、この言い方は上の例（くどいようですが、M1はPAのモデルであり、そしてM1では ¬Con(PA) は真ですが、しかしメタの意味ではPAは矛盾していません）に照らせば、非常に問題のある言い方であるということができるのではないでしょうか。そして、どのような枠組みで議論しているかを問うことなしに、例えば「言明『体系が無矛盾である』が真である」と主張するのは無意味です。
超準数と巨大基数
今までPAの話をしてきましたが、では他の理論、例えばZFに関してはどうでしょうか。ZFに対して、Con(ZF)に相当するのが巨大基数の存在公理です。自然数論の場合、超準モデルは「病的なもの」として嫌われる傾向がありますが、ZFの巨大基数論は集合論の華であり、それを排除することは許されないと思う人も多いでしょう。その意味で、同じ不完全性に起因する現象なのに、この扱いの差をうらやましく思います。この原因は、
- 我々は、自然数とは何かということを知っていると思い込んでいる
- が、高次無限に関してはまだ謙虚さを保っている
ではないかと思うこともあります。
メタ論理的言明と有限性
さて、今回の結果は、「ある体系Tが文Aを証明する」というとき、「有限性」という概念が、いかに本質的な役割を果たしているかということを示唆します。しかし一方で、一部の哲学者（クリスピン・ライトなど）は、公理と推論規則を定めれば、論理的帰結関係はそれから自動的に定まるかのように語っています*4。
われわれが古典命題論理を用いてAからBを導くとき、BはAを受け入れることに基づいて条件的に証明されているといわれるかもしれない。さらに
は古典命題論理の受け入れに基づいて条件的に証明されているのであるといわれるのかもしれない。しかし、
は、いささかも条件的ではなく証明されているのである。ここに登場する一連の操作、すなわち、ある論理体系が実際に特定の前提から特定の帰結を導くだけの材料を提供しているということの証明として受け取られるような一連の操作は、完全な現象学的説得力を持ちうる
で、「現象学的説得力」の意味ですが、松坂氏の解説によれば
「
だそうです。しかし、不完全性定理を巡る議論は、このような証明可能性関係が、メタ論理的操作を行う場面での「有限概念」（上の例ではどのモデルの中で操作を行うか）に強く依存していることを示唆します。
この意味で、ライトの主張は、間違いとは言いませんが、大きな要素（有限性などに関するメタの立場）を無視しており、不十分であるかのようにも見えます。なんといっても、「有限性」という概念が議論の余地なく明白であるとか、メタの立場を定めたときに明白に一つ同定できるとかいうのなら、別に言及する必要はないのですが、そうとはいえない（帰納的公理化可能という条件がある限り、理論のレベルでは超準数を排除できない）というのが不完全性定理の帰結であるからです。つまり、「メタ理論的操作を行う」場面における有限概念とは何かを巡っては深刻な困難があるように見えることが理由です。
テッド・チャンの「矛盾の導出」
さて、テッド・チャンの短編のなかの「0=1」に至る証明がどういうものか分かりません。二枚の紙に一分で書ききることができるらしいですが。
もちろん、M1での「無限の長さ」の証明を、人間が書ききる訳にはいきませんが、しかし、実際の数学の多くの分野の証明では、証明の構成法だけを与えて、実際に全て記号で書ききるなんてことをしないことが多いこともたしかです。もしかしたら、こういうタイプの証明で、もしかしたら自然数論が矛盾していることではなく、超準数が存在することを証明しただけかもしれません。
