日々の流転

λ. 不完全性定理に関して混乱中 (2)

不完全性定理に関して混乱中の続き。 かがみさんの「モデルでの真偽」というエントリを読んで、考えてみる。

第二不完全性定理の証明では第一不完全性定理の算術化が必要なので、第一不完全性定理で使う概念は、ω無矛盾性を含めて全て算術化可能なのではないかと思います*1。 Tのω無矛盾性は「任意のnについて T ⊢ P(n) ならば T ⊬ ∃x. ¬P(x)」だから、 provable(x) := ∃y. prove(y,x) と定義すると、 ωCon(T) := ∀[P]. (∀n. provable([P(n)])) → ¬provable([∃x. ¬P(x)]) のような感じで算術化可能なはず(表記は少し誤魔化してるけど)。

そうすると、私の知りたかったことは、大体「M ⊧ T∪{¬G} のとき M ⊧ ¬ωCon(T) や M ⊧ provable([¬ωCon(T)]) は成り立つのか?」になるのかな……

まず、M ⊧ ¬ωCon(T) について考えてみる。 T ⊢ Con(T)→¬provable([G]) と T ⊢ G≡¬provable([G]) から T ⊢ Con(T)→G 。 対偶をとって T ⊢ ¬G→¬Con(T) で、したがって T∪{¬G} ⊢ ¬Con(T) 。 完全性定理から T∪{¬G} の任意のモデルMで M ⊧ ¬Con(T) 。 M ⊧ ¬ωCon(T) だけでなく M ⊧ ¬Con(T) まで成り立つのだな(考えてみればあたりまえだけど)。

次に、M ⊧ provable([¬Con(T)]) について考えてみる。 T∪{¬G} ⊢ ¬Con(T) ということは任意の論理式Aについて T∪{¬G} ⊢ provable([A]) であり、従って T∪{¬G} ⊢ provable([¬Con(T)]) 。ということは、M ⊧ provable([¬Con(T)]) も言える。

結論。Mの中で形式化したTは矛盾している。 そして、矛盾してしまったのは、超自然数に対応する証明図がある分、証明能力が強くなっているため。 疑問は解けたが、なんだか少し不思議な感じがするなぁ。

λ. 世界一の債権国、日本に味方はいない

<URL:http://www.h-yamaguchi.net/2007/03/post_3683.html> より。 後で読む。