[proofplan] We prove the closed soundness statement by proving a stronger uniform soundness lemma for derivations with free variables and undischarged assumptions. The lemma assigns to each natural-deduction derivation a partial recursive operation which transforms realizers of the assumptions, under any numerical assignment to the free variables, into a realizer of the conclusion. The logical rules are verified by the recursive clauses in the definition of Kleene realizability, implication and universal introduction use the $s$-$m$-$n$ theorem, and the induction schema is realized by primitive recursion. The stated theorem is then the special case with no free variables and no assumptions. [/proofplan]

[step:Fix the realizability convention and the uniform form of soundness] We use the following standard form of Kleene realizability. Let $\varphi_e$ denote the unary partial recursive function with index $e \in \mathbb{N}$, and let $\langle \cdot,\cdot\rangle:\mathbb{N}^2 \to \mathbb{N}$ be a fixed primitive recursive pairing function with primitive recursive projections $\pi_0,\pi_1:\mathbb{N}\to\mathbb{N}$. All finite tuples and all multi-argument partial recursive functions are represented through a fixed primitive recursive coding of finite sequences; in particular, notation such as $\varphi_q(a_1,\dots,a_m,d_1,\dots,d_r)$ abbreviates unary evaluation of $\varphi_q$ on the code of that tuple. We write $\varphi_e(n)\downarrow$ to mean that the computation of $\varphi_e$ on input $n$ halts, and we write $\varphi_e(n)\simeq \varphi_f(n)$ to mean that the two partial computations are Kleene-equal, namely either both are undefined or both are defined with the same value. For a closed atomic formula $R$ of arithmetic, a number $e$ realizes $R$, written $e \Vdash R$, exactly when $R$ is true in the standard structure $\mathbb{N}$. If the language includes a primitive absurdity constant $\bot$, no natural number realizes $\bot$; if negation is used, $\neg B$ is treated as the abbreviation $B\to\bot$. For compound closed formulas, realizability is defined recursively as follows: \begin{align*} e \Vdash B \wedge C \quad \text{iff} \quad \pi_0(e) \Vdash B \text{ and } \pi_1(e) \Vdash C. \end{align*} \begin{align*} e \Vdash B \vee C \quad \text{iff} \quad \pi_0(e)=0 \text{ and } \pi_1(e)\Vdash B, \text{ or } \pi_0(e)=1 \text{ and } \pi_1(e)\Vdash C. \end{align*} \begin{align*} e \Vdash B \to C \quad \text{iff} \quad \text{for every } d \in \mathbb{N}, \ d \Vdash B \text{ implies } \varphi_e(d)\downarrow \text{ and } \varphi_e(d)\Vdash C. \end{align*} \begin{align*} e \Vdash \forall x\,B(x) \quad \text{iff} \quad \text{for every } n \in \mathbb{N}, \ \varphi_e(n)\downarrow \text{ and } \varphi_e(n)\Vdash B(\bar n). \end{align*} \begin{align*} e \Vdash \exists x\,B(x) \quad \text{iff} \quad \pi_1(e)\Vdash B(\overline{\pi_0(e)}). \end{align*} For an open formula $D(x_1,\dots,x_m)$ and a numerical assignment $a=(a_1,\dots,a_m)\in\mathbb{N}^m$, write $D[a]$ for the closed formula obtained by substituting the numeral $\bar a_i$ for $x_i$. We prove the following uniform lemma: if there is a derivation in $\mathrm{HA}$ of $C(x_1,\dots,x_m)$ from assumptions $B_1(x_1,\dots,x_m),\dots,B_r(x_1,\dots,x_m)$, then there is an index $q\in\mathbb{N}$ of a partial recursive function \begin{align*} \varphi_q:\mathbb{N}^{m+r} \rightharpoonup \mathbb{N} \end{align*} such that, for every $a=(a_1,\dots,a_m)\in\mathbb{N}^m$ and every $d_1,\dots,d_r\in\mathbb{N}$, if $d_i \Vdash B_i[a]$ for all $1\le i\le r$, then \begin{align*} \varphi_q(a_1,\dots,a_m,d_1,\dots,d_r)\downarrow \end{align*} and \begin{align*} \varphi_q(a_1,\dots,a_m,d_1,\dots,d_r)\Vdash C[a]. \end{align*} [/step]

