超丁寧に解説するΣ_1完全性と表現定理

いずれも$m, n$についてのメタレベルの帰納法による、ルーチンな計算である。要点だけ示す。
$\mathbf{R1}$は$\mathbf{Q4}$, $\mathbf{Q5}$から$n$についての帰納法で、$\mathbf{R2}$は$\mathbf{Q6}$, $\mathbf{Q7}$と$\mathbf{R1}$から$n$についての帰納法で得られる。$\mathbf{R3}$は$\mathbf{Q1}$と$\mathbf{Q2}$から、$m, n$についての帰納法で得られる。
$\mathbf{R4}$は$n$についてのメタレベルの帰納法による。$n = 0$の場合を見ておこう。$x \le \overline{0}$は$\exists w(w+x = 0)$である。$\mathbf{Q3}$より$x = 0$または$x = s(u)$なる$u$がある。前者ならよい。後者なら$\mathbf{Q5}$より$w+x = w+s(u) = s(w+u)$であり、$\mathbf{Q2}$よりこれは$0$と等しくない。よって$x = \overline{0}$。
$\mathbf{R5}$も$n$についてのメタレベルの帰納法による。$\square$

$(1)$ $x < \overline{n}$は$x \le \overline{n} \wedge x \neq \overline{n}$である。$\mathbf{R4}$より$x = \overline{0} \vee \cdots \vee x = \overline{n}$が得られ、$x \neq \overline{n}$が最後の選言肢を除く。
$(2)$ $\mathbf{R5}$より$x \le \overline{n}$または$\overline{n} \le x$。前者の場合、$x = \overline{n}$かそうでないかで場合分けすれば、$x = \overline{n}$または$x < \overline{n}$。後者も同様に$x = \overline{n}$または$\overline{n} < x$。$\square$

$t$の構成に関する帰納法。
$t = 0$のとき：$n = 0$であり$\overline{0} = 0$なので明らか。
$t = s(u)$のとき：$u$の値を$k$とすると$n = k+1$。帰納法の仮定より$\mathrm{R} \vdash u = \overline{k}$。よって$\mathrm{R} \vdash s(u) = s(\overline{k})$であり、$s(\overline{k})$は$\overline{k+1} = \overline{n}$そのものである。
$t = u + v$のとき：$u, v$の値をそれぞれ$k, l$とすると$n = k+l$。帰納法の仮定より$\mathrm{R} \vdash u = \overline{k}$, $\mathrm{R} \vdash v = \overline{l}$。$\mathbf{R1}$より$\mathrm{R} \vdash \overline{k} + \overline{l} = \overline{k+l}$。等号の推移律を使って$\mathrm{R} \vdash u+v = \overline{n}$。
$t = u \cdot v$のとき：$\mathbf{R2}$を使って同様。$\square$

$\varphi$が$\Delta_0$論理式であることの定義に関する帰納法。以下、閉項$t$の値を$|t|$と書く。
$(\text{i})$ $\varphi$が$t = u$の形のとき。$\varphi^*$は閉項どうしの等式$t^* = u^*$である。閉項の計算の補題より$\mathrm{R} \vdash t^* = \overline{|t^*|}$, $\mathrm{R} \vdash u^* = \overline{|u^*|}$。$|t^*| = |u^*|$ならば$\mathrm{R} \vdash t^* = u^*$。$|t^*| \neq |u^*|$ならば$\mathbf{R3}$より$\mathrm{R} \vdash \overline{|t^*|} \neq \overline{|u^*|}$、よって$\mathrm{R} \vdash \neg(t^* = u^*)$。
$(\text{ii})$ $\varphi$が$t \le u$の形のとき。$m = |t^*|$, $n = |u^*|$とおけば$\overline{m} \le \overline{n}$の場合に帰着する。
$m \le n$のとき：$k = n - m$とおくと$\mathbf{R1}$より$\mathrm{R} \vdash \overline{k} + \overline{m} = \overline{n}$。存在導入して$\mathrm{R} \vdash \exists w(w + \overline{m} = \overline{n})$、すなわち$\mathrm{R} \vdash \overline{m} \le \overline{n}$。
$m > n$のとき：$\mathbf{R4}$より$\mathrm{R} \vdash \overline{m} \le \overline{n} \to (\overline{m} = \overline{0} \vee \cdots \vee \overline{m} = \overline{n})$。各$i \le n$について$m \neq i$だから$\mathbf{R3}$より$\mathrm{R} \vdash \overline{m} \neq \overline{i}$。よって右辺の否定が導け、$\mathrm{R} \vdash \neg(\overline{m} \le \overline{n})$。
$(\text{iii})$ $\varphi$が$\neg\psi$や$\psi \to \chi$の形のとき（$\wedge$, $\vee$で作ったものも同様）。$\varphi^*$は$\neg\psi^*$や$\psi^* \to \chi^*$の形で、$\psi^*, \chi^*$はそれぞれ$\psi, \chi$の代入結果だから、帰納法の仮定と命題論理から直ちに従う。たとえば$\varphi = \neg\psi$で$\mathfrak{N} \models \varphi^*$なら$\mathfrak{N} \not\models \psi^*$だから、帰納法の仮定より$\mathrm{R} \vdash \neg\psi^*$、すなわち$\mathrm{R} \vdash \varphi^*$。
$(\text{iv})$ $\varphi$が$\forall x \le t\ \psi$の形のとき。$\varphi^*$は$\forall x \le t^*\ \psi^*(x)$の形である。ここで$t^*$は閉項、$\psi^*(x)$は$\psi$の$x$以外の自由変数に数項を代入したものである。$n = |t^*|$とおく。閉項の計算の補題より$\mathrm{R} \vdash t^* = \overline{n}$なので、$\overline{n}$の場合を考えればよい。$\mathbf{R4}$より
$$ \mathrm{R} \vdash \forall x\big(x \le \overline{n} \to (x = \overline{0} \vee \cdots \vee x = \overline{n})\big) $$
各$i \le n$について、$\psi^*(\overline{i})$は$\psi$の代入結果であることに注意する。
$\mathfrak{N} \models \varphi^*$のとき：各$i \le n$について$\mathfrak{N} \models \psi^*(\overline{i})$だから、帰納法の仮定より$\mathrm{R} \vdash \psi^*(\overline{i})$。上の式と合わせて$\mathrm{R} \vdash \forall x \le \overline{n}\ \psi^*(x)$。
$\mathfrak{N} \not\models \varphi^*$のとき：ある$i \le n$で$\mathfrak{N} \not\models \psi^*(\overline{i})$。帰納法の仮定より$\mathrm{R} \vdash \neg\psi^*(\overline{i})$。また$(\text{ii})$より$\mathrm{R} \vdash \overline{i} \le \overline{n}$。よって$\mathrm{R} \vdash \neg\forall x \le \overline{n}\ \psi^*(x)$。
$(\text{v})$ $\varphi$が$\exists x \le t\ \psi$の形のとき。$(\text{iv})$と双対的である。$\square$

