超丁寧に解説するゲーデルの完全性定理（前編）

$T$からの証明列は、そのまま$T'$からの証明列の条件を満たす（条項$2$が$T'$でも成り立つため）。$\square$

$\bar v(\psi) = \mathbb{F}$とすると、$\bar v(\varphi)=\mathbb{T}$と併せて$\bar v$の定義より$\bar v(\varphi \to \psi) = \mathbb{F}$となり不合理。$\square$

前半：$\mathbf{P1}$～$\mathbf{P3}$の実例がトートロジーであることは、真理値表を書けば確かめられる（たとえば$\mathbf{P3}$は、値が$\mathbb{F}$と仮定すると$\bar v(\varphi)=\mathbb{T}\, , \bar v(\psi)=\mathbb{F}$、ゆえに $\bar v(\neg\psi)=\mathbb{T} \, ,\bar v(\neg\varphi)=\mathbb{F}$となり、前件が$\mathbb{F}$になって不合理）。
$v \models T$なる任意の$v$を固定し、$T$からの証明$\varphi_0,\dots,\varphi_n = \varphi$の添字$k$に関する累積帰納法で$\bar v(\varphi_k) = \mathbb{T}$を示す。定義2の三つの場合のうち、条項$1$は公理のトートロジー性から、条項$2$は$v \models T$から従い、どちらも帰納法の仮定を使わない。条項$3$では$i, j < k$だから帰納法の仮定が両方に使えて、補題4より$\bar v(\varphi_k) = \mathbb{T}$。$k = n$とすれば$v \models \varphi$であり、$v$は任意だったから$T \models \varphi$。
後半：$v \models T$とする。$T$が矛盾するなら$T \vdash \chi$かつ$T \vdash \neg\chi$ なる$\chi$があり、前半より$\bar v(\chi) = \bar v(\neg\chi) = \mathbb{T}$となって$\neg$の真理条件に反する。$\square$

次の五行が$\emptyset$からの証明列である。
$(1)$ $\big(\varphi \to ((\varphi\to\varphi) \to \varphi)\big) \to \Big(\big(\varphi\to(\varphi\to\varphi)\big) \to (\varphi \to \varphi)\Big)$
根拠：$\mathbf{P2}$ $(\psi = \varphi\to\varphi \, , \chi = \varphi)$
$(2)$ $\varphi \to ((\varphi\to\varphi) \to \varphi)$
根拠：$\mathbf{P1}$ $(\psi = \varphi\to\varphi)$
$(3)$ $\big(\varphi\to(\varphi\to\varphi)\big) \to (\varphi\to\varphi)$
根拠：$(1)$,$(2)$に $\mathrm{MP}$
$(4)$ $\varphi \to (\varphi\to\varphi)$
根拠：$\mathbf{P1}$ $(\psi = \varphi)$
$(5)$ $\varphi \to \varphi$
根拠：$(3)$,$(4)$ に $\mathrm{MP}$
$\square$

$T \cup \lbrace \varphi \rbrace$からの証明$\psi_0, \dots, \psi_n = \psi$を固定し、添字$k$に関する累積帰納法で$T \vdash \varphi \to \psi_k$を示す。定義2より場合は三つ。
$(\text{i})$ $\psi_k$が公理の実例、または$\psi_k \in T$のとき：
どちらも$T \vdash \psi_k$である。
$\mathbf{P1}$の実例$\psi_k \to (\varphi \to \psi_k)$と$\mathrm{MP}$により$T \vdash \varphi \to \psi_k$。
$(\text{ii})$ $\psi_k = \varphi$ のとき：
補題6と単調性（補題3）より $T \vdash \varphi \to \varphi$。
$(\text{iii})$ ある$i, j < k$について$\psi_j = \psi_i \to \psi_k$のとき：
帰納法の仮定より$T \vdash \varphi\to\psi_i$および$T \vdash \varphi \to (\psi_i \to \psi_k)$。$\mathbf{P2}$の実例
$$ \big(\varphi \to (\psi_i \to \psi_k)\big) \to \Big(\big(\varphi\to\psi_i\big) \to \big(\varphi\to\psi_k\big)\Big)$$
に$\mathrm{MP}$を二回適用して$T \vdash \varphi\to\psi_k$。
なお$\psi_k$が$T \cup \lbrace \varphi \rbrace$の要素である場合は、$\psi_k \in T$なら$(\text{i})$、$\psi_k = \varphi$なら$(\text{ii})$で処理されている。$k=n$として結論を得る。
逆向き：$T \vdash \varphi\to\psi$なら、単調性より$T \cup \lbrace \varphi \rbrace\vdash\varphi\to\psi$であり、$T \cup \lbrace \varphi \rbrace\vdash\varphi$と$\mathrm{MP}$から$T \cup \lbrace \varphi \rbrace\vdash\psi$。$\square$

$T \cup \lbrace \neg\varphi \rbrace $が矛盾するなら、ある$\chi$について $T \cup \lbrace \neg\varphi \rbrace \vdash \chi$かつ$T \cup \lbrace \neg\varphi \rbrace \vdash \neg\chi$。演繹定理より$T \vdash \neg\varphi \to \chi$および$T \vdash \neg\varphi \to \neg\chi$。後者と$\mathbf{P3}$から$T \vdash \chi \to \varphi$。これと前者を三段論法でつないで$T \vdash \neg\varphi \to \varphi$。道具箱$(2)$と$\mathrm{MP}$より $T \vdash \varphi$。後半も同様（道具箱$(4)$を併用する）。$\square$