[step:Prove the uniform lemma by induction on the derivation]We argue by induction on the given natural-deduction derivation. The assumption rule is realized by the projection map \begin{align*} P_j:\mathbb{N}^{m+r}\to\mathbb{N}, \qquad (a_1,\dots,a_m,d_1,\dots,d_r)\mapsto d_j, \end{align*} which is primitive recursive. If the last line is a quantifier-free true atomic defining equation, then after substituting numerals according to an assignment $a\in\mathbb{N}^m$ it is a closed atomic formula true in the standard model $\mathbb{N}$, and hence any fixed number, say $0$, realizes it by the atomic clause. The corresponding constant map \begin{align*} K_0:\mathbb{N}^{m+r}\to\mathbb{N}, \qquad (a_1,\dots,a_m,d_1,\dots,d_r)\mapsto 0, \end{align*} is primitive recursive. For each non-atomic non-induction arithmetic or equality axiom schema in the chosen presentation of $\mathrm{HA}$, the formalized statement assumes the standard uniform Kleene realizer for its closed numerical instances; applying that primitive-recursive realizer-producing operation to the numerical parameters in $a$ gives the required base-case realizer. The induction axioms are handled separately below. For conjunction introduction, the induction hypothesis gives recursive realizers $u$ for $B[a]$ and $v$ for $C[a]$ from the same data. The map sending the data to $\langle u,v\rangle$ is partial recursive by closure under composition and realizes $B[a]\wedge C[a]$. Conjunction elimination is realized by composing the realizer of $B[a]\wedge C[a]$ with $\pi_0$ or $\pi_1$. Disjunction introduction is realized by sending a realizer $u$ of $B[a]$ to $\langle 0,u\rangle$, or a realizer $v$ of $C[a]$ to $\langle 1,v\rangle$. For [disjunction elimination](/theorems/4625), suppose the induction hypotheses give a realizer $w$ of $B[a]\vee C[a]$, a recursive operation sending a realizer of $B[a]$ to a realizer of $D[a]$, and a recursive operation sending a realizer of $C[a]$ to a realizer of $D[a]$. Define the case-analysis operation \begin{align*} E:\mathbb{N}^{m+r}\rightharpoonup\mathbb{N} \end{align*} by first computing $w$, then computing $\pi_0(w)$ and $\pi_1(w)$, and finally applying the left branch when $\pi_0(w)=0$ and the right branch when $\pi_0(w)=1$. This is partial recursive by composition and primitive recursive case distinction. Since $w\Vdash B[a]\vee C[a]$, one of these two cases holds, and the corresponding branch returns a realizer of $D[a]$.[/step]

[guided]The induction hypothesis is stronger than the closed theorem because it tracks the data needed for open derivations. At a derivation line with free variables $x_1,\dots,x_m$ and assumptions $B_1,\dots,B_r$, the recursive operation receives two kinds of input: first the numerical assignment $a_1,\dots,a_m$, and then realizers $d_1,\dots,d_r$ of the assumptions under that assignment. The goal is always to compute a realizer of the conclusion under the same assignment. The assumption rule is the simplest test of this formulation. If the conclusion is the assumption $B_j$, then the input already contains a realizer $d_j\Vdash B_j[a]$. The realizing operation is therefore the projection \begin{align*} P_j:\mathbb{N}^{m+r}\to\mathbb{N}, \qquad (a_1,\dots,a_m,d_1,\dots,d_r)\mapsto d_j. \end{align*} This map is primitive recursive, so it has an index among the partial recursive functions, and it returns exactly the required realizer. For quantifier-free true atomic defining equations, the key point is the atomic convention. A closed true atomic formula is realized by every natural number. Each such defining equation of the primitive recursive symbols of $\mathrm{HA}$ is true in the standard structure $\mathbb{N}$ after substituting numerals for the free variables. Hence the constant operation \begin{align*} K_0:\mathbb{N}^{m+r}\to\mathbb{N}, \qquad (a_1,\dots,a_m,d_1,\dots,d_r)\mapsto 0 \end{align*} realizes those atomic axiom instances. For the non-atomic equality, successor, and other non-induction arithmetic axiom schemata in the chosen presentation, the theorem statement supplies the standard uniform Kleene realizers. The corresponding base-case operation is obtained by applying the primitive-recursive realizer-producing function for that axiom schema to the numerical parameters in the assignment $a$. The connectives are then handled exactly as their realizability clauses prescribe. If we have computed $u\Vdash B[a]$ and $v\Vdash C[a]$, the pair $\langle u,v\rangle$ realizes $B[a]\wedge C[a]$ because its first projection realizes $B[a]$ and its second projection realizes $C[a]$. Conversely, from $w\Vdash B[a]\wedge C[a]$, the primitive recursive projection $\pi_0(w)$ realizes $B[a]$ and $\pi_1(w)$ realizes $C[a]$. For disjunction, the first component is a tag. A realizer of $B[a]$ becomes a realizer of $B[a]\vee C[a]$ by forming $\langle 0,u\rangle$, and a realizer of $C[a]$ becomes a realizer of $B[a]\vee C[a]$ by forming $\langle 1,v\rangle$. In disjunction elimination, the computed realizer $w$ of $B[a]\vee C[a]$ contains both the tag $\pi_0(w)$ and the payload $\pi_1(w)$. If the tag is $0$, the payload realizes $B[a]$, so the left branch of the derivation gives a realizer of $D[a]$. If the tag is $1$, the payload realizes $C[a]$, so the right branch gives a realizer of $D[a]$. Primitive recursive case distinction lets a single partial recursive operation implement exactly this branch selection.[/guided]