$\varphi = \exists x_1 \cdots \exists x_k\ \theta(x_1,\dots,x_k)$（$\theta$は$\Delta_0$）とする。$\mathfrak{N} \models \varphi$だから、自然数$n_1,\dots,n_k$が存在して$\mathfrak{N} \models \theta(n_1,\dots,n_k)$。
$\theta(\overline{n_1},\dots,\overline{n_k})$は$\Delta_0$論理式$\theta$の代入結果であり、$\mathfrak{N}$で真だから、$\Delta_0$完全性より
$$ \mathrm{R} \vdash \theta(\overline{n_1},\dots,\overline{n_k}) $$
存在導入を$k$回適用して$\mathrm{R} \vdash \varphi$。$\square$

$m = \max(n, x_0, \dots, x_n)$とおき、$\delta(m) = \mathrm{lcm}(1, 2, \dots, m)$（$1$から$m$までの最小公倍数。$\delta(0) = 1$と約束する）とする。$b = \delta(m)$として、$y_i = (i+1)b+1$（$0 \le i \le n$）とおく。
$y_0, \dots, y_n$は互いに素である。 $i < j \le n$とし、素数$p$が$y_i$と$y_j$の共通の約数だとする。$p$は$y_j - y_i = (j-i)b$を割る。ここで$p$は$b$を割らない。もし$p \mid b$なら$p \mid y_i = (i+1)b+1$から$p \mid 1$となって不合理だからである。よって$p \mid (j-i)$。ところが$0 < j-i \le n \le m$だから$(j-i)$は$1$から$m$までのどれかであり、$(j-i) \mid \delta(m) = b$。したがって$p \mid b$となって矛盾。
各$i$について$x_i < y_i$である。 実際$x_i \le m \le \delta(m) = b < (i+1)b+1 = y_i$。
以上より、中国剰余定理から、$a \equiv x_i \pmod{y_i}$（$0 \le i \le n$）を満たす自然数$a$が存在する。$x_i < y_i$だから$a$を$y_i$で割った余りはちょうど$x_i$であり、$\beta(a,b,i) = x_i$。$\square$

$\beta$関数定理で得られる$a, b$を用いて$e = \mathrm{pair}(a,b)$とすればよい。$\square$

$Z_k(\vec x) = \mu y\big(P^{k+1}_{k+1}(\vec x, y) = 0\big) = \mu y (y = 0) = 0$。
$\mathrm{one}(x) = \mu y\big(\mathrm{equal}(Z_2(x,y), P^2_2(x,y)) = 0\big) = \mu y\big(\mathrm{equal}(0,y) = 0\big)$。$\mathrm{equal}(0,0) = 1 \neq 0$、$\mathrm{equal}(0,1) = 0$だから値は$1$である。
$s(x) = P^1_1(x) + \mathrm{one}(x)$。$\square$

$(\neg A)^{\circ}(\vec x) = \mathrm{equal}(A^{\circ}(\vec x), 0)$、$(A \wedge B)^{\circ}(\vec x) = A^{\circ}(\vec x) \cdot B^{\circ}(\vec x)$、$(A \vee B)^{\circ} = (\neg(\neg A \wedge \neg B))^{\circ}$。$\square$