両方矛盾するとすると、補題9より$T \vdash \neg\varphi$かつ$T \vdash \varphi$となり、$T$が矛盾する。$\square$

前半：証明は有限列だから、条項$2$によってそこに現れる$T$の要素は有限個。それを$S$とすればよい。
後半：$T \vdash \chi$, $T \vdash \neg\chi$なる$\chi$ をとり、前半を二回使って有限部分集合$S_1, S_2$を得れば、$S_1 \cup S_2$が矛盾する有限部分集合である。$\square$

$(1)\Rightarrow(2)$：補題10より$U \cup \lbrace \varphi \rbrace $か$U \cup \lbrace \neg\varphi \rbrace $の一方は無矛盾。極大性よりそれは$U$自身に等しく、$\varphi \in U$または$\neg\varphi \in U$。
$(2)\Rightarrow(1)$：$U \subsetneq U'$と$\varphi \in U' \setminus U$をとる。$(2)$より$\neg\varphi \in U \subseteq U'$。一方$\varphi \in U'$だから$U'$は矛盾する。$\square$

$\varphi \notin U$とすると補題12より$\neg\varphi \in U$、すなわち$U \vdash \neg\varphi$。$U \vdash \varphi$と併せて$U$が矛盾し、不合理。$\square$

$X = \lbrace T' \subseteq \mathrm{Fml} : T \subseteq T' \text{ かつ } T' \text{ は無矛盾} \rbrace $ とおき、包含関係で半順序集合とみなす。$T \in X$より$X \neq \emptyset$。
$\mathcal{Y} \subseteq X$を空でない鎖（全順序部分集合）とし、$T_{\mathcal{Y}} = \bigcup \mathcal{Y}$とおく。$T_{\mathcal{Y}}$が無矛盾であることを示す。矛盾したとすると、補題11より矛盾する有限部分集合$ \lbrace \varphi_1,\dots,\varphi_n \rbrace \subseteq T_{\mathcal{Y}}$がとれる。各$\varphi_i$はある$T_i \in \mathcal{Y}$に属し、$\mathcal{Y}$は鎖だから、これら有限個のうち最大のもの$T_j$が存在して$\lbrace \varphi_1,\dots,\varphi_n \rbrace \subseteq T_j$。すると$T_j$が矛盾し、$T_j \in X$に反する。よって$T_{\mathcal{Y}} \in X$は$\mathcal{Y}$の上界である。
Zornの補題より$X$は極大元$U$を持ち、これが求める極大無矛盾な拡大である。$\square$

$(\text{i})$ $\varphi$が命題変数のとき：定義そのもの。
$(\text{ii})$ $\varphi = \neg\psi$のとき：
$$ \bar v_U(\neg\psi) = \mathbb{T} \iff \bar v_U(\psi) = \mathbb{F} \iff \psi \notin U \iff \neg\psi \in U$$
一つ目は $\bar v$ の定義、二つ目は帰納法の仮定、三つ目は補題12（$\psi \in U$ か $\neg\psi \in U$）と $U$ の無矛盾性（両方は入らない）である。
$(\text{iii})$ $\varphi = \psi \to \chi$ のとき：示すべきは
$$ (\psi \to \chi) \in U \iff (\psi \notin U \text{ または } \chi \in U)$$
（左辺が$\bar v_U(\psi\to\chi)=\mathbb{T}$と、右辺が$\bar v_U(\psi)=\mathbb{F}$または$\bar v_U(\chi)=\mathbb{T}$と、帰納法の仮定により対応する。）
$(\Rightarrow)$：$(\psi \to \chi) \in U$かつ$\psi \in U$とすると、$\mathrm{MP}$より$U \vdash \chi$、補題13より$\chi \in U$。
$(\Leftarrow)$：$\chi \in U$なら、$\mathbf{P1}$より$U \vdash \chi \to (\psi \to \chi)$、$\mathrm{MP}$と補題13より$(\psi\to\chi) \in U$。$\psi \notin U$なら補題12より$\neg\psi \in U$で、道具箱$(1)$より $U \vdash \neg\psi \to (\psi \to \chi)$、よって $(\psi \to \chi) \in U$。$\square$

Lindenbaumの補題より、$T \subseteq U$なる極大無矛盾な理論$U$をとる。真理補題より、$\varphi \in U$なる任意の$\varphi$について$\bar v_U(\varphi) = \mathbb{T}$。とくに$T \subseteq U$だから$v_U \models T$。$\square$

$(\Rightarrow)$は健全性そのもの。$(\Leftarrow)$は対偶を示す。$T \nvdash \varphi$とすると、補題9の対偶より$T \cup \lbrace \neg\varphi \rbrace $は無矛盾。モデル存在定理より$T \cup \lbrace \neg\varphi \rbrace $のモデル$v$が存在する。この$v$は$v \models T$かつ$\bar v(\varphi) = \mathbb{F}$を満たすから、$T \not\models \varphi$。$\square$

$T$の任意の有限部分集合$S$はモデルを持つから、健全性より$S$は無矛盾。補題11の後半の対偶より$T$は無矛盾。モデル存在定理より$T$はモデルを持つ。$\square$