形式体系

定理なら対応がとれている。 後の prop-formal-system-inductive により、空でない対応のとれた文字列の全体が $ab$ を含み (R1)・(R2) で閉じていることを示せばよい。$ab$ の始切片 $\varepsilon,a,ab$ の $h$ は $0,1,0$ である。$x$ が対応のとれた文字列なら、$axb$ の始切片は $\varepsilon$、$ap$（$p$ は $x$ の始切片）、$axb$ のどれかで、$h$ の値はそれぞれ $0$、$1+h(p)\ge1$、$1+h(x)-1=0$ である。$x,y$ が対応のとれた文字列なら、$xy$ の始切片は $x$ の始切片 $p$ か $xp'$（$p'$ は $y$ の始切片）で、$h(p)\ge0$、$h(xp')=h(x)+h(p')=h(p')\ge0$、$h(xy)=0$ である。
対応がとれていれば定理。 空でない対応のとれた文字列 $w$ の長さに関する帰納法で示す。長さ $1$ の始切片の $h$ が $0$ 以上なので、$w$ は $a$ で始まる。$h$ は 1 文字ごとに $\pm1$ ずつ変わり、$h(w)=0$ なので、長さが正で $h$ が $0$ になる始切片のうち最も短いもの $u$ がある。$w=uv$ と書く。$u$ より短い空でない始切片の $h$ は正なので、$u$ の最後の文字は $b$ であり、$u=au'b$ と書ける。$u'$ の始切片 $p$ について、$ap$ は $u$ より短い空でない始切片なので $h(p)=h(ap)-1\ge0$ であり、$h(u')=h(u)-1+1=0$ だから、$u'$ は対応のとれた文字列か空列である。$v$ についても、$h(up')=h(p')$ から対応のとれた文字列か空列である。
$u'=\varepsilon$ なら $u=ab$ は公理である。$u'\ne\varepsilon$ なら $u'$ は $w$ より短いので帰納法の仮定により定理であり、(R1) により $u$ も定理である。$v=\varepsilon$ なら $w=u$ で終わる。$v\ne\varepsilon$ なら $v$ は帰納法の仮定により定理であり、(R2) により $w=uv$ も定理である。$\square$

$Y:=\{\varphi\mid\Gamma\vdash_S\varphi\}$ とおく。$A\cup\Gamma$ の元は 1 行の導出をもつので $Y$ に属する。$\varphi_1,\dots,\varphi_k\in Y$ で $(\varphi_1,\dots,\varphi_k;\psi)\in\rho$ なら、$\varphi_1,\dots,\varphi_k$ の導出を順に並べ、最後に $\psi$ を書いた列は導出である（$\psi$ の行は、前にある $\varphi_1,\dots,\varphi_k$ の行から $\rho$ で得られる）。よって $Y$ は規則で閉じている。
逆に $X$ が $A\cup\Gamma$ を含み規則で閉じているとする。$\Gamma$ からの導出 $\psi_1,\dots,\psi_n$ の各行が $X$ に属することを $i$ に関する帰納法で示す。$\psi_i\in A\cup\Gamma$ なら $\psi_i\in X$ である。$\psi_i$ が前の行 $\psi_{j_1},\dots,\psi_{j_k}$ から規則で得られるなら、帰納法の仮定によりそれらは $X$ に属し、$X$ は規則で閉じているので $\psi_i\in X$ である。よって $Y\subset X$ である。$\square$

$\Gamma$ の元を、ある計算可能な手順で $\gamma_0,\gamma_1,\gamma_2,\dots$ と書き出せるとする（$\Gamma=\emptyset$ の場合は下の手順で前提を使わないだけである。帰納的可算集合 の定理「帰納的可算集合の言い換え」の 1 と 2 の同値性）。$\Sigma^*$ の元の有限列 $(w_1,\dots,w_n)$ と自然数 $m$ の組を、すべて漏れなく 1 つずつ並べる（記号が可算個で番号から求まるので、組の全体も符号化により自然数で番号付けられる）。各組について、次を検査する。

1. 各 $w_i$ が $F$ に属するか（$F$ は決定可能）。
2. 各 $w_i$ について、$w_i\in A$ であるか（$A$ は決定可能）、$w_i$ が $\gamma_0,\dots,\gamma_m$ のどれかに等しいか、またはある $\rho\in R$ と $i$ より前の行の組 $(w_{j_1},\dots,w_{j_k})$ について $(w_{j_1},\dots,w_{j_k};w_i)\in\rho$ であるか。$R$ は有限で、各 $\rho$ について前の行の組は有限個しかなく、各 $\rho$ は決定可能なので、この検査は有限の手順で終わる。
   検査に通った組について最後の行 $w_n$ を書き出す。導出の各行で前提として使った $\Gamma$ の元は有限個なので、ある $m$ でそれらがすべて $\gamma_0,\dots,\gamma_m$ に現れる。したがって $\Gamma\vdash_S\varphi$ ならば、$\varphi$ を最後の行とする導出と十分大きい $m$ の組が検査に通り、$\varphi$ が書き出される。逆に書き出されるのは導出の最後の行だけである。こうして $\{\varphi\mid\Gamma\vdash_S\varphi\}$ を計算可能な手順で書き出せた（この集合は $A\cup\Gamma$ が空でなければ空でなく、空なら導出は存在しない）。符号化すると、この集合は「$\varphi$ を最後の行とする組が検査に通る」という決定可能な関係の射影なので、帰納的可算集合 の定理「帰納的可算集合の言い換え」の 4 により帰納的可算である。$\square$

$T=\emptyset$ なら $T'=\emptyset$ でよい。$T\ne\emptyset$ なら、帰納的可算集合 の定理「帰納的可算集合の言い換え」の 2 により、計算可能な写像 $n\mapsto\sigma_n$ で $T=\{\sigma_n\mid n\in\mathbb N\}$ となるものがある。文 $\sigma$ と $n\ge0$ について、$\sigma$ を $n+1$ 個左から順に $\land$ で結んだ文を
$$ \sigma^{(0)}:=\sigma,\qquad\sigma^{(n+1)}:=\bigl(\sigma^{(n)}\land\sigma\bigr) $$
で定め、$T':=\{\sigma_n^{(n)}\mid n\in\mathbb N\}$ とおく。
$T'$ は決定可能である。 文 $\psi$ が与えられたとする。$\sigma^{(n)}$ の長さは $n$ とともに増えるので、$\psi=\sigma^{(n)}$ となりうる $n$ は $\psi$ の長さ以下である。各 $n$ について、$\psi$ が $\sigma^{(n)}$ の形かどうかは、外側から $\lnot(\ \cdot\ \to\lnot\ \cdot\ )$ の形をはがしていけば判定でき、その形ならはがし方は 1 通りで $\sigma$ も 1 つに決まる（論理式 の定理「一意読み取り」）。その $\sigma$ と $\sigma_n$ を計算して比べればよい。調べる $n$ は有限個なので、この手順は必ず終わる。
定理は同じである。 各 $n$ で、$\sigma_n^{(n)}$ と $\sigma_n$ はどの構造でも真偽が一致するので、$\{\sigma_n\}\models\sigma_n^{(n)}$ かつ $\{\sigma_n^{(n)}\}\models\sigma_n$ である。文の間では健全性と完全性により $\models$ と $\vdash$ が一致する（Gödelの完全性定理）ので、$\{\sigma_n\}\vdash\sigma_n^{(n)}$ かつ $\{\sigma_n^{(n)}\}\vdash\sigma_n$ である。よって $T$ から $T'$ のすべての元が、$T'$ から $T$ のすべての元が導出でき、一階論理の証明体系 の命題「導出可能性の基本性質」の 4（推移性）により、$T\vdash\varphi$ と $T'\vdash\varphi$ は同値である。$\square$