一階論理の証明体系

次の列は $\mathbf H$ の導出である。

1. $\varphi\to((\varphi\to\varphi)\to\varphi)$ ——(A1) で $\alpha:=\varphi$、$\beta:=\varphi\to\varphi$
2. $(\varphi\to((\varphi\to\varphi)\to\varphi))\to((\varphi\to(\varphi\to\varphi))\to(\varphi\to\varphi))$ ——(A2) で $\alpha:=\varphi$、$\beta:=\varphi\to\varphi$、$\gamma:=\varphi$
3. $(\varphi\to(\varphi\to\varphi))\to(\varphi\to\varphi)$ ——1、2 から MP
4. $\varphi\to(\varphi\to\varphi)$ ——(A1) で $\alpha:=\varphi$、$\beta:=\varphi$
5. $\varphi\to\varphi$ ——4、3 から MP
   各行は公理か、それより前の 2 行から MP で得られるので、定義の条件を満たす。$\square$

1：1 行の列 $\varphi$ が導出である。
2：$\Gamma$ からの導出の各行は、論理公理か、$\Gamma$ の元か、規則の結論である。$\Gamma\subset\Delta$ なので $\Gamma$ の元は $\Delta$ の元でもあり、ほかの条件は前提の集合によらない。よって同じ列が $\Delta$ からの導出である。
3：$\Gamma$ からの $\varphi$ の導出 $\varphi_1,\dots,\varphi_n$ をとり、$\Gamma_0:=\{\varphi_i\mid\varphi_i\in\Gamma\}$ とおく。$\Gamma_0$ は $n$ 個以下の元からなる有限集合で、前提として使った行はすべて $\Gamma_0$ に属するので、同じ列が $\Gamma_0$ からの導出である。
4：$\Delta$ からの $\psi$ の導出 $\psi_1,\dots,\psi_m$ をとる。その中で前提として使われた $\Delta$ の元は有限個 $\delta_1,\dots,\delta_k$ である。各 $\delta_j$ について $\Gamma$ からの導出 $D_j$ をとり、列 $D_1,\dots,D_k,\psi_1,\dots,\psi_m$ を作る。$\psi_l$ のうち前提 $\delta_j$ として正当化されていた行は、$D_j$ の最後の行の後にあり、$D_j$ で導出済みの式と同じ式なので、同じ式を繰り返し書いた行とみなせる（前の行と同じ式の行は、その前の行の正当化をそのまま使える）。ほかの行の正当化は変わらない。よってこの列は $\Gamma$ からの $\psi$ の導出である。$\square$

$\Leftarrow$：$\Gamma\vdash\alpha\to\beta$ なら、単調性により $\Gamma\cup\{\alpha\}\vdash\alpha\to\beta$ であり、$\Gamma\cup\{\alpha\}\vdash\alpha$ と合わせ、2 つの導出をつないで MP を 1 回使えば $\Gamma\cup\{\alpha\}\vdash\beta$ である。
$\Rightarrow$：$\Gamma\cup\{\alpha\}$ からの導出 $\beta_1,\dots,\beta_n=\beta$ をとり、$i$ に関する帰納法で、すべての $i$ について $\Gamma\vdash\alpha\to\beta_i$ を示す。

• $\beta_i$ が論理公理か $\Gamma$ の元の場合：$\beta_i$、(A1) の実例 $\beta_i\to(\alpha\to\beta_i)$、MP で $\alpha\to\beta_i$ という 3 行が $\Gamma$ からの導出である。
• $\beta_i=\alpha$ の場合：lem-first-order-proof-systems-identity により $\vdash\alpha\to\alpha$ である。
• $\beta_i$ が $\beta_j$ と $\beta_k=(\beta_j\to\beta_i)$（$j,k< i$）から MP で得られた場合：帰納法の仮定により $\Gamma\vdash\alpha\to\beta_j$ と $\Gamma\vdash\alpha\to(\beta_j\to\beta_i)$ である。(A2) の実例
  $$ (\alpha\to(\beta_j\to\beta_i))\to((\alpha\to\beta_j)\to(\alpha\to\beta_i)) $$
  と MP を 2 回使えば $\Gamma\vdash\alpha\to\beta_i$ である（導出をつなぐことは prop-first-order-proof-systems-structural の 4 で正当化される）。
  $\mathbf H$ の推論規則は MP だけなので、場合はこれで尽きる。$i=n$ として $\Gamma\vdash\alpha\to\beta$ である。$\square$

$\Gamma$ からの導出 $\varphi_1,\dots,\varphi_n=\varphi$ をとり、$i$ に関する帰納法で、すべての $i$ について $\Gamma\vdash\forall x\,\varphi_i$ を示す。

• $\varphi_i$ が論理公理の場合：論理公理は公理図式の実例の全称化なので、$\forall x\,\varphi_i$ も論理公理である。
• $\varphi_i\in\Gamma$ の場合：仮定から $x\notin\operatorname{FV}(\varphi_i)$ なので、$\varphi_i\to\forall x\,\varphi_i$ は (A6) の実例である。$\varphi_i$ とこの公理から MP で $\forall x\,\varphi_i$ を得る。
• $\varphi_i$ が $\varphi_j$ と $\varphi_j\to\varphi_i$ から MP で得られた場合：帰納法の仮定により $\Gamma\vdash\forall x\,\varphi_j$ と $\Gamma\vdash\forall x\,(\varphi_j\to\varphi_i)$ である。(A5) の実例 $\forall x\,(\varphi_j\to\varphi_i)\to(\forall x\,\varphi_j\to\forall x\,\varphi_i)$ と MP を 2 回使えば $\Gamma\vdash\forall x\,\varphi_i$ である。
  $i=n$ として主張を得る。$\square$