補題9より$(\neg A)^{\circ}$は$\mathrm{Recu}$に属し、$A(\vec x, y)$が成り立つときちょうど$0$になる。仮定より、各$\vec x$に対して$(\neg A)^{\circ}(\vec x, y) = 0$となる$y$があるので、$\mathrm{Recu}$の定義の$(3)$より
$$ f(\vec x) = \mu y\big[(\neg A)^{\circ}(\vec x, y) = 0\big] $$
は$\mathrm{Recu}$に属す。$\square$

$m(\vec x) = \mu y\big(y = t(\vec x) \vee A(\vec x, y)\big)$とおく。この条件は$\mathrm{Recu}$述語である（$y = t(\vec x)$の特性関数は$\mathrm{equal}(y, t(\vec x))$で、$\vee$は補題9で保たれる）。また$y = t(\vec x)$で必ず成り立つ。よって前の補題より$m$は$\mathrm{Recu}$に属し、$m(\vec x) \le t(\vec x)$である。
$m(\vec x) < t(\vec x)$は「$t(\vec x)$より前に条件を満たす$y$がある」ということであり、$y < t(\vec x)$では条件は$A(\vec x, y)$と同じである。したがって
$$ (\exists y < t(\vec x))A(\vec x, y) \iff m(\vec x) < t(\vec x) \iff m(\vec x) \neq t(\vec x) $$
（後の同値は$m(\vec x) \le t(\vec x)$による）。右端は$\mathrm{Recu}$述語$m(\vec x) = t(\vec x)$の否定なので、$\mathrm{Recu}$述語である。$\forall$は$(\forall y < t)A \iff \neg(\exists y < t)\neg A$から従う。$\square$

定数$1$, $2$は$\mathrm{one}$から足し算で作れる。以下で最小化する条件はどれも、すでに$\mathrm{Recu}$と分かった関数の等式（$\mathrm{equal}$）を論理結合子と有界量化子で組み合わせたものなので、$\mathrm{Recu}$述語である。よって補題10を使うには、条件を満たす値が必ずあることを示せばよい。あわせて、最小値が意図した値であることも確かめる。
・$\mathrm{half}(x) = \mu y\big((2\cdot y = x) \vee (2\cdot y + 1 = x)\big)$とおく。条件は$2y \le x \le 2y+1$と同じで、これを満たす$y$は$\lfloor x/2 \rfloor$ただ一つである。よって$\mathrm{half}(x) = \lfloor x/2 \rfloor$。
・$(x+y)(x+y+1)$は連続する二数の積で偶数なので、$\mathrm{pair}(x,y) = \mathrm{half}\big((x+y)(x+y+1)\big) + x$。
・$\mathrm{1st}(z) = \mu x(\exists y < z+1)(z = \mathrm{pair}(x,y))$、$\mathrm{2nd}(z) = \mu y(\exists x < z+1)(z = \mathrm{pair}(x,y))$だった。$\mathrm{pair}$は全単射なので、$z = \mathrm{pair}(x_0, y_0)$となる$(x_0, y_0)$がただ一組ある。$\frac{n(n+1)}{2} \ge n$より$\mathrm{pair}(x,y) \ge (x+y) + x$なので、$x_0, y_0 \le z$であり、上限$z+1$の範囲に入る。よって$\mathrm{1st}$の条件を満たす$x$は$x_0$だけ、$\mathrm{2nd}$の条件を満たす$y$は$y_0$だけであり、$\mathrm{1st}(z) = x_0$, $\mathrm{2nd}(z) = y_0$。
・$\mathrm{rm}(x,y) = \mu z(\exists q < x+1)(x = q\cdot y + z)$とおく。$z = x$は$q = 0$で条件を満たす。$y \ge 1$のとき、条件を満たす$z$は、$q\cdot y \le x$を満たす$q$を使って$z = x - q\cdot y$と書ける数である（このとき$q \le x$なので、上限で漏れる$q$はない）。最小になるのは$q$が商のときで、そのときの$z$が余りである。$y = 0$のときは$\mathrm{rm}(x, 0) = x$となるが、$\beta$では割る数が$1$以上なので、この値は使わない。
・$\beta$と$\mathrm{decode}$は、定義のとおり合成で得られる。$\square$

