命題論理

まず、論理式の真の始切片は論理式でない。論理式なら $L=R$、真の始切片なら $L>R$ で両立しないからである。また、帰納法により、論理式の最初の記号は命題変数か左括弧であり、$\lnot$ や $\land$ で始まる論理式はない。
形が 3 つのどれかであることは定義による。命題変数は長さ $1$ で括弧をもたず、2・3 の形は左括弧で始まるので、1 と 2・3 は重ならない。2 の形は 2 番目の記号が $\lnot$ であり、3 の形は 2 番目の記号が論理式 $\varphi$ の最初の記号（命題変数か左括弧）なので、2 と 3 も重ならない。
2 の一意性：$(\lnot\varphi)=(\lnot\varphi')$ なら、両端の記号を取り除いて $\varphi=\varphi'$ である。
3 の一意性：$(\varphi\ast\psi)=(\varphi'\ast'\psi')$ とする。先頭の左括弧を取り除いた記号列を見ると、$\varphi$ と $\varphi'$ はどちらもその始切片なので、一方が他方の始切片である。$\varphi\neq\varphi'$ なら短いほうが長いほうの真の始切片で、しかも論理式になり、最初の段落に反する。よって $\varphi=\varphi'$ であり、続く記号から $\ast=\ast'$、残りの記号列から $\psi=\psi'$ が従う。$\square$

$\varphi$ が命題変数なら仮定そのものである。$\varphi=\lnot\psi$ なら $\psi$ に現れる変数は $\varphi$ に現れるので、帰納法の仮定から $v(\psi)=w(\psi)$ であり、$v(\varphi)$ と $w(\varphi)$ は def-propositional-logic-valuation の規則によってこの共通の値から同じように決まる。$\varphi=\psi\ast\chi$ の場合も、$v(\psi)=w(\psi)$、$v(\chi)=w(\chi)$ から同様である。$\square$

$a\in\{\mathrm{T},\mathrm{F}\}^n$ に対し、$a_i=\mathrm{T}$ なら $\ell_i^a:=p_i$、$a_i=\mathrm{F}$ なら $\ell_i^a:=\lnot p_i$ とし、$C_a:=\ell_1^a\land\ell_2^a\land\cdots\land\ell_n^a$（括弧は左から順に付ける）とおく。$v(C_a)=\mathrm{T}$ は、すべての $i$ で $v(\ell_i^a)=\mathrm{T}$、すなわち $v(p_i)=a_i$ であることと同値である。よって $f_{C_a}(b)=\mathrm{T}\iff b=a$ である。
$f(a)=\mathrm{T}$ となる $a$ があれば、そのような $a$ 全体を $a^{(1)},\dots,a^{(k)}$ として $\varphi:=C_{a^{(1)}}\lor\cdots\lor C_{a^{(k)}}$ とおく。$f_\varphi(b)=\mathrm{T}$ は、ある $j$ で $b=a^{(j)}$、すなわち $f(b)=\mathrm{T}$ と同値なので、$f_\varphi=f$ である。そのような $a$ がなければ $\varphi:=p_1\land\lnot p_1$ とおくと、$f_\varphi$ はつねに $\mathrm{F}$ で $f$ に等しい。
後半：$\varphi\mapsto f_\varphi$ は同値類の集合から $\{\mathrm{T},\mathrm{F}\}^n$ 上の真理値の関数全体への単射であり、前半により全射である。関数全体は $2^{2^n}$ 個ある。$\square$

次の 3 つの同値は、$v(\varphi),v(\psi)$ の 4 通りを調べれば確かめられる。
$$ \lnot\varphi\equiv\varphi\uparrow\varphi,\qquad \varphi\land\psi\equiv(\varphi\uparrow\psi)\uparrow(\varphi\uparrow\psi),\qquad \varphi\lor\psi\equiv(\varphi\uparrow\varphi)\uparrow(\psi\uparrow\psi). $$
たとえば 3 つ目は、右辺が偽になるのが $\varphi\uparrow\varphi$ と $\psi\uparrow\psi$ がともに真、すなわち $\varphi,\psi$ がともに偽のときに限ることからわかる。論理式の組み立てに沿って $\varphi^{\uparrow}$ を定める：命題変数 $p$ では $p^{\uparrow}:=p$、$(\lnot\psi)^{\uparrow}:=\psi^{\uparrow}\uparrow\psi^{\uparrow}$、$(\psi\land\chi)^{\uparrow}:=(\psi^{\uparrow}\uparrow\chi^{\uparrow})\uparrow(\psi^{\uparrow}\uparrow\chi^{\uparrow})$、$(\psi\lor\chi)^{\uparrow}:=(\psi^{\uparrow}\uparrow\psi^{\uparrow})\uparrow(\chi^{\uparrow}\uparrow\chi^{\uparrow})$。帰納法の仮定 $v(\psi^{\uparrow})=v(\psi)$、$v(\chi^{\uparrow})=v(\chi)$ と上の同値から、各付値で $v(\varphi^{\uparrow})=v(\varphi)$ である。最後の主張は thm-propositional-logic-dnf と合わせて従う。$\square$

代表元によらないこと：$\varphi\equiv\varphi'$、$\psi\equiv\psi'$ なら、各付値で $v(\varphi\lor\psi)$ は $v(\varphi)=v(\varphi')$ と $v(\psi)=v(\psi')$ だけで決まるので $\varphi\lor\psi\equiv\varphi'\lor\psi'$ である。$\land$ と $\lnot$ も同様である。
$S:=\{\mathrm{T},\mathrm{F}\}^n$ とし、$\Phi\colon B_n\to\mathcal{P}(S)$ を $\Phi([\varphi]):=\{a\in S\mid f_\varphi(a)=\mathrm{T}\}$ で定める。$\varphi\equiv\psi\iff f_\varphi=f_\psi$ なので $\Phi$ は定義され単射であり、thm-propositional-logic-dnf により全射である。付値の規則から $\Phi([\varphi\lor\psi])=\Phi([\varphi])\cup\Phi([\psi])$、$\Phi([\varphi\land\psi])=\Phi([\varphi])\cap\Phi([\psi])$、$\Phi([\lnot\varphi])=S\setminus\Phi([\varphi])$、$\Phi(0)=\emptyset$、$\Phi(1)=S$ である。$\mathcal{P}(S)$ は Boole 代数であり（Boole代数 の記事の例「冪集合と 2 元の Boole 代数」）、$\Phi$ は演算を保つ全単射なので、Boole 代数の各等式は $\mathcal{P}(S)$ から $B_n$ に移り、$B_n$ は Boole 代数で $\Phi$ は同型である。順序：$[\varphi]\le[\psi]$ は $\Phi([\varphi])\subset\Phi([\psi])$、すなわち「$\varphi$ を真にする付値はすべて $\psi$ を真にする」ことであり、これは $\varphi\to\psi$ が恒真式であることと同値である。元の個数は $2^{|S|}=2^{2^n}$ で、原子は 1 点集合 $\{a\}=\Phi([C_a])$ に対応する。$\square$

規則の $\Gamma,\Delta$（主論理式を除いた部分）について、$\Gamma$ のある元が偽であるか、$\Delta$ のある元が真であるなら、結論も前提もすべて $v$ に満たされる。そこで $\Gamma$ がすべて真、$\Delta$ がすべて偽の場合を調べる。このとき各シーケントを満たすかどうかは、残りの論理式の真偽だけで決まる。

• $\lnot$ の左規則：結論を満たす $\iff v(\lnot A)=\mathrm{F}\iff v(A)=\mathrm{T}\iff$ 前提を満たす。右規則：結論を満たす $\iff v(\lnot A)=\mathrm{T}\iff v(A)=\mathrm{F}\iff$ 前提を満たす。
• $\land$ の左規則：結論を満たす $\iff v(A\land B)=\mathrm{F}\iff v(A)=\mathrm{F}$ または $v(B)=\mathrm{F}\iff$ 前提を満たす。右規則：結論を満たす $\iff v(A)=v(B)=\mathrm{T}\iff$ 2 つの前提をともに満たす。
• $\lor$ の左規則：結論を満たす $\iff v(A)=v(B)=\mathrm{F}\iff$ 2 つの前提をともに満たす。右規則：結論を満たす $\iff v(A)=\mathrm{T}$ または $v(B)=\mathrm{T}\iff$ 前提を満たす。
• $\to$ の左規則：結論を満たす $\iff v(A\to B)=\mathrm{F}\iff v(A)=\mathrm{T}$ かつ $v(B)=\mathrm{F}\iff$ 2 つの前提をともに満たす。右規則：結論を満たす $\iff v(A\to B)=\mathrm{T}\iff v(A)=\mathrm{F}$ または $v(B)=\mathrm{T}\iff$ 前提を満たす。
  $\Gamma$ に主論理式や $A,B$ がもともと含まれている場合（集合なので重複は 1 つにまとまる）も、上の同値は変わらない。$\square$

健全性（導出可能 $\Rightarrow$ 妥当）：導出の長さに関する帰納法で示す。始シーケント $\Gamma\Rightarrow\Delta$ は、共通の論理式 $A$ があるので、$\Gamma$ がすべて真なら $A\in\Delta$ が真であり、妥当である。規則の前提がすべて妥当なら、lem-propositional-logic-invertible によりどの付値も結論を満たすので、結論も妥当である。
完全性（妥当 $\Rightarrow$ 導出可能）：論理式 $A$ に現れる結合子の個数を $|A|$ とし、シーケント $S=(\Gamma\Rightarrow\Delta)$ について $c(S):=\sum_{A\in\Gamma}|A|+\sum_{A\in\Delta}|A|$ とおく。妥当な $S$ が導出可能であることを $c(S)$ に関する帰納法で示す。
$\Gamma\cap\Delta\neq\emptyset$ なら $S$ は始シーケントである。以下 $\Gamma\cap\Delta=\emptyset$ とする。
$\Gamma,\Delta$ の元がすべて命題変数の場合：付値 $v$ を、$\Gamma$ に属する命題変数で $\mathrm{T}$、それ以外で $\mathrm{F}$ と定めると、$\Gamma$ はすべて真で、$\Delta$ の元は $\Gamma$ に属さない命題変数なのですべて偽である。これは $S$ が妥当であることに反するので、この場合は起こらない。
そうでない場合：命題変数でない論理式 $C$ が $\Gamma$ か $\Delta$ のちょうど一方にある。$C\in\Gamma$ なら $\Gamma_0:=\Gamma\setminus\{C\}$ とおくと、$S$ は $C$ の結合子の左規則の、文脈 $\Gamma_0,\Delta$ での結論である（$C\in\Delta$ なら右規則で同様）。lem-propositional-logic-invertible により、$S$ が妥当なのでその前提はすべて妥当である。各前提では $C$ が取り除かれ、代わりに $C$ の直前の部分論理式（結合子の個数の合計は $|C|-1$ 以下）が加わるだけなので、$c(\text{前提})< c(S)$ である。帰納法の仮定により前提はすべて導出可能であり、その規則を使えば $S$ も導出可能である。
最後の主張：$\emptyset\Rightarrow\{\varphi\}$ を満たす付値は $\varphi$ を真にする付値であり、$\Sigma\Rightarrow\{\varphi\}$ が妥当であることは $\Sigma\vDash\varphi$ の定義そのものである。$\square$