【ゲーデル】クライゼルの注意に注意【不完全性定理】

作者:昭二, 前原
朝倉書店

不完全性定理というのはもちろん哲学的にも興味深い定理だと思う*1。不完全性定理に関連して哲学の文脈でよく聴く（気がする）のがクライゼルの注意というやつで、前原基礎論にも解説が載っていた。前原先生曰く

　わたくしは、局所的な意味においては、クライゼルによるこの注意を評価しない。けれども、論理式による命題の表現法が明々白々に確定しているわけではない、という一般的視野に立てば、これは、やはり重要かつ適切な注意である、と思っている。（163ページ）

とのこと。この意味を考えてみたい。

第二不完全性定理とは！？クライゼルの注意とは！？

　第二不完全性定理とは「何とかかんとかの条件を満す形式体系*2が無矛盾ならば自身の無矛盾性を証明できない」というような定理だが、クライゼルの注意によると、場合によっては無矛盾性を証明できてしまうように見えることがある。

　前原基礎論では体系*3 $K$ の無矛盾性を表現する論理式はこうなる。

　 $\lnot \exists x [{\rm {\bf Bew}}_K(x) \land {\rm {\bf Bew}}_K({\rm {\bf Neg}}(x))]$

${\rm {\bf Bew}}_K(x)$ というのは（ゲーデル数） $x$ （の論理式）は $K$ で証明できるということを意味する（しかしそれを意味する述語を数値別に表現した形式内の述語を使っているというわけではない）。 ${\rm {\bf Neg}}(x)$ は（ゲーデル数） $x$ （の論理式）に否定をつけた論理式（のゲーデル数）である。これは、それ自身もその否定も証明できるような論理式は存在しないという意味と解釈でき、 $K$ の無矛盾性を定義通りに表現した論理式に見える。これが $K$ で証明できないということなのだが、これはこうしても良い。

　 $\lnot {\rm {\bf Bew}}_K({\bf \lceil 1 = 0 \rceil})$

${\bf \lceil 1 = 0 \rceil}$ というのは $1 = 0$ を表す論理式のゲーデル数の（いわゆる）数項である。これも証明できない。つまり、何らかの証明できない論理式があるということを表していて、それが証明できないということを証明できない、みたいな。矛盾した体系からはどんな論理式も証明できるので、証明できない論理式があるということは体系は矛盾していないということになる。なので何らかの証明できない論理式の存在を表す論理式もまた無矛盾性を表現しているように見える。

　しかし以下は証明できてしまう。

　 $\lnot {\rm {\bf Bew}}_K^*({\bf \lceil 1 = 0 \rceil})$

${\rm {\bf Bew}}_K^*$ はロッサー述語というやつである。これが何を表現しているのかということが問題なのである。トゥイッターで木原先生がいろいろ述べているのを発見した。

togetter.com

クライゼルの注意で「無矛盾性を表す文」とされているものは全然無矛盾性を表しちゃいないんじゃないか、とのことである。

考察

　 ${\rm {\bf Bew}}_K^*(x)$ は、「ゲーデル数 $x$ の論理式は証明でき、その否定の証明のゲーデル数はその証明のゲーデル数以下の数にはない」というような意味となる。これの否定を考えてみると、クライゼルの注意で無矛盾性を表すとされる文の意味は木原先生の仰る「自分は無矛盾である or 矛盾も無矛盾も証明するが無矛盾の証明の方が簡単」というようなものとなる。

　ロッサー述語は、 $K$ が無矛盾であればゲーデルの述語と同値になる。無矛盾ならば証明できる論理式の否定の証明は存在しないので。そう考えるとクライゼルの注意は無矛盾性が証明できているようにも思える。

　しかし形式体系内では同値にならない（ $K$ が無矛盾ならば同値性を証明できないことが証明できる）。これは不完全性定理の帰結である。ここが味噌ではなかろうか。「 $K$ が無矛盾ならば」という条件は形式体系の内部では証明できない。これは第二不完全性定理の主張である。ということは $K$ の内部では「無矛盾性を表現した文」ではなくなる。そんな感じじゃなかろうか。

　数学的な言明の論理式による表現というのを恣意的に解さず、数値別に表現する論理式に限ってしまうとどうか。しかし ${\rm {\bf Bew}}_K(x)$ も ${\rm {\bf Bew}}_K^*(x)$ も証明可能性の数値別表現になっていない。これは第一不完全性定理の主張の一部である。なんか上手く出来ている。

まとめ的な

　木原先生が仰るように、クライゼルの注意はそのまま「無矛盾性を表す文が証明できる」と解せるようなものではない。しかし前原先生の仰るように無矛盾性の表現や解釈はいろいろだということを示唆している。その際に不完全性定理への理解が重要となる。

　無矛盾性証明というのはヒルベルト・プログラム以来の重要概念である。不完全性定理はそれが不可能であることを証明したと俗に言われるが、そもそも「無矛盾性を証明できない」といった時の無矛盾性とか証明とかいうのはメタ数学的言明の形式体系における対応物であって、私はメタとオブジェクトの対応があんまり信じられない人間なので、まああんまり気にすることもないようにも思えてくる。なのでゲンツェンとかダイアレクティカ解釈とかいろいろな無矛盾性の解釈とその正当化を考えるのが重要なのでしょうな*4。そういうターニング・ポイントとして不完全性定理はやはり興味深い。

*1:それ以上に俗流テツガクの格好の題材になってもうてますが…。

*2:ここでは論理式の集合（理論）も含めた意味で使います

*3:これも「理論」と書くべきか。形式体系と論理式の集合を合せたもの

*4:と思うのだけれど無矛盾性証明の解釈はいろいろあれど無矛盾性の解釈を変更することってあるんスかね。ゲンツェンはそんなことしていないと思うけどダイアレクティカ解釈については何も知りません。