再帰的関数の定義に関する帰納法による。$f$が零関数や後者関数の場合は補題8からいえる。射影関数の場合や、合成・最小化で得られた場合は$\mathrm{Recu}$の定義と帰納法の仮定から明らかである。
問題は$f$が$g$と$h$から原始再帰で得られた場合である。すなわち
$$ f(\vec x, 0) = g(\vec x) \qquad f(\vec x, y+1) = h(\vec x, y, f(\vec x, y)) $$
とする。ここで、列$f(\vec x, 0), f(\vec x, 1), \dots, f(\vec x, y)$のコードを$\vec x, y$から求める関数を考える。
$$ t(\vec x, y) = \mu e\Big(\mathrm{decode}(e,0) = g(\vec x) \ \wedge\ (\forall i < y)\big(\mathrm{decode}(e,i+1) = h(\vec x, i, \mathrm{decode}(e,i))\big)\Big) $$
まず、このような$e$が存在することを確認する。$i = 0, 1, \dots, y$に対して$\mathrm{decode}(e,i) = f(\vec x, i)$となる$e$が有限列コード化定理により存在し、それが上の条件を満たす。
逆に、条件を満たす$e$ならどれでも、$i = 0, 1, \dots, y$について$\mathrm{decode}(e,i) = f(\vec x, i)$となる。$i = 0$では条件の前半と$f(\vec x, 0) = g(\vec x)$から、$i$から$i+1$へは条件の後半と再帰方程式から従う（$i$についての帰納法）。条件を満たす最小の$e$である$t(\vec x, y)$も、もちろんこの性質を持つ。
次に、最小化の中身が$\mathrm{Recu}$述語であることを確認する。$g$と$h$は帰納法の仮定より$\mathrm{Recu}$に属し、$\mathrm{decode}$も補題12より$\mathrm{Recu}$に属す。等式は$\mathrm{equal}$で書けるので$\mathrm{Recu}$述語、有界全称量化子と$\wedge$は補題9,11より$\mathrm{Recu}$述語を保つ。よって$t$は$\mathrm{Recu}$に属す。
最後に
$$ f(\vec x, y) = \mathrm{decode}\big(t(\vec x, y),\ y\big) $$
となるので、$f$も$\mathrm{Recu}$に属す。$\square$

$f$が$\varphi(\vec x, y)$で表現されているとし、入力$\vec n$を一つ固定する。
手順：論理式の有限列を、もれなく一列に並べて順に調べる。調べている列が、ある$m$についての$\varphi(\overline{\vec n}, \overline{m})$の$\mathrm{PA}$での証明になっていたら、その$m$を出力して止まる。
この手順は機械的に実行できる。
・論理式の有限列は、もれなく一列に並べられる。たとえば記号に番号を付けておき、段階$s = 1, 2, 3, \dots$で「長さが$s$以下で、番号が$s$以下の記号だけを使う列」（有限個）を書き出していけば、どの列もいつかは現れる。
・与えられた列が$\mathrm{PA}$の証明かどうかは、各行が公理（$\mathrm{PA}$の公理か論理の公理）であるか、前の行から推論規則で得られるかを確かめれば判定できる。どれも形を見れば分かる。最後の行が、ある$m$について$\varphi(\overline{\vec n}, \overline{m})$の形をしているかどうかも形で分かり、そのときの$m$も読み取れる。
表現の定義から分かること：止まることと正しいことは、次の二つの事実から出る。表現の定義の$\forall y$に数項$\overline{m}$を代入すると、どの$m$についても
$$ \mathrm{PA} \vdash \overline{m} = \overline{f(\vec n)} \leftrightarrow \varphi(\overline{\vec n}, \overline{m}) $$
である。
$(\text{a})$ $m = f(\vec n)$なら、左辺は証明できるので、$\mathrm{PA} \vdash \varphi(\overline{\vec n}, \overline{m})$。
$(\text{b})$ $m \neq f(\vec n)$なら、$\mathbf{R3}$より左辺の否定が証明できるので、$\mathrm{PA} \vdash \neg\varphi(\overline{\vec n}, \overline{m})$。
止まること（停止性）： $(\text{a})$より、$\varphi(\overline{\vec n}, \overline{f(\vec n)})$の$\mathrm{PA}$での証明がある。それは並べた列のどこかに現れるので、手順は遅くともそこで止まる。
正しいこと（正当性）：手順は、それより前に別の証明を見つけて止まるかもしれない。そこで、出力される$m$が必ず$f(\vec n)$であることを示す。$m$が出力されたなら、$\mathrm{PA} \vdash \varphi(\overline{\vec n}, \overline{m})$である。もし$m \neq f(\vec n)$なら、$(\text{b})$より$\mathrm{PA} \vdash \neg\varphi(\overline{\vec n}, \overline{m})$でもあるので、$\mathrm{PA}$は矛盾する。しかし$\mathfrak{N}$は$\mathrm{PA}$のモデルなので、$\mathrm{PA}$は無矛盾である。よって$m = f(\vec n)$。
以上より、この手順はどの入力に対しても止まり、$f(\vec n)$を出力する。このような手順で計算できる関数は、Church-Turingのテーゼにより再帰的、すなわち計算可能である。$\square$

基本関数の場合

