第２不完全性定理

新井先生の本p.110によれば、第２不完全性定理を証明するために使う事実は、
・不動点定理
・標準的な証明可能性述語
だけで、第１不完全性定理に比べると、そんなに多くない。
この二つが成り立つ任意の公理系で第２不完全性定理は成り立つので、ＺＦやＺＦＣでも成り立つ。

公理系Ｔを与えておく。

不動点定理

任意の一変数論理式φ[v]に対して、閉論理式Ｆが存在して、
　　　

ただし、φの中身はＦのゲーデル数（のＴにおける数項）を表している。

不動点定理はどんな公理系でも成り立つわけではなく、教科書ではＰＡにおける不動点定理を扱っている。原始再帰的関数とそのコードの関係を使った証明。

証明可能性述語Ｐｒ

φ，ψを任意の論理式とする
（Ｄ１）
　　
（Ｄ２）
　　
（Ｄ３）
　　

　公理系Ｔで「φはＴで証明可能である」を意味する証明可能性述語Pr(φ)が上の三条件を満たしている時、Prは標準的な証明可能述語といい、これらから第二不完全性定理を証明できる。

第２不完全性定理の証明

では、証明の中で実際にどのようにして不動点定理と証明可能述語が使われているかをp.109に従ってまとめます。

　　　第２不完全性定理
証明体系Ｈを含む公理系Ｔで、不動点定理と(Ｄ１)、(Ｄ２)、(Ｄ３)が成立するとする。

Ｔが無矛盾ならば、
　　　　　　　　　　
ただし、Con(T)はＴの無矛盾性を意味する論理式で、Fmlを論理式の集合とすると、
　　　　

（証明）
はじめに不動点定理により、ゲーデル文Ｇをつくる。
閉論理式Ｇを、
　　　　　…（１）
により定義する。

このとき、Ｔが無矛盾であれば、
　　　　　…(２)
となる。

このことは背理法により示せる。使う性質は（Ｄ１）。
　　　　（Ｄ１）
　　 　　（Ｇの定義より）
上の二つから、
　　　　…（３）
であるので、ＧがＴで証明可能であるとするとＴは矛盾してしまう。
以上で（１）の証明終わり。

ところで、（３）をＴの中に形式化したものは、
　　　　…（４）
であるが、これは（１）の証明に（Ｄ３）をはさむと導出できる。

さらに、
　　　　…（５）
が、どんな論理式についても成り立つことが、（Ｄ１）と（Ｄ２）とＴ|- Con(Ｔ)を使って導ける。

（５）の証明：
　　　　（トートロジー）
　　　　（¬記号で書き換えた）
　　　　（Ｄ１）
と、Ｔ|- Con(Ｔ)の仮定から
　　
を合わせて、
　　
あとは、（Ｄ２）から
　　
が任意の論理式に対して言えるので、その対偶を考えることで、
　　
よって、
　　
(５)が導かれた。

（４）と（５）から、
　　
であり、
否定記号¬は、¬φ:≡φ→⊥の略記であったので、
　　
となる。

したがってＧの定義より、
　　
となり、（２）に反する！！！

と、証明を書き下してみたものの

ちょっとアヤシイな。
この証明では、Ｔ|- Con(Ｔ)の仮定が、論理式に⊥を入れたものしか使っていない。
つまりCon(Ｔ)としては、
　　¬Pr(⊥)
を準備すれば十分だったことになります。
まぁ実際、Ｔの無矛盾性を意味する論理式は、述語Ｐｒさえしっかりと定義できていれば、「無矛盾ならば少なくとも一つ証明できいない論理式がある」ので、たとえば「⊥」を使っちゃえばいい。ということなんでしょうかね。

上で定義したCon(Ｔ)は教科書通り書き写したものです。
しかし、これは正式には論理式ではなく、第一不完全性定理からの流れで、原始再帰的述語から写された論理式の省略形でした。第一不完全性定理にこだわらなければ、Con(Ｔ)はけっこう簡単に書いてしまってかまわない、ということなのかもしれませんね。