[step:Realize implication rules using indices for computed functions] For implication elimination, suppose the induction hypotheses produce $u\Vdash B[a]\to C[a]$ and $v\Vdash B[a]$. By the definition of realizability for implication, $\varphi_u(v)\downarrow$ and $\varphi_u(v)\Vdash C[a]$. The operation which computes $u$, computes $v$, and then evaluates $\varphi_u(v)$ is partial recursive by closure under composition and universal evaluation for partial recursive functions. For implication introduction, suppose the last rule discharges an additional assumption $B$ and derives $C$. By the induction hypothesis, there is an index $q$ such that \begin{align*} \varphi_q(a_1,\dots,a_m,d_1,\dots,d_r,b)\Vdash C[a] \end{align*} whenever $b\Vdash B[a]$ and the $d_i$ realize the open assumptions. By the $s$-$m$-$n$ theorem applied to the fixed coding of tuples, there is a primitive recursive function \begin{align*} S:\mathbb{N}^{m+r}\to\mathbb{N} \end{align*} such that, for every $b\in\mathbb{N}$, \begin{align*} \varphi_{S(a_1,\dots,a_m,d_1,\dots,d_r)}(b) \simeq \varphi_q(a_1,\dots,a_m,d_1,\dots,d_r,b). \end{align*} The uniformity condition required here is exactly that the already-fixed parameters $a_1,\dots,a_m,d_1,\dots,d_r$ are coded effectively and left as parameters while the last argument $b$ remains the input to the resulting unary partial recursive function. Thus $S(a_1,\dots,a_m,d_1,\dots,d_r)$ realizes $B[a]\to C[a]$. [/step]

[step:Track numerical parameters through the quantifier rules] For universal elimination, suppose $u\Vdash \forall x\,B(x,a)$. If $t(x_1,\dots,x_m)$ is an arithmetic term, let \begin{align*} t_{\mathbb{N}}:\mathbb{N}^m\to\mathbb{N} \end{align*} be the primitive recursive function interpreting $t$ in $\mathbb{N}$. Then $\varphi_u(t_{\mathbb{N}}(a))$ is defined and realizes $B(\overline{t_{\mathbb{N}}(a)},a)$ by the universal clause. For universal introduction, suppose the derivation gives $B(y,a)$ and $y$ is not free in any undischarged assumption. By the induction hypothesis, there is an index $q$ whose computation on inputs $(a,n,d_1,\dots,d_r)$ realizes $B(\bar n,a)$ whenever the $d_i$ realize the assumptions under $a$. Since $y$ is not free in the assumptions, the same $d_i$ realize those assumptions for every $n\in\mathbb{N}$. By the $s$-$m$-$n$ theorem applied to the fixed coding of tuples, we obtain a recursive operation which, from $(a,d_1,\dots,d_r)$, returns an index $u$ such that \begin{align*} \varphi_u(n)\simeq \varphi_q(a,n,d_1,\dots,d_r) \end{align*} for every $n\in\mathbb{N}$. The eigenvariable condition is used here to ensure that the assumption realizers $d_1,\dots,d_r$ do not depend on the newly varied numerical input $n$. Hence $u\Vdash \forall y\,B(y,a)$. For existential introduction, suppose the induction hypothesis gives $v\Vdash B(\overline{t_{\mathbb{N}}(a)},a)$. Then \begin{align*} \langle t_{\mathbb{N}}(a),v\rangle \Vdash \exists y\,B(y,a) \end{align*} by the existential clause. For existential elimination, suppose $w\Vdash \exists y\,B(y,a)$. The natural-deduction eigenvariable condition says that the witness variable $y$ is not free in the conclusion $D$ and is not free in any undischarged assumption except the temporary assumption $B(y,a)$. Therefore the realizers $d_1,\dots,d_r$ for the open assumptions under $a$ remain the same for every numerical value assigned to $y$, and the conclusion has the closed instance $D[a]$ independent of that value. The induction hypothesis for the subderivation gives a recursive operation which transforms a witness $n$ and a realizer of $B(\bar n,a)$ into a realizer of $D[a]$. Since $\pi_0(w)$ is the witness and $\pi_1(w)\Vdash B(\overline{\pi_0(w)},a)$, applying that operation to $\pi_0(w)$ and $\pi_1(w)$ yields a realizer of $D[a]$. [/step]