以下の論理式はどれも$\Delta_0$なので、$\Sigma_1$でも$\Pi_1$でもある。そこで$\varphi^\Sigma = \varphi^\Pi = \varphi$と取る。基本関数では、表現の条件の同値を直接示す。
足し算：$\varphi(x_1, x_2, y) \equiv (y = x_1 + x_2)$とする。$\mathbf{R1}$より$\mathrm{PA} \vdash \overline{n_1 + n_2} = \overline{n_1} + \overline{n_2}$なので、等号の推移律から
$$ \mathrm{PA} \vdash y = \overline{n_1 + n_2} \leftrightarrow y = \overline{n_1} + \overline{n_2} $$
右辺が$\varphi(\overline{n_1}, \overline{n_2}, y)$である。$y$について一般化すれば表現の条件になる。
掛け算：$\varphi(x_1, x_2, y) \equiv (y = x_1 \cdot x_2)$とし、$\mathbf{R2}$を使って同様。
射影関数：$\varphi(x_1, \dots, x_k, y) \equiv (y = x_i)$とする。$P^k_i(\vec n) = n_i$なので、示すべきは$\mathrm{PA} \vdash y = \overline{n_i} \leftrightarrow y = \overline{n_i}$であり、これは自明である。
等号の特性関数：$x_1 \neq x_2$を$\neg(x_1 = x_2)$の略記として
$$ \varphi(x_1, x_2, z) \equiv (x_1 = x_2 \wedge z = \overline{1}) \vee (x_1 \neq x_2 \wedge z = \overline{0}) $$
とする。二つの場合に分け、それぞれ同値を二段に分けて示す。
$(\text{i})$ $n_1 = n_2$のとき：$n = n_1$と書くと$\mathrm{equal}(n, n) = 1$なので、示すべきは$\mathrm{PA} \vdash z = \overline{1} \leftrightarrow \varphi(\overline{n}, \overline{n}, z)$である。
・$\mathrm{PA} \vdash z = \overline{1} \leftrightarrow (\overline{n} = \overline{n} \wedge z = \overline{1})$。$\mathrm{PA} \vdash \overline{n} = \overline{n}$だからである。
・$\mathrm{PA} \vdash (\overline{n} = \overline{n} \wedge z = \overline{1}) \leftrightarrow \varphi(\overline{n}, \overline{n}, z)$。$\to$は選言の導入で明らか。$\leftarrow$は、第二の選言肢が否定できることによる。実際、$\mathrm{PA} \vdash \overline{n} = \overline{n}$から、二重否定で$\mathrm{PA} \vdash \neg(\overline{n} \neq \overline{n})$、選言導入で$\mathrm{PA} \vdash \neg(\overline{n} \neq \overline{n}) \vee \neg(z = \overline{0})$、De Morganで$\mathrm{PA} \vdash \neg(\overline{n} \neq \overline{n} \wedge z = \overline{0})$となる。あとはトートロジー$(A \vee B) \wedge \neg B \to A$を使えばよい。
$(\text{ii})$ $n_1 \neq n_2$のとき：$\mathrm{equal}(n_1, n_2) = 0$なので、示すべきは$\mathrm{PA} \vdash z = \overline{0} \leftrightarrow \varphi(\overline{n_1}, \overline{n_2}, z)$である。
・$\mathrm{PA} \vdash z = \overline{0} \leftrightarrow (\overline{n_1} \neq \overline{n_2} \wedge z = \overline{0})$。$\mathbf{R3}$より$\mathrm{PA} \vdash \overline{n_1} \neq \overline{n_2}$だからである。
・$\mathrm{PA} \vdash (\overline{n_1} \neq \overline{n_2} \wedge z = \overline{0}) \leftrightarrow \varphi(\overline{n_1}, \overline{n_2}, z)$。$(\text{i})$と同様で、今度は$\mathrm{PA} \vdash \overline{n_1} \neq \overline{n_2}$から、選言導入とDe Morganで第一の選言肢$\overline{n_1} = \overline{n_2} \wedge z = \overline{1}$が否定できる。
どちらの場合も、最後に$z$について一般化すればよい。

合成の場合

