"The tower of Hanoi" W. Hugh Woodin

論文 logic 哲学

in: Truth in Mathematics, p.329-351. Oxford science publications, 1998.
ここ一週間読んでいるのだが、この結果についてどう考えたらいいのか、全然わからない。このエントリーも何回書き直していることか。

Godelのincompleteness theoremより、 ペアノ算術PAにおいて、例えば not con(PA)（PAは矛盾している!）という文はPAから独立である。だから PA+ not con(PA)を仮定しても矛盾ではない、つまり PA+ not con(PA)のモデルMが存在する。not con(PA)とは、構成の仕方を考えると、「ある証明が存在して、矛盾した式 "0=1"が証明できる」という内容の文章である。ということはMはPAのモデルであり、なおかつ矛盾した式 "0=1"にいたる証明が存在することになる。それではその「証明」とはどのようなものだろうか。
答えは、Mのなかでは「超準的な自然数」dが存在するというものである。「超準的な自然数」とは、一応（Mの中的な意味では）自然数なのだが、他の「標準的な」自然数（0,1,2,3,4,…）すべてよりも大きい。そしてMの中の "0=1"にいたる証明の長さはdとなる。つまり、Mの中の "0=1"にいたる証明の長さは、自然数の「標準モデル」の中の意味では無限の長さとなってしまう。もちろん標準モデルの内部で"0=1"を証明することはできない。
つまり、もし標準モデルの中のTuring machine T に"0=1"の証明を計算させたとすると永遠に停止しない（が、M内の視点からすれば「有限」ステップで"0=1"を出力し停止する）。


さてWoodinは、非常に弱い集合論の体系T_0上で、ある整数kに対しGodel likeな文Ω_kを構成でき、

  1. 論理式Ω_kは「kは整数で、かつ長さが10^24kより短い証明で"not Ω_k"が証明できる」ことを主張し、
  2. また"Ω_k"は「"not Ω_k"の証明 p は"reasonableな"transitive model の元となる（この意味でreasonableである）」ことも主張する

が成立することを示した。Ω_kを仮定しても not Ω_k を仮定しても結論としてnot Ω_k が出てくる。実際、not Ω_kはすべてのT_0のモデルで真であり、つまりT_0から証明可能となる。そしてnot Ω_kの証明がすべて10^24kより長ければそれで話は終わりである。


もしnot Ω_kの10^24kより短い証明 p が見つかったら大変なことになる。この場合、T_0の立場からはkが整数であることは検証できるし、自然数論も展開できるはずである。しかし10^24kより大きい数を整数として認めると"0=1"を証明してしまうため、整合性を守るため10^24kより大きな整数の存在を認めることはできない。

この場合、10^24kよりずっと大きい自然数（例えばExp_2011(10^24k)とか）は、以下の意味で存在しないということになってしまう。

  1. あるfinite state Turing Machine T" が存在して、T" は停止しない（PAの標準モデルの中で"0=1"を証明できないのと同じ理由）
  2. しかしTの計算ステップ数は決してExp_2011(10^24k)を超えない！（超えたらΩ_kが証明されてしまう！）

ということである。T"の計算ステップ数はもちろんkは超えることができる。
つまりここではkは標準的自然数なのに10^24kが超準的自然数の代わりをすることになる。謎な世界だ。


我々の住む世界は実はnot Ω_kの10^24kより短い証明が存在する世界であると考えても全く矛盾はない。我々は日常10^24kなんて大きな数を使うわけではない。もちろん10^24kなんて長さの証明を全部チェックするわけにはいかない（有名なパズルのハノイの塔が本当に全部移動できるのかやってみるわけにはいかないのと同じだ）。
数学の哲学であればここから「我々は自然数に関して整合的な直観なんて持っていない」と論じる･･･方向に向け鋭意努力する出発点になるのかもしれないようなどうでしょう。エッセニン・ボルピンとか、「大きな自然数は存在しない」ということをいう人は昔から少数ながらいた。彼らのいうことは、ある意味では集合論と整合的であると言えることになる。またWoodin自身のコメントのように、ZF集合論において可測基数などを仮定すると非常にたくさんのことが言えてしまうため、もしかしたら上のpのような証明が構成できてしまうかもしれない！



ついでにお恥ずかしい話だが、Woodinの論文はぱっと見は明快に書かれているようで、とても飛躍が多く、非常にわかりにくい。何がなんだか。誰か、私の上に書いた内容に間違いを見つけて、教えてください。

ちなみにこのWoodin論文のネタはSolovayは"Injecting inconsistencies into models of PA"から来たらしい。PAの中ではなく、集合論の中で遂行することで、証明の見通しがクリアになった･･･らしい。