[step:Realize the induction schema by primitive recursion] Let $B(x,a)$ be a formula with displayed induction variable $x$ and remaining parameters $a=(a_1,\dots,a_m)$. An instance of the induction schema has the form \begin{align*} B(0,a)\to \bigl(\forall x\,(B(x,a)\to B(x+1,a))\bigr)\to \forall x\,B(x,a). \end{align*} We define a partial recursive function \begin{align*} R:\mathbb{N}^3\rightharpoonup\mathbb{N} \end{align*} by primitive recursion in the third argument: \begin{align*} R(b,s,0) \simeq b. \end{align*} \begin{align*} R(b,s,n+1) \simeq \varphi_{\varphi_s(n)}(R(b,s,n)). \end{align*} Closure of partial recursive functions under primitive recursion and composition gives an index for $R$ (citing a result not yet in the wiki: closure of partial recursive functions under primitive recursion and composition). Fix $b,s\in\mathbb{N}$ such that $b\Vdash B(0,a)$ and $s\Vdash \forall x\,(B(x,a)\to B(x+1,a))$. We prove by induction on $n\in\mathbb{N}$ that $R(b,s,n)\downarrow$ and $R(b,s,n)\Vdash B(\bar n,a)$. For $n=0$, this is the defining equation $R(b,s,0)\simeq b$ and the assumption on $b$. If the assertion holds at $n$, then $s\Vdash \forall x\,(B(x,a)\to B(x+1,a))$ implies $\varphi_s(n)\downarrow$ and \begin{align*} \varphi_s(n)\Vdash B(\bar n,a)\to B(\overline{n+1},a). \end{align*} Applying this implication realizer to $R(b,s,n)\Vdash B(\bar n,a)$ gives \begin{align*} \varphi_{\varphi_s(n)}(R(b,s,n))\downarrow \end{align*} and \begin{align*} \varphi_{\varphi_s(n)}(R(b,s,n))\Vdash B(\overline{n+1},a). \end{align*} By the recursive definition of $R$, this is exactly $R(b,s,n+1)$. Therefore $R(b,s,n)\Vdash B(\bar n,a)$ for every $n\in\mathbb{N}$. Using the $s$-$m$-$n$ theorem once more, first fix $b$ as a parameter in the partial recursive map $(b,s,n)\mapsto R(b,s,n)$, and then fix $s$ as a parameter in the resulting binary map. Thus there is an index $e_{\mathrm{ind}}$ for a unary partial recursive function with the following curried behaviour: for every $b\in\mathbb{N}$, $\varphi_{e_{\mathrm{ind}}}(b)$ is defined and is an index for a unary partial recursive function such that, for every $s\in\mathbb{N}$, $\varphi_{\varphi_{e_{\mathrm{ind}}}(b)}(s)$ is defined and is an index for the map \begin{align*} n\mapsto R(b,s,n). \end{align*} If $b\Vdash B(0,a)$, then $\varphi_{e_{\mathrm{ind}}}(b)$ realizes \begin{align*} \bigl(\forall x\,(B(x,a)\to B(x+1,a))\bigr)\to \forall x\,B(x,a). \end{align*} If also $s\Vdash \forall x\,(B(x,a)\to B(x+1,a))$, then the index $\varphi_{\varphi_{e_{\mathrm{ind}}}(b)}(s)$ realizes $\forall x\,B(x,a)$ by the induction on $n$ just proved. Hence $e_{\mathrm{ind}}$ realizes the curried implication \begin{align*} B(0,a)\to \bigl(\forall x\,(B(x,a)\to B(x+1,a))\bigr)\to \forall x\,B(x,a). \end{align*} [/step]

[step:Specialize the uniform lemma to a closed theorem] Let $A$ be a closed sentence and suppose $\mathrm{HA}\vdash A$. Apply the uniform lemma to the derivation of $A$ with $m=0$ free variables and $r=0$ undischarged assumptions. We obtain an index $q\in\mathbb{N}$ of a nullary partial recursive computation such that \begin{align*} \varphi_q()\downarrow \end{align*} and its value realizes $A$. Let \begin{align*} e:=\varphi_q(). \end{align*} Then $e\in\mathbb{N}$ and $e\Vdash A$, which is the desired conclusion. [/step]