数学基礎論 p.30〜p.35あたり

1章のハイライトのひとつ、定理1.4.14(コンパクト性定理)の証明についてコメントする。

まず、P.30の初めにある『1階論理のトートロジー』の定義であるが、よく理解できなかったので、ちょっと調べてみるとその採用した体系によって若干異なる定義があり、またおそらく誤って、どんな構造に対しても成立する閉論理式というようなものもあった。印象としてはあまりポピュラーなものではなさそうという感じである。


実際によくわからなかったのは、1階論理の素論理式の定義である。もちろん定義はテキストにあるようにシンプルなもので、『原子論理式か∃,∀で始まる論理式』である。しかし、この定義からでは、いつ2つの素論理式を同じものとみなさなくてはならないかがはっきり理解できなかったのである。具体的にいうと ∀xP(x)と∀yP(y)は同じ素論理式であろうか? 同じ素論理式に対する付値は同じでなければならないため、これは肝心な点である。結論からいうと、これらは異なる素論理式である。素論理式が同じであるとはセマンティクスからではなくて、シンタックスで同じつまり、記号並びが完全に同一な時だけであるというのが正しい解釈である。


すると ∀xP(x)→∀yP(y) ですら『1階論理のトートロジー』になっていないということになる。これで大丈夫かいなというのが第一感であるが、というのは、補題1.4.13が述べていることは、(Tを拡大しておいて)命題論理として充足可能なとき、それを拡張して1階論理としてのTのモデルを作ることができるということであり、もし、最初の付値がセマンティカルに同じ素論理式に違う値を割りつけていたなら、このような拡張は不可能である。\mathcal{M}\mid =\varphi\Leftrightarrow \nu(\varphi)=1が成り立つようにしたくとも、左辺はセマンティカルに同じ素論理式では同じ値を取るからである。


しかし、いったい補題1.4.13の証明のどこにそれを保証する部分があったのだろうか? 


証明を反省してみると Henkin公理と量化公理が手品のタネであることがわかる。実際のところは 論理式\varphiを素論理式に分解して、分解が∃,∀のところで止まったら、付値νの1,0に応じて、その束縛変数を任意の閉式やHenkin定数を置きかえることで、∃,∀を消去して、さらに素論理式への分解を進めていくということで帰納的に証明している。その分解の過程で、付値の割り当てが(セマンティカルに)整合しているかが先の疑問なのだが、具体的に言うと、


1) ν(∃xP(x))=1 ⇔ ある定数cについて ν(P(c))=1

2) ν(∃xP(x))=0 ⇔ すべての閉式tについて ν(P(t))=0

3) ν(∀xP(x))=1 ⇔ すべての閉式tについて ν(P(t))=1

4) ν(∀xP(x))=0 ⇔ ある定数cについて ν(P(c))=0


が成立しているか、ということである。


1)についてはテキストの証明中にある。
2)の右向きの証明は、右辺を否定すると、ある閉式tが存在して、ν(P(t))=1 となるが、量化公理 P(t)→∃xP(x) に対して ν(P(t)→∃xP(x))=1 であるため、ν(∃xP(x))=1が出て矛盾である。
2)の左向きは、左辺を否定して、ν(∃xP(x))=1とすると1) の右辺と2)の右辺とで矛盾がでる。

3)の右向きは、量化公理 ∀xP(x)→P(t)に対して、ν(∀xP(x)→P(t))=1なのでただちに出る。
3)の左向きは、Henkin公理 P(C_{\exists x\neg P(x)})→∀xP(x) に対して、ν(P(C_{\exists x\neg P(x)})→∀xP(x))=1 より従う。

4)の右向きは、ν(P(C_{\exists x\neg P(x)})→∀xP(x))=1 より ν(P(C_{\exists x\neg P(x)}))=1 となる。
4)の左向きは、左辺を否定すると、4)の右辺と3)の右辺は矛盾する。□


というわけで、νの存在だけでほとんど終わっているという感があり、命題論理と1階述語論理の差はどこにあるんだろう?という疑問も湧いてくる。しかし、それはきっと完全性の部分にちがいない...