構造 $\mathcal M$ と割り当て $s$ を任意にとり、各公理図式の実例が $s$ のもとで真であることを示す。以下「真」は $\mathcal M$、$s$ のもとで真であることをいう。
(A1)〜(A3)：$\to$ と $\lnot$ の充足条件は真理値表と同じなので、$\alpha,\beta,\gamma$ の真偽の組み合わせを調べればよい。(A1) が偽になるには $\alpha$ が真で $\beta\to\alpha$ が偽でなければならないが、$\alpha$ が真なら $\beta\to\alpha$ は真である。(A2) が偽になるには、$\alpha\to(\beta\to\gamma)$ と $\alpha\to\beta$ が真で $\alpha\to\gamma$ が偽、すなわち $\alpha$ が真で $\gamma$ が偽でなければならない。そのとき $\alpha\to\beta$ から $\beta$ が真、$\alpha\to(\beta\to\gamma)$ から $\gamma$ が真となり矛盾する。(A3) が偽になるには、$\lnot\beta\to\lnot\alpha$ と $\lnot\beta\to\alpha$ が真で $\beta$ が偽でなければならない。そのとき $\lnot\beta$ が真なので $\lnot\alpha$ と $\alpha$ がともに真となり矛盾する。
(A4)：$\forall x\,\alpha$ が真とし、$b:=t^{\mathcal M}[s]$ とおく。充足の定義から $\mathcal M\models\alpha[s_x^b]$ である。$t$ は $\alpha$ の $x$ に代入可能なので、一階述語論理 の記事の補題「代入補題」の 2 により $\mathcal M\models\alpha[t/x][s]$ である。
(A5)：$\forall x\,(\alpha\to\beta)$ と $\forall x\,\alpha$ が真とする。各 $a\in M$ について $\alpha\to\beta$ と $\alpha$ が $s_x^a$ のもとで真なので、$\beta$ も $s_x^a$ のもとで真である。よって $\forall x\,\beta$ は真である。
(A6)：$\alpha$ が真とする。$x\notin\operatorname{FV}(\alpha)$ なので、各 $a\in M$ について $s$ と $s_x^a$ は $\operatorname{FV}(\alpha)$ の上で一致し、一階述語論理 の記事の補題「一致補題」により $\alpha$ は $s_x^a$ のもとでも真である。よって $\forall x\,\alpha$ は真である。
(A7)：$x^{\mathcal M}[s]=x^{\mathcal M}[s]$ なので真である。
(A8)：$x=y$ が真、すなわち $s(x)=s(y)$ とする。まず、項 $u$ の中の $x$ の出現のいくつかを $y$ に置き換えた項を $u'$ とすると $u'^{\mathcal M}[s]=u^{\mathcal M}[s]$ であることを、項に関する帰納法で示す。$u$ が変数 $x$ なら $u'$ は $x$ か $y$ で、どちらの値も $s(x)$ である。$u$ がほかの変数か定数記号なら $u'=u$ である。$u=f(u_1,\dots,u_n)$ なら $u'=f(u_1',\dots,u_n')$（各 $u_i'$ は $u_i$ の出現のいくつかを置き換えたもの）なので、帰納法の仮定から値は等しい。原子論理式 $\alpha$ は $u_1=u_2$ か $R(u_1,\dots,u_n)$ の形で、$\beta$ はそれぞれ $u_1'=u_2'$、$R(u_1',\dots,u_n')$ の形である。各項の値が変わらないので、$\alpha$ が真なら $\beta$ も真である。
全称化：論理式 $\theta$ が妥当なら $\forall x\,\theta$ も妥当である。実際、任意の $\mathcal M$、$s$、$a\in M$ について $\theta$ は $s_x^a$ のもとで真なので、$\forall x\,\theta$ は $s$ のもとで真である。公理図式の実例はいま示したとおり妥当なので、その全称化も（全称記号の個数に関する帰納法で）妥当である。$\square$

構造 $\mathcal M$ と割り当て $s$ で、$\Gamma$ のすべての元が $s$ のもとで真であるものをとる。$\Gamma$ からの導出 $\varphi_1,\dots,\varphi_n=\varphi$ の各行が $s$ のもとで真であることを、$i$ に関する帰納法で示す。$\varphi_i$ が論理公理なら lem-first-order-proof-systems-axioms-valid により真である。$\varphi_i\in\Gamma$ なら $s$ の選び方から真である。$\varphi_i$ が $\varphi_j$ と $\varphi_j\to\varphi_i$ から MP で得られたなら、帰納法の仮定によりこの 2 つは真であり、$\to$ の充足条件から $\varphi_i$ も真である。よって $\varphi=\varphi_n$ は $s$ のもとで真である。$\mathcal M,s$ は任意だったので $\Gamma\models\varphi$ である。$\square$