記号を簡単にするため$f(\vec x) = h(g(\vec x))$とする（一般の$f(\vec x) = h(g_1(\vec x),\dots,g_l(\vec x))$でも議論は同じである）。
帰納法の仮定より、$g$に対して$\psi^\Sigma$,$\psi^\Pi$が、$h$に対して$\chi^\Sigma$,$\chi^\Pi$が取れて、任意の$\vec n$,$k$について
$$ \mathrm{PA} \vdash \forall y\big(y = \overline{g(\vec n)} \leftrightarrow \psi^\Sigma(\overline{\vec n},y)\big) \qquad \mathrm{PA} \vdash \forall y\big(y = \overline{g(\vec n)} \leftrightarrow \psi^\Pi(\overline{\vec n},y)\big) $$
$$ \mathrm{PA} \vdash \forall y\big(y = \overline{h(k)} \leftrightarrow \chi^\Sigma(\overline{k},y)\big) \qquad \mathrm{PA} \vdash \forall y\big(y = \overline{h(k)} \leftrightarrow \chi^\Pi(\overline{k},y)\big) $$
が成り立つとする。そこで
$$ \varphi^\Sigma(\vec x,y) \equiv \exists z\big(\psi^\Sigma(\vec x,z) \wedge \chi^\Sigma(z,y)\big) $$
$$ \varphi^\Pi(\vec x,y) \equiv \forall z\big(\psi^\Sigma(\vec x,z) \to \chi^\Pi(z,y)\big) $$
と定める（$\psi^\Pi$はここでは使わない）。
$\vec n$を固定し、$k = g(\vec n)$,$m = h(k)$とおく。このとき$f(\vec n) = m$である。帰納法の仮定に証明の方針の$(\text{a})$,$(\text{b})$を当てはめると、次の四つが得られる。
$(\text{g1})$ $\mathrm{PA} \vdash \psi^\Sigma(\overline{\vec n}, \overline{k})$
$(\text{g2})$ $\mathrm{PA} \vdash \psi^\Sigma(\overline{\vec n}, z) \to z = \overline{k}$
$(\text{h1})$ $\mathrm{PA} \vdash \chi^\Sigma(\overline{k}, \overline{m})$、$\mathrm{PA} \vdash \chi^\Pi(\overline{k}, \overline{m})$
$(\text{h2})$ $\mathrm{PA} \vdash \chi^\Sigma(\overline{k}, y) \to y = \overline{m}$、$\mathrm{PA} \vdash \chi^\Pi(\overline{k}, y) \to y = \overline{m}$
$(\to)$の向き：
・$\varphi^\Sigma$について：$(\text{g1})$と$(\text{h1})$より$\mathrm{PA} \vdash \psi^\Sigma(\overline{\vec n}, \overline{k}) \wedge \chi^\Sigma(\overline{k}, \overline{m})$。存在導入で
$$ \mathrm{PA} \vdash \exists z\big(\psi^\Sigma(\overline{\vec n}, z) \wedge \chi^\Sigma(z, \overline{m})\big) $$
すなわち$\mathrm{PA} \vdash \varphi^\Sigma(\overline{\vec n}, \overline{m})$。
・$\varphi^\Pi$について：$(\text{g2})$と$(\text{h1})$から、等号の代入で$\mathrm{PA} \vdash \psi^\Sigma(\overline{\vec n}, z) \to \chi^\Pi(z, \overline{m})$。$z$について一般化して
$$ \mathrm{PA} \vdash \forall z\big(\psi^\Sigma(\overline{\vec n}, z) \to \chi^\Pi(z, \overline{m})\big) $$
すなわち$\mathrm{PA} \vdash \varphi^\Pi(\overline{\vec n}, \overline{m})$。
$(\leftarrow)$の向き：
・$\varphi^\Sigma$について：$(\text{h2})$と等号の代入から$\mathrm{PA} \vdash z = \overline{k} \wedge \chi^\Sigma(z, y) \to y = \overline{m}$。これと$(\text{g2})$を合わせて
$$ \mathrm{PA} \vdash \psi^\Sigma(\overline{\vec n}, z) \wedge \chi^\Sigma(z, y) \to y = \overline{m} $$
$z$は$y = \overline{m}$に自由に現れないので、存在除去により$\mathrm{PA} \vdash \exists z\big(\psi^\Sigma(\overline{\vec n}, z) \wedge \chi^\Sigma(z, y)\big) \to y = \overline{m}$、すなわち$\mathrm{PA} \vdash \varphi^\Sigma(\overline{\vec n}, y) \to y = \overline{m}$。
・$\varphi^\Pi$について：$\varphi^\Pi(\overline{\vec n}, y)$の$\forall z$に$\overline{k}$を代入して
$$ \mathrm{PA} \vdash \varphi^\Pi(\overline{\vec n}, y) \to \big(\psi^\Sigma(\overline{\vec n}, \overline{k}) \to \chi^\Pi(\overline{k}, y)\big) $$
$(\text{g1})$より内側の前件は証明できるので、$\mathrm{PA} \vdash \varphi^\Pi(\overline{\vec n}, y) \to \chi^\Pi(\overline{k}, y)$。これと$(\text{h2})$を合わせて$\mathrm{PA} \vdash \varphi^\Pi(\overline{\vec n}, y) \to y = \overline{m}$。
複雑さ：$\varphi^\Sigma$が$\mathrm{PA}$上で$\Sigma_1$であることは、$\psi^\Sigma$と$\chi^\Sigma$を同値な$\Sigma_1$論理式に置き換えて、存在量化子を前に出せば分かる。$\varphi^\Pi$では、$\psi^\Sigma$が「ならば」の前件に置かれている。$A \to B$は$\neg A \vee B$と同値なので、前件は否定の下にあるのと同じである。$\Pi_1$版を作るときは否定の下に$\Sigma_1$版を置く、という方針どおりである。実際、$\psi^\Sigma$と同値な$\Sigma_1$論理式を$\exists \vec w \theta$（$\theta$は$\Delta_0$）と書けば
$$ \varphi^\Pi(\vec x,y) \leftrightarrow \forall z \forall \vec w\big(\theta(\vec x,z,\vec w) \to \chi^\Pi(z,y)\big) $$
となり、$\chi^\Pi$と同値な$\Pi_1$論理式の先頭の全称量化子も前に出せるので、$\varphi^\Pi$は$\mathrm{PA}$上で$\Pi_1$である。

最小化の場合

