日々の流転

λ. 整礎性は一階述語論理では表現できないのね

先日、ヘンキン文 - ヒビルテ (2007-09-16) で、「Xが証明可能であることを□Xと書くと、証明可能性を様相論理で扱える」ということに触れた。これが Löb Logic と呼ばれる論理で、□(□φ→φ)→□φ という公理図式(axiom schema)を持っていて、PAでの証明可能性をある意味で忠実に反映した体系になっている。 それで、この論理をSPASSで扱って遊べないかと思ったのだけど、ちょっといじっているうちに、出来ないということに気付いた。しょぼーん。以下にその理由を簡単に書く。

SPASSはあくまで一階述語論理の定理証明機なので、□(□φ→φ)→□φ のような様相論理の公理図式は、クリプキ構造に関する一階述語論理の公理で表現してやる必要がある。 そして、□(□φ→φ)→□φ はクリプキ構造の到達可能性関係が推移的かつ整礎(well-founded)であることに対応することが知られている。 で、推移性は何の問題もないのだけど、問題は整礎性。

関係Rの整礎性は「空でない部分集合にはRに関する極小元が存在する」こと、もしくは「x0 R x1 R x2 R … という無限列が存在しない」ことによって定義される*1。 前者の定義では集合を量化する必要があるけど、一階述語論理では個体しか量化できず、集合を量化出来ないのだった。二階論理なら ∀P. (∃x. P(x)) → (∃x. P(x) ∧ ∀y. P(y)→¬R(x,y)) と書けるんだけどね。後者の定義も同様に一階述語論理では書けない。