古典論理

1：$\varepsilon_i\ne\delta_i$ となる $i$ があり、$m_\varepsilon\wedge m_\delta$ は $a_i\wedge a_i'=0$ を含む交わりなので $0$ である。
2：$n$ についての帰納法による。$n=0$ では空な交わり $1$ である。$\{0,1\}^n$ の元を最初の $n-1$ 成分 $\varepsilon'$ と最後の成分に分けると、分配律により
$$ m_{\{0,1\}^n}=\bigvee_{\varepsilon'}\bigl((m_{\varepsilon'}\wedge a_n)\vee(m_{\varepsilon'}\wedge a_n')\bigr)=\bigvee_{\varepsilon'}\bigl(m_{\varepsilon'}\wedge(a_n\vee a_n')\bigr)=\bigvee_{\varepsilon'}m_{\varepsilon'} $$
であり、帰納法の仮定により右辺は $1$ である。
3：結びの式は結びの結合律と冪等律による。交わりは分配律で展開すると $\bigvee_{\varepsilon\in S,\,\delta\in T}(m_\varepsilon\wedge m_\delta)$ となり、1 により $\varepsilon=\delta$ の項 $m_\varepsilon$ だけが残るので $m_{S\cap T}$ である。$S^c:=\{0,1\}^n\setminus S$ とおくと、いま示した 2 式と 2 により $m_S\wedge m_{S^c}=m_\emptyset=0$、$m_S\vee m_{S^c}=1$ なので、$m_{S^c}$ は $m_S$ の補元である。補元は一意なので（Boole代数 の記事の命題「補元の一意性と基本法則」）、$m_S{}'=m_{S^c}$ である。
4：論理式に関する帰納法による。$\varphi=p_i$ のとき、2 と分配律により $a_i=a_i\wedge m_{\{0,1\}^n}=\bigvee_\varepsilon(a_i\wedge m_\varepsilon)$ であり、$a_i\wedge m_\varepsilon$ は $\varepsilon_i=1$ なら $m_\varepsilon$、$\varepsilon_i=0$ なら $a_i\wedge a_i'$ を含むので $0$ である。よって $a_i=m_S$（$S=\{\varepsilon:\varepsilon_i=1\}=S_{p_i}$）である。一方、真理値表の規則により
$$ S_{\lnot\varphi}=S_\varphi^c,\quad S_{\varphi\land\psi}=S_\varphi\cap S_\psi,\quad S_{\varphi\lor\psi}=S_\varphi\cup S_\psi,\quad S_{\varphi\to\psi}=S_\varphi^c\cup S_\psi $$
である。$[\![\cdot]\!]_v$ の定義と 3 を比べると、帰納法の仮定 $[\![\varphi]\!]_v=m_{S_\varphi}$、$[\![\psi]\!]_v=m_{S_\psi}$ から各場合が従う。たとえば $[\![\varphi\to\psi]\!]_v=m_{S_\varphi}{}'\vee m_{S_\psi}=m_{S_\varphi^c\cup S_\psi}=m_{S_{\varphi\to\psi}}$ である。$\square$

1 ⇒ 2：$\varphi$ が恒真式なら $S_\varphi=\{0,1\}^n$ である。任意の Boole 代数 $B$ と付値 $v$ について、lem-classical-logic-minterms の 4 と 2 により $[\![\varphi]\!]_v=m_{\{0,1\}^n}=1$ である。
2 ⇒ 1：$B=\{0,1\}$ とすると、$[\![\varphi]\!]_v$ は $v$ のもとでの通常の真理値に一致する（定義の各式が真理値表の規則と同じ）。すべての $v$ で値が $1$ なので、$\varphi$ は恒真式である。$\square$

$\varphi,\psi$ に現れる変数をまとめて $p_1,\dots,p_n$ とする。論理的に同値なら $S_\varphi=S_\psi$ なので、lem-classical-logic-minterms の 4 により値は等しい。逆に値がつねに等しければ、$B=\{0,1\}$ で真理値が等しいので論理的に同値である。$\square$

構造 $\mathcal M$ と割り当て $s$ を固定する。$x\notin\operatorname{FV}(\psi)$ なので、一階述語論理 の記事の補題「一致補題」により、すべての $a\in M$ について「$\mathcal M\models\psi[s_x^a]\iff\mathcal M\models\psi[s]$」である。以下 $A(a)$ を「$\mathcal M\models\varphi[s_x^a]$」、$P$ を「$\mathcal M\models\psi[s]$」と書く。充足の定義により、各組の両辺は次の主張になる。
1：左辺は「すべての $a$ で $A(a)$、ではない」、右辺は「ある $a$ で $A(a)$ でない」。各 $A(a)$ は成り立つか成り立たないかのどちらかなので、両者は同値である。後半も同様である。
3 の 1 つ目：左辺は「（すべての $a$ で $A(a)$）でない、または $P$」、右辺は「ある $a$ で（$A(a)$ でない、または $P$）」。$P$ が成り立つとき、左辺は真であり、右辺も真である。右辺では台集合が空でないことを使って $a$ を 1 つとる。$P$ が成り立たないとき、左辺は「すべての $a$ で $A(a)$、ではない」、右辺は「ある $a$ で $A(a)$ でない」で、1 と同じく同値である。
ほかの組も、$P$ が成り立つ場合と成り立たない場合に分けると、次の表のとおり両辺が同じ主張になる（$\psi$ が左右どちらにあっても $\land,\lor$ では同じである）。表の中の $\forall a\,A(a)$ は「すべての $a\in M$ で $A(a)$」、$\exists a\,A(a)$ は「ある $a\in M$ で $A(a)$」という主張を表す。

5 行目の $P$ が成り立たない場合の 2 つの主張は、定義から直ちに同値である。「元を 1 つとる」と書いた箇所で台集合が空でないことを使う。$\square$

$\chi$ に関する帰納法による。置き換える出現が $\chi$ 全体なら仮定そのものである。そうでなければ、出現は $\chi$ の直接の成分（$\lnot\chi_1$ の $\chi_1$、$(\chi_1\ast\chi_2)$ の一方、$Qx\,\chi_1$ の $\chi_1$）の中にあり、帰納法の仮定によりその成分は置き換えの前後で論理的に同値である。充足関係の定義では、$\chi$ の充足は各成分の（割り当て $s$ または $s_x^a$ のもとでの）充足だけで決まるので、$\chi$ と $\chi'$ も論理的に同値である。$\square$

$\chi$ の組み立てに沿った帰納法で示す。原子論理式は $k=0$ の冠頭形である。$\chi=Qx\,\chi_1$ なら、$\chi_1$ を帰納法の仮定で冠頭形 $\chi_1^*$ に替えた $Qx\,\chi_1^*$ が冠頭形であり、lem-classical-logic-replacement により $\chi$ と同値である。
$\chi=\lnot\chi_1$ で $\chi_1$ が冠頭形 $Q_1x_1\cdots Q_kx_k\,\theta$ と同値なら、lem-classical-logic-quantifier-moves の 1 と lem-classical-logic-replacement を $k$ 回使うと、$\lnot$ を右へ送って
$$ \lnot Q_1x_1\cdots Q_kx_k\,\theta\ \text{は}\ \overline{Q_1}x_1\cdots\overline{Q_k}x_k\,\lnot\theta\ \text{と同値} $$
である。ここで $\overline{\forall}=\exists$、$\overline{\exists}=\forall$ とする。
$\chi=(\chi_1\ast\chi_2)$（$\ast$ は $\land,\lor,\to$）で、$\chi_1,\chi_2$ がそれぞれ冠頭形 $Q_1x_1\cdots Q_kx_k\,\theta_1$、$R_1y_1\cdots R_ly_l\,\theta_2$ と同値だとする。一階述語論理 の記事の系「束縛変数の付け替え」と lem-classical-logic-replacement により、束縛変数 $x_1,\dots,x_k,y_1,\dots,y_l$ を、互いに異なり、$\chi_1,\chi_2$ にも 2 つの冠頭形 $Q_1x_1\cdots Q_kx_k\,\theta_1$、$R_1y_1\cdots R_ly_l\,\theta_2$ にも現れない新しい変数に替えておける（変数は無限個あるので、このような変数はとれる）。すると各 $x_i$ は $R_1y_1\cdots R_ly_l\,\theta_2$ の自由変数でなく、各 $y_j$ は $\theta_1$ の自由変数でない。lem-classical-logic-quantifier-moves の 2・3 を使って、まず $Q_1x_1,\dots,Q_kx_k$ を左から順に外へ出し、次に $R_1y_1,\dots,R_ly_l$ を外へ出すと、冠頭形
$$ Q_1^*x_1\cdots Q_k^*x_k\,R_1^*y_1\cdots R_l^*y_l\,(\theta_1\ast\theta_2) $$
を得る。ここで $Q_i^*$ は、$\ast$ が $\land,\lor$ のとき、または $\to$ の右側から出したときは $Q_i$ のままであり、$\to$ の左側から出したときだけ $\overline{Q_i}$ に替わる（lem-classical-logic-quantifier-moves の 3）。
どの段階も、束縛変数の付け替えと量化記号の移動は自由変数を変えないので、最後の冠頭形の自由変数は $\chi$ と同じである。$\square$