§E16.12項モデルと完全性定理

証明. 等号公理の反射律から$T^H\vdash t=t$なので、$t\sim t$である。§E16.10 補題 4.1により、$t\sim u$なら$u\sim t$であり、$t\sim u$かつ$u\sim v$なら$t\sim v$である。したがって$\sim$は同値関係である。

$f$を$n$項関数記号とし、各$t_i\sim u_i$を仮定する。定義により$T^H\vdash t_i=u_i$である。有限個の等式を命題論理の派生則によって連言にまとめ、関数合同公理

へ modus ponens を適用すると、$T^H\vdash f(\bar t)=f(\bar u)$を得る。$n=0$では前件が空の連言であり、結論は同じ零項関数記号が表す閉項の反射的等式である。

$R$を$n$項関係記号とする。同じ連言と関係合同公理から

を得る。双条件の二方向と modus ponens により、一方が導出可能なら他方も導出可能である。$n=0$では公理は同じ零項関係$R$と自身の双条件を述べるので、同じ結論が成り立つ。以上はすべての有限$n$に対する個別の公理スキーマに基づいており、二項演算だけの商降下には依存しない。▨

証明.$r$の構造に関する帰納法を用いる。$r=x$なら、左辺は定義により$s_\tau(x)=[\tau(x)]$であり、右辺と一致する。$r$が定数記号なら、両辺はその定数の同値類である。

$r=f(r_1,\ldots,r_n)$とする。帰納法の仮定と項モデルの関数解釈により

$n=0$の場合も第2行が零項関数の定義そのものである。▨

証明.$\varphi$の構造に関する帰納法を用いる。

$\varphi$が$r=u$なら、補題 2.2と商集合の等号から

を得る。$\varphi=R(r_1,\ldots,r_n)$の場合も、項評価補題と関係の定義から

を得る。$n=0$も同じ定義に含まれる。

$\varphi=\neg\psi$とする。帰納法の仮定と極大無矛盾性により

最後の同値は§E16.11 補題 5.3 (1)と§E16.11 補題 5.3 (2)による。

$\varphi=\psi\to\chi$とする。含意の意味と二つの帰納法の仮定により、左辺が真であることは$T^H\nvdash\psi[\tau]$または$T^H\vdash\chi[\tau]$と同値である。§E16.11 補題 5.3 (1)と§E16.11 補題 5.3 (3)により、同じ条件は$T^H\vdash\psi[\tau]\to\chi[\tau]$と同値である。

$\varphi=\forall x\psi$とする。束縛変数を必要ならアルファ変換し、$x$が$\tau$で代入する閉項に現れないようにする。$x$以外の自由変数を$\tau$で置き換えた論理式を$\theta(x)$と書く。まず$T^H\vdash\forall x\theta(x)$とする。任意の閉項$t$について全称具体化の公理 (Q1) から$T^H\vdash\theta(t)$である。帰納法の仮定により、$M_{T^H},s_\tau[x\mapsto[t]]\models\psi$である。項モデルの各要素に対して、その要素を同値類として表す閉項$t$が存在するので、$M_{T^H},s_\tau\models\forall x\psi$を得る。

逆に$M_{T^H},s_\tau\models\forall x\psi$とする。任意の閉項$t$について帰納法の仮定から$T^H\vdash\theta(t)$である。$T^H\nvdash\forall x\theta(x)$と仮定する。極大無矛盾性により$T^H\vdash\neg\forall x\theta(x)$であり、量化子の否定に関する派生同値から$T^H\vdash\exists x\neg\theta(x)$を得る。 Henkin 性により、Henkin 定数$c$が存在して

となる。modus ponens により$T^H\vdash\neg\theta(c)$となるが、全閉項の場合から$T^H\vdash\theta(c)$でもある。$\theta(c)$とその否定の二つの導出は$T^H$の無矛盾性に反する。したがって$T^H\vdash\forall x\theta(x)$である。

存在量化子は$\exists x\psi:=\neg\forall x\neg\psi$と定義されるため、以上の帰納法にすでに含まれる。証人の対応を直接確認すると、$T^H\vdash\exists x\theta(x)$なら Henkin 性により、$T^H\vdash\theta(c)$を満たす閉項$c$が存在する。帰納法の仮定から$[c]$が意味論的な証人になる。逆に意味論的な証人$[t]$が存在すれば、帰納法の仮定から$T^H\vdash\theta(t)$であり、存在量化子導入の派生則から$T^H\vdash\exists x\theta(x)$となる。

以上で原始結合子のすべての場合を処理した。有限変数表示では、$s(x_i)=[t_i]$となる閉項割当て$\tau$を選び、残りの変数へ一つの固定閉項を割り当てる。§E16.6 定理 4.1により、$s$と$s_\tau$の$FV(\varphi)$外での違いは真理値を変えない。▨

証明.§E16.11 定理 6.1により$T$を極大無矛盾な Henkin 理論$T^H$へ拡大し、定義 2.1の項モデル$M_{T^H}$を作る。$\sigma\in T^H$は文なので、真理補題で代入する自由変数は無い。§E16.11 補題 5.3の導出閉包と補題 3.1により

である。したがって$M_{T^H}\models T^H$であり、特に$M_{T^H}\models T$である。厳密には$M_{T^H}$は拡大言語の構造なので、元の言語$L$への還元を$M$とすれば$M\models T$である。

§E16.11 系 2.2により$L^H$の閉項集合は高々$\kappa(L,T)$個である。項モデルの台集合はその商なので$|M|=|M_{T^H}|\le\kappa(L,T)$である。▨

証明. モデルをもつ理論が無矛盾であることは健全性から従う。無矛盾な理論がモデルをもつことは定理 4.1で証明した。▨

証明.$T\cup\{\neg\varphi\}$が矛盾すると仮定する。演繹定理により$T\vdash\neg\varphi\to\bot$である。古典命題論理では$(\neg\varphi\to\bot)\to\varphi$を導出することができるので、modus ponens により$T\vdash\varphi$となり、$T\nvdash\varphi$という仮定に反する。▨

証明.$T\vdash\varphi$なら、一階 Hilbert 系の健全性により$T\models\varphi$である。

逆向きの対偶を示す。$T\nvdash\varphi$とする。補題 5.1により$T\cup\{\neg\varphi\}$は構文的に無矛盾である。定理 4.1を適用すると、ある$L$構造$M$が存在して

となる。したがって$M\models T$かつ$M\not\models\varphi$であり、$T\not\models\varphi$である。対偶により$T\models\varphi$なら$T\vdash\varphi$である。▨