$f(\vec x) = \mu y[g(\vec x,y) = 0]$とする。帰納法の仮定より$g$に対して$\psi^\Sigma$,$\psi^\Pi$が取れて、任意の$\vec n$,$k$について
$$ \mathrm{PA} \vdash \forall w\big(w = \overline{g(\vec n,k)} \leftrightarrow \psi^\Sigma(\overline{\vec n},\overline{k},w)\big) $$
$$ \mathrm{PA} \vdash \forall w\big(w = \overline{g(\vec n,k)} \leftrightarrow \psi^\Pi(\overline{\vec n},\overline{k},w)\big) $$
が成り立つとする（$\psi$の最後の変数が$g$の値である）。そこで
$$ \varphi^\Sigma(\vec x,y) \equiv \psi^\Sigma(\vec x,y,\overline{0}) \wedge \forall z< y\ \neg\psi^\Pi(\vec x,z,\overline{0}) $$
$$ \varphi^\Pi(\vec x,y) \equiv \psi^\Pi(\vec x,y,\overline{0}) \wedge \forall z< y\ \neg\psi^\Sigma(\vec x,z,\overline{0}) $$
と定める。否定の下に置かれる論理式の階層が入れ替わっていることに注目してほしい。これが証明の方針で述べた工夫である。
$\vec n$を固定し、$m = f(\vec n)$とおく。これは、$g(\vec n,m) = 0$かつ、すべての$k < m$について$g(\vec n,k) \neq 0$、ということである。$g(\vec n, z) = 0$となる$z$を$g(\vec n, \cdot)$の零点と呼べば、$m$は最小の零点である。
以下、$\psi$は$\psi^\Sigma$と$\psi^\Pi$のどちらを表してもよい。帰納法の仮定から、次の二つが得られる。
$(\text{m1})$ $\mathrm{PA} \vdash \psi(\overline{\vec n}, \overline{m}, \overline{0})$
$(\text{m2})$ $\mathrm{PA} \vdash \forall z < \overline{m}\ \neg\psi(\overline{\vec n}, z, \overline{0})$
$(\text{m1})$は、$g(\vec n, m) = 0$に証明の方針の$(\text{a})$を当てはめたものである。$(\text{m2})$は二段で示す。
・各$k < m$について、$g(\vec n, k) \neq 0$である。そこで証明の方針の$(\text{c})$を、入力$(\vec n, k)$、$j = g(\vec n, k)$、$i = 0$として当てはめると、$\mathrm{PA} \vdash \neg\psi(\overline{\vec n}, \overline{k}, \overline{0})$。ここで$\mathbf{R3}$が働く。
・補題2の$(1)$より$\mathrm{PA} \vdash z < \overline{m} \to (z = \overline{0} \vee \cdots \vee z = \overline{m-1})$。各選言肢$z = \overline{k}$からは、等号の代入と一段目から$\neg\psi(\overline{\vec n}, z, \overline{0})$が出る。よって$\mathrm{PA} \vdash z < \overline{m} \to \neg\psi(\overline{\vec n}, z, \overline{0})$であり、$z$について一般化すれば$(\text{m2})$になる。
一段目で得られるのは「$0$は零点でない」「$1$は零点でない」…「$m-1$は零点でない」にあたる有限個の主張で、二段目はそれを一つの有界量化の文にまとめる操作である。
$(\to)$の向き：$(\text{m1})$の$\psi^\Sigma$版と$(\text{m2})$の$\psi^\Pi$版を並べれば
$$ \mathrm{PA} \vdash \psi^\Sigma(\overline{\vec n}, \overline{m}, \overline{0}) \wedge \forall z < \overline{m}\ \neg\psi^\Pi(\overline{\vec n}, z, \overline{0}) $$
すなわち$\mathrm{PA} \vdash \varphi^\Sigma(\overline{\vec n}, \overline{m})$である。$\Sigma$と$\Pi$を入れ替えれば、同じく$\mathrm{PA} \vdash \varphi^\Pi(\overline{\vec n}, \overline{m})$。
$(\leftarrow)$の向き：$\varphi^\Sigma$について示す。方針は、$y$が$\overline{m}$より大きくも小さくもないことを示し、三分律で$y = \overline{m}$を導くことである。
・$\overline{m} < y$を否定する：$\forall z< y\ \neg\psi^\Pi(\overline{\vec n},z,\overline{0})$の$z$に$\overline{m}$を代入すると
$$ \mathrm{PA} \vdash \forall z< y\ \neg\psi^\Pi(\overline{\vec n},z,\overline{0}) \wedge \overline{m} < y \to \neg\psi^\Pi(\overline{\vec n},\overline{m},\overline{0}) $$
一方、$(\text{m1})$より$\mathrm{PA} \vdash \psi^\Pi(\overline{\vec n},\overline{m},\overline{0})$である。トートロジー$(A \wedge B \to \neg C) \wedge C \to (A \to \neg B)$により
$$ \mathrm{PA} \vdash \forall z< y\ \neg\psi^\Pi(\overline{\vec n},z,\overline{0}) \to \neg(\overline{m} < y) \tag{$*$} $$
直観的には、「$y$より小さい数はどれも零点でないのに、$m$は零点である。だから$m$は$y$より小さくない」ということである。
・$y < \overline{m}$を否定する：$(\text{m2})$の$\psi^\Sigma$版の$z$に$y$を代入すると、$\mathrm{PA} \vdash y < \overline{m} \to \neg\psi^\Sigma(\overline{\vec n},y,\overline{0})$。対偶を取って
$$ \mathrm{PA} \vdash \psi^\Sigma(\overline{\vec n},y,\overline{0}) \to \neg(y < \overline{m}) \tag{$**$} $$
直観的には、「$y$は零点だが、$m$より小さい数は零点でない。だから$y$は$m$より小さくない」ということである。
・$(*)$と$(**)$を合わせると
$$ \mathrm{PA} \vdash \varphi^\Sigma(\overline{\vec n},y) \to \big(\neg(\overline{m} < y) \wedge \neg(y < \overline{m})\big) $$
他方、補題2の$(2)$より$\mathrm{PA} \vdash y < \overline{m} \vee y = \overline{m} \vee \overline{m} < y$である（三分律）。これらを合わせて
$$ \mathrm{PA} \vdash \varphi^\Sigma(\overline{\vec n},y) \to y = \overline{m} $$
$\varphi^\Pi$についても、$\Sigma$と$\Pi$の役割を入れ替えれば同じ議論が通る。
複雑さ：$\varphi^\Pi$が$\mathrm{PA}$上で$\Pi_1$であることは、$\neg\psi^\Sigma$が$\Pi_1$と同値であり、$\Pi_1$論理式の連言と有界全称量化がふたたび$\Pi_1$と同値になることから分かる（$\forall z< y\ \forall w \theta$は$\forall w\ \forall z< y\ \theta$と論理的に同値である）。
$\varphi^\Sigma$のほうは事情が違う。第二の連言肢$\forall z< y\ \neg\psi^\Pi$では、$\Sigma_1$と同値な$\neg\psi^\Pi$の前に有界全称量化子が付いている。これを$\Sigma_1$の形に直すには
$$ \forall z< y\ \exists w\ \theta(z,w) \leftrightarrow \exists W\ \forall z< y\ \exists w< W\ \theta(z,w) $$
という書き換えが必要になる（右から左は明らか、左から右は「有限個の証人の最大値を取る」という操作で、収集原理と呼ばれる）。これは論理だけでは出てこないが$\mathrm{PA}$では証明できる。したがって$\varphi^\Sigma$は$\mathrm{PA}$上で$\Sigma_1$である。表現定理の証明で、$\mathrm{Q}$の公理を超えて$\mathrm{PA}$の帰納法を使うのはこの一箇所だけであり、その意味は「$\mathrm{R}$での表現可能性」で論じる。
以上で表現定理の証明が完成した。$\square$

述語$P$の特性関数$P^{\circ}$が論理式$\varphi(\vec x,y)$で表現されているとする。このとき$P$は$\varphi(\vec x,\overline{1})$で表現される。
実際、$P(\vec n)$が成り立つときは$P^{\circ}(\vec n) = 1$なので、証明の方針の$(\text{a})$より$\mathrm{PA} \vdash \varphi(\overline{\vec n},\overline{1})$。成り立たないときは$P^{\circ}(\vec n) = 0 \neq 1$なので、証明の方針の$(\text{c})$より$\mathrm{PA} \vdash \neg\varphi(\overline{\vec n},\overline{1})$。$\square$

証明の方針から最小化の場合の議論で、$\mathrm{PA}$を$\mathrm{R}$に置き換え、$\Sigma$版と$\Pi$版のペアを一つの論理式に置き換えるだけでよい。各節の「複雑さ」の段落は使わない。証明の方針の$(\to)$と$(\leftarrow)$による確かめ方も、帰納法の仮定から取り出す$(\text{a})$, $(\text{b})$, $(\text{c})$も、$\mathrm{R}$でそのまま成り立つ（$(\text{c})$で使うのは$\mathbf{R3}$だけである）。そこで、$f$に対して単一の論理式$\varphi_f$を次のように作る。
基本関数：基本関数の場合とまったく同じ$\Delta_0$論理式を使う。そこで用いたのは$\mathbf{R1}$, $\mathbf{R2}$, $\mathbf{R3}$だけである。
合成：$f(\vec x) = h(g(\vec x))$に対して
$$ \varphi_f(\vec x,y) \equiv \exists z\big(\varphi_g(\vec x,z) \wedge \varphi_h(z,y)\big) $$
とする。合成の場合の$\varphi^\Sigma$についての議論で、$\psi^\Sigma$を$\varphi_g$に、$\chi^\Sigma$を$\varphi_h$に読み替えればよい（$(\text{g1})$, $(\text{g2})$, $(\text{h1})$, $(\text{h2})$も同じく読み替える）。そこでは順序についての性質を一切使っていない。
最小化：$f(\vec x) = \mu y[g(\vec x,y)=0]$に対して
$$ \varphi_f(\vec x,y) \equiv \varphi_g(\vec x,y,\overline{0}) \wedge \forall z< y\ \neg\varphi_g(\vec x,z,\overline{0}) $$
とする。最小化の場合の議論で、$\psi^\Sigma$と$\psi^\Pi$をともに$\varphi_g$に置き換えればよい。$(\text{m1})$と$(\text{m2})$、$(\to)$の向き、$(*)$と$(**)$の導出、最後の場合分けは、そのまま通る。使うのは、$(\text{m2})$での$\mathbf{R3}$（証明の方針の$(\text{c})$を通して）と$\mathbf{R4}$（補題2の$(1)$を通して）、最後の場合分けでの$\mathbf{R5}$（補題2の$(2)$を通して）である。
どの段階でも$\mathrm{PA}$の帰納法は使っていない。関係の場合も系：関係の場合と同じで、そこで使った$(\text{a})$と$(\text{c})$は$\mathrm{R}$でも成り立つ。$\square$