完全性定理(命題論理)

まず (A1)〜(A3) の実例はどれも恒真式である。付値 $v$ を任意にとる。

• (A1)：$v(\varphi)=\mathrm{T}$ なら $v(\psi\to\varphi)=\mathrm{T}$ なので、全体は真である。
• (A2)：$v(\varphi\to(\psi\to\chi))=v(\varphi\to\psi)=\mathrm{T}$ とし、$v(\varphi\to\chi)=\mathrm{T}$ を示せばよい。$v(\varphi)=\mathrm{T}$ なら $v(\psi)=\mathrm{T}$ と $v(\psi\to\chi)=\mathrm{T}$ から $v(\chi)=\mathrm{T}$ である。
• (A3)：$v(\lnot\psi\to\lnot\varphi)=v(\lnot\psi\to\varphi)=\mathrm{T}$ で $v(\psi)=\mathrm{F}$ とすると、$v(\lnot\psi)=\mathrm{T}$ から $v(\lnot\varphi)=v(\varphi)=\mathrm{T}$ となって矛盾する。よって $v(\psi)=\mathrm{T}$ である。
  $v$ が $\Gamma$ のすべての元を真にするとき、導出 $\varphi_1,\dots,\varphi_n$ の各行が $v$ で真であることを $i$ に関する帰納法で示す。公理は恒真式、$\Gamma$ の元は仮定により真であり、$\varphi_i$ が $\varphi_j$ と $\varphi_j\to\varphi_i$ から MP で得られるなら、両者が真なので $\varphi_i$ も真である。最後の行 $\varphi$ も真であり、$\Gamma\models\varphi$ である。$\square$

1〜5 は、一階論理の Hilbert 流の体系 $\mathbf H$ について 無矛盾性 の記事が証明している。1 は補題「矛盾からの導出」、2 は命題「証明可能性と無矛盾性」の 1・2、3 は命題「矛盾の言い換え」の 3、4 は定理「Lindenbaum の補題」、5 は命題「極大無矛盾集合の性質」である。
それらの証明で使われているのは、(A1)・(A3) の実例、MP、演繹定理、$\{\lnot\lnot\varphi\}\vdash\varphi$、導出の基本性質（反射性・単調性・有限性・推移性）、Zorn の補題だけである。$\mathbf H_0$ の (A1)〜(A3) は $\mathbf H$ の (A1)〜(A3) と同じ形であり、$\mathbf H_0$ の導出も前の行だけを参照する有限列なので導出の基本性質が成り立つ。演繹定理は上で述べたとおり成り立ち、$\{\lnot\lnot\varphi\}\vdash\varphi$ は Hilbert流の証明体系 の記事の例「二重否定の除去」が $\mathbf H_0$ で導出している。したがって同じ証明が、一階の論理式を命題論理の論理式に読み替えて $\mathbf H_0$ でそのまま通る。$\square$

$\varphi$ の組み立てに関する帰納法で示す。
命題変数 $p$ のときは $v_\Delta$ の定義そのものである。
$\varphi=\lnot\psi$ のとき：
$$ v_\Delta(\lnot\psi)=\mathrm{T}\iff v_\Delta(\psi)=\mathrm{F}\iff\psi\notin\Delta\iff\lnot\psi\in\Delta. $$
2 つ目の同値は帰納法の仮定、3 つ目は lem-pc-tools の 5 (b) による。
$\varphi=\psi\to\chi$ のとき：
$$ v_\Delta(\psi\to\chi)=\mathrm{T}\iff\bigl(v_\Delta(\psi)=\mathrm{F}\text{ または }v_\Delta(\chi)=\mathrm{T}\bigr)\iff\bigl(\psi\notin\Delta\text{ または }\chi\in\Delta\bigr)\iff(\psi\to\chi)\in\Delta. $$
2 つ目の同値は $\psi,\chi$ についての帰納法の仮定、3 つ目は lem-pc-tools の 5 (c) による。$\square$

$\Gamma$ を付値 $v$ が充足するとする。$\Gamma\vdash\varphi$ かつ $\Gamma\vdash\lnot\varphi$ なら、健全性（prop-pc-soundness）により $v(\varphi)=v(\lnot\varphi)=\mathrm{T}$ となり、これは起こらない。よって $\Gamma$ は無矛盾である。
逆に $\Gamma$ が無矛盾なら、lem-pc-tools の 4 により極大無矛盾集合 $\Delta\supset\Gamma$ がある。lem-pc-truth により $v_\Delta$ は $\Delta$ のすべての元を真にするので、とくに $\Gamma$ を充足する。$\square$

$\Rightarrow$ は prop-pc-soundness である。
$\Leftarrow$ を対偶で示す。$\Gamma\vdash\varphi$ でないとする。lem-pc-tools の 2 により $\Gamma\cup\{\lnot\varphi\}$ は無矛盾である。prop-pc-model-existence により、$\Gamma\cup\{\lnot\varphi\}$ を充足する付値 $v$ がある。$v$ は $\Gamma$ のすべての元を真にし、$v(\lnot\varphi)=\mathrm{T}$ なので $v(\varphi)=\mathrm{F}$ である。よって $\Gamma\models\varphi$ ではない。$\square$

$\Delta_v$ は $v$ で充足されるので、prop-pc-model-existence により無矛盾である。$\psi\notin\Delta_v$ なら $v(\lnot\psi)=\mathrm{T}$ で $\lnot\psi\in\Delta_v$ なので、$\Delta_v\cup\{\psi\}$ は $\psi$ と $\lnot\psi$ を含んで矛盾する。よって $\Delta_v$ は極大無矛盾である。
$v_{\Delta_v}(p)=\mathrm{T}\iff p\in\Delta_v\iff v(p)=\mathrm{T}$ なので $v_{\Delta_v}=v$ である。また lem-pc-truth により $\varphi\in\Delta\iff v_\Delta(\varphi)=\mathrm{T}\iff\varphi\in\Delta_{v_\Delta}$ なので $\Delta_{v_\Delta}=\Delta$ である。$\square$

$\Gamma_v:=\{q_1^v,\dots,q_n^v\}$ とおき、$\varphi$ の組み立てに関する帰納法で示す。導出をつなぐときは推移性を断らずに使う。
命題変数． $\varphi=q_i$ なら $\varphi^v=q_i^v\in\Gamma_v$ である。
否定． $\varphi=\lnot\psi$ とする。$v(\psi)=\mathrm{F}$ なら $v(\varphi)=\mathrm{T}$ で、$\varphi^v=\lnot\psi=\psi^v$ である。帰納法の仮定 $\Gamma_v\vdash\psi^v$ がそのまま求める式である。$v(\psi)=\mathrm{T}$ なら $\varphi^v=\lnot\lnot\psi$ で、帰納法の仮定は $\Gamma_v\vdash\psi$ である。$\{\psi\}\cup\{\lnot\psi\}$ は矛盾するので、lem-pc-tools の 2 の後半（論理式 $\lnot\psi$ に当てはめる）により $\{\psi\}\vdash\lnot\lnot\psi$ であり、$\Gamma_v\vdash\lnot\lnot\psi$ を得る。
含意． $\varphi=\psi\to\chi$ とし、3 つの場合に分ける。

• $v(\psi)=\mathrm{F}$ のとき：$\varphi^v=\varphi$ で、帰納法の仮定は $\Gamma_v\vdash\lnot\psi$ である。爆発律（lem-pc-tools の 1）により $\{\lnot\psi,\psi\}\vdash\chi$ なので、演繹定理により $\{\lnot\psi\}\vdash\psi\to\chi$ である。
• $v(\chi)=\mathrm{T}$ のとき：$\varphi^v=\varphi$ で、帰納法の仮定は $\Gamma_v\vdash\chi$ である。(A1) の実例 $\chi\to(\psi\to\chi)$ と MP で $\Gamma_v\vdash\psi\to\chi$ を得る。
• $v(\psi)=\mathrm{T}$、$v(\chi)=\mathrm{F}$ のとき：$\varphi^v=\lnot(\psi\to\chi)$ で、帰納法の仮定は $\Gamma_v\vdash\psi$、$\Gamma_v\vdash\lnot\chi$ である。$\{\psi,\lnot\chi,\psi\to\chi\}$ からは MP で $\chi$ が導出でき、$\lnot\chi$ も前提なので、この集合は矛盾する。lem-pc-tools の 2 の後半により $\{\psi,\lnot\chi\}\vdash\lnot(\psi\to\chi)$ であり、$\Gamma_v\vdash\lnot(\psi\to\chi)$ を得る。$\square$

lem-pc-tools の 2 により、$\Gamma\cup\{\lnot\varphi\}$ が矛盾することを示せばよい。$\Gamma\cup\{\lnot\varphi\}\cup\{\psi\}$ からは $\varphi$ と $\lnot\varphi$ が導出できるので矛盾し、2 の後半により $\Gamma\cup\{\lnot\varphi\}\vdash\lnot\psi$ である。同様に $\Gamma\cup\{\lnot\varphi\}\cup\{\lnot\psi\}$ は矛盾し、2 の前半により $\Gamma\cup\{\lnot\varphi\}\vdash\psi$ である。よって $\Gamma\cup\{\lnot\varphi\}$ は矛盾する。$\square$

$\varphi$ に現れる命題変数を $q_1,\dots,q_n$ とする。$m=n,n-1,\dots,0$ の順に、次の主張を示す。
$(\ast)_m$：すべての付値 $v$ について $\{q_1^v,\dots,q_m^v\}\vdash\varphi$。
$m=n$ のとき：$\varphi$ は恒真式なので $\varphi^v=\varphi$ であり、lem-pc-kalmar そのものである。
$(\ast)_m$ から $(\ast)_{m-1}$（$m\ge1$）：付値 $v$ をとり、$q_m$ だけを真に変えた付値を $v^+$、偽に変えた付値を $v^-$ とする。$i< m$ では $q_i^{v^\pm}=q_i^v$ なので、$\Gamma:=\{q_1^v,\dots,q_{m-1}^v\}$ とおくと、$(\ast)_m$ を $v^+,v^-$ に当てはめて
$$ \Gamma\cup\{q_m\}\vdash\varphi,\qquad\Gamma\cup\{\lnot q_m\}\vdash\varphi $$
を得る。lem-pc-cases により $\Gamma\vdash\varphi$ である。
$(\ast)_0$ は $\vdash\varphi$ である。$\square$

充足可能なら有限部分集合も同じ付値で充足される。逆に $\Gamma$ が充足可能でないとすると、prop-pc-model-existence により $\Gamma$ は矛盾し、lem-pc-tools の 3 によりある有限部分集合 $\Gamma_0$ が矛盾する。再び prop-pc-model-existence により $\Gamma_0$ は充足可能でない。$\square$

thm-pc-main により $\Gamma\vdash\varphi\iff\Gamma\models\varphi$ である。論理式の真理値は現れる命題変数の値だけで決まる（命題論理 の記事の補題「現れる変数だけで値が決まる」）。したがって $\Gamma\models\varphi$ は、$\Gamma\cup\{\varphi\}$ に現れる $k$ 個の命題変数の $2^k$ 通りの値それぞれで、$\Gamma$ の元がすべて真なのに $\varphi$ が偽になる場合がないかを調べれば判定できる。$\square$