[proofplan] We prove the stronger open-context soundness theorem: from a derivation of $A$ under assumptions $A_1,\ldots,A_k$, one constructs a term realizing $A$ from variables realizing the assumptions. The proof is by induction on the given derivation, interpreting the logical rules by the corresponding product, sum, function, and witness-pair operations in the stated term calculus. The non-logical axioms are handled exactly because the theorem has restricted equality to intensional equality and primitive-recursive defining equations, all of which are atomic after expansion. The induction rule is interpreted by primitive recursion at the realizer type, and the resulting correctness assertion is proved by internal induction on an admissible formula of $\mathrm{HA}^{\omega}_{\mathrm{int}}$. [/proofplan]

[step:Prove open-context soundness by derivation induction] Let $\Gamma$ be the finite list $A_1,\ldots,A_k$. For each $i$, introduce a fresh realizer variable $x_i:|A_i|$, and let $X$ denote the tuple $(x_1,\ldots,x_k)$. Write $X\Vdash_{\mathrm{mr}}\Gamma$ for the iterated conjunction of the formulas $x_i\Vdash_{\mathrm{mr}}A_i$. We prove by induction on derivations that, whenever $\Gamma\vdash A$, there is a term $R_A:|A|$, whose free realizer variables are among $x_1,\ldots,x_k$ and whose other free variables are among the object variables of the derivation, such that \begin{align*} \mathrm{HA}^{\omega}_{\mathrm{int}}\vdash (X\Vdash_{\mathrm{mr}}\Gamma)\to R_A\Vdash_{\mathrm{mr}}A. \end{align*} The expression on the left is read as the corresponding iterated intuitionistic implication from the assumptions $x_i\Vdash_{\mathrm{mr}}A_i$. [/step]

[step:Realize assumptions and structural rules] If the last rule selects the assumption $A_i$ from $\Gamma$, take $R_A:=x_i$. From $X\Vdash_{\mathrm{mr}}\Gamma$, intuitionistic conjunction elimination gives $x_i\Vdash_{\mathrm{mr}}A_i$. Weakening, exchange, and contraction act only on the list of realizer variables. Weakening ignores the new variable, exchange permutes the tuple, and contraction uses one variable for both occurrences of the contracted formula. In each case the required implication follows from the induction hypothesis by the corresponding intuitionistic propositional derivation in $\mathrm{HA}^{\omega}_{\mathrm{int}}$. [/step]

[step:Interpret the propositional rules using product, sum, and function terms]For conjunction introduction, use $(R_A,R_B):|A|\times |B|$. The conjunction clause says that this term realizes $A\land B$ exactly when $R_A\Vdash_{\mathrm{mr}}A$ and $R_B\Vdash_{\mathrm{mr}}B$. For conjunction elimination, use the projections $\pi_1$ and $\pi_2$. For implication introduction, suppose the derivation of $B$ has an additional discharged assumption $A$. Let $y:|A|$ be the corresponding realizer variable. The induction hypothesis gives a term $S(X,y):|B|$ and proves \begin{align*} \mathrm{HA}^{\omega}_{\mathrm{int}}\vdash (X\Vdash_{\mathrm{mr}}\Gamma)\to (y\Vdash_{\mathrm{mr}}A)\to S(X,y)\Vdash_{\mathrm{mr}}B. \end{align*} Define $R_{A\to B}:=\lambda y.S(X,y):|A|\to |B|$. By the implication clause, $R_{A\to B}\Vdash_{\mathrm{mr}}A\to B$ is precisely the statement that every realizer of $A$ is sent to a realizer of $B$. For implication elimination, use application: if $F:|A|\to |B|$ realizes $A\to B$ and $R_A:|A|$ realizes $A$, then $F(R_A):|B|$ realizes $B$. For disjunction introduction, use $\operatorname{inl}(R_A):|A|+|B|$ or $\operatorname{inr}(R_B):|A|+|B|$. For [disjunction elimination](/theorems/4625), let $D:|A|+|B|$ realize $A\lor B$, let $S_A(X,a):|C|$ realize $C$ from $a:|A|$ realizing $A$, and let $S_B(X,b):|C|$ realize $C$ from $b:|B|$ realizing $B$. Define \begin{align*} R_C:=\operatorname{case}(D,\lambda a.S_A(X,a),\lambda b.S_B(X,b)). \end{align*} The sum-elimination clause for modified realizability proves $R_C\Vdash_{\mathrm{mr}}C$ in the left and right cases. For falsity elimination, first define by structural recursion a closed default realizer $e_A:|A|$ for every formula $A$. For atomic formulas and $\bot$, take the unit term. For conjunctions take pairs, for disjunctions take the left injection, for implications and universal formulas take constant functions, and for existential formulas take $(d_\sigma,e_{A(d_\sigma)})$, using the stipulated closed default term $d_\sigma:\sigma$. If the induction hypothesis gives a realizer of $\bot$, then the formula realized is $\bot$ itself, so intuitionistic ex falso proves $e_A\Vdash_{\mathrm{mr}}A$.[/step]

[guided]The propositional clauses work because the theorem statement has made the realizer type constructors part of the object term calculus. A conjunction realizer is an actual pair, so from realizers $R_A:|A|$ and $R_B:|B|$ we form $(R_A,R_B):|A|\times |B|$, and the definition of modified realizability for $A\land B$ expands to the two formulas $R_A\Vdash_{\mathrm{mr}}A$ and $R_B\Vdash_{\mathrm{mr}}B$. Conversely, the eliminations are the product projections, and their correctness is exactly the product clause. For implication, the introduction rule has one extra assumption $A$. We represent that extra assumption by a fresh variable $y:|A|$. The induction hypothesis gives a term $S(X,y):|B|$ and proves that, if the variables $X$ realize the old assumptions and $y$ realizes $A$, then $S(X,y)$ realizes $B$. Therefore the abstraction $\lambda y.S(X,y):|A|\to |B|$ maps each realizer of $A$ to a realizer of $B$, which is the modified-realizability definition of $A\to B$. The elimination rule is ordinary application: applying a realizing function $F:|A|\to |B|$ to a realizing input $R_A:|A|$ gives $F(R_A):|B|$, and the implication clause proves that this output realizes $B$. The delicate point is falsity elimination. To derive an arbitrary realized conclusion from $\bot$, we must already have a term of the required realizer type. This is why the theorem statement explicitly assumes a closed default element $d_\sigma:\sigma$ for every finite type and includes unit, product, sum, and function types in the term calculus. These data give a closed default realizer $e_A:|A|$ by recursion on $A$: unit for atomic formulas and $\bot$, pairs for conjunctions, left injections for disjunctions, constant functions for implications and universals, and $(d_\sigma,e_{A(d_\sigma)})$ for existentials. Once $e_A$ is available, the induction hypothesis for a proof of $\bot$ gives $u\Vdash_{\mathrm{mr}}\bot$, which is definitionally $\bot$; intuitionistic ex falso then proves $e_A\Vdash_{\mathrm{mr}}A$.[/guided]

[step:Interpret quantifier rules over arbitrary finite types] For universal introduction, suppose $\forall z^\sigma A(z)$ is inferred from $A(z)$ and $z$ is not free in the undischarged assumptions. The induction hypothesis gives $S(X,z):|A(z)|$ realizing $A(z)$ under $X\Vdash_{\mathrm{mr}}\Gamma$. Define $R:=\lambda z.S(X,z):\sigma\to |A(z)|$. The eigenvariable condition ensures that the assumption-realizability formulas do not depend on $z$, so the universal clause proves $R\Vdash_{\mathrm{mr}}\forall z^\sigma A(z)$. For universal elimination, if $F:\sigma\to |A(z)|$ realizes $\forall z^\sigma A(z)$ and $t:\sigma$ is a term, define $R:=F(t):|A(t)|$. The universal clause gives $F(t)\Vdash_{\mathrm{mr}}A(t)$. For existential introduction, if $t:\sigma$ and $R:|A(t)|$ realizes $A(t)$, define $(t,R):\sigma\times |A(t)|$. The existential clause proves that this pair realizes $\exists z^\sigma A(z)$. For existential elimination, let $D:\sigma\times |A(z)|$ realize $\exists z^\sigma A(z)$, and let the second premise derive $C$ from $\Gamma,A(z)$ with $z$ not free in $C$ or in $\Gamma$. Define $z_D:=\pi_1(D):\sigma$ and $a_D:=\pi_2(D):|A(z_D)|$. If $S(X,z,a):|C|$ is the term supplied by the induction hypothesis for the second premise, set $R_C:=S(X,z_D,a_D)$. The existential clause gives $a_D\Vdash_{\mathrm{mr}}A(z_D)$, and the induction hypothesis gives $R_C\Vdash_{\mathrm{mr}}C$. [/step]

[step:Realize intensional equality, defining equations, and substitution] Every primitive-recursive defining equation, every basic arithmetic axiom, and every reflexivity or congruence axiom for intensional equality is atomic. Since atomic formulas have unit realizer type and $u\Vdash_{\mathrm{mr}}P$ is definitionally $P$, the unit term realizes each such axiom exactly because the axiom is provable in $\mathrm{HA}^{\omega}_{\mathrm{int}}$. For equality substitution, suppose a derivation step replaces a term $s:\sigma$ by a term $t:\sigma$ using a proof of $s=t$. The induction hypothesis gives the realizability formula before substitution. The formula $R\Vdash_{\mathrm{mr}}A$ is an ordinary formula of $\mathrm{HA}^{\omega}_{\mathrm{int}}$, because it is obtained by structural recursion from atomic formulas using only the allowed logical connectives, equality predicates, term constructors, and finite-type quantifiers. Therefore the equality-substitution rule of $\mathrm{HA}^{\omega}_{\mathrm{int}}$ transports the realizability formula along $s=t$. No functional extensionality case is required, because functional extensionality is not an axiom of the stated theory. [/step]

[step:Realize natural-number induction by primitive recursion at the realizer type] Let the last rule be induction for a formula $B(n)$ with $n:\mathbb{N}$. Put $\rho:=|B(n)|$. The type $\rho$ is independent of the value of $n$, since replacing an object variable by a term changes parameters inside formulas but not the structural realizer type. The induction hypotheses provide a base realizer $b_0:\rho$ for $B(0)$ and a step realizer $g:\mathbb{N}\to\rho\to\rho$ such that $g(n)(q)$ realizes $B(Sn)$ whenever $q$ realizes $B(n)$. By primitive recursion at type $\rho$, define $h:\mathbb{N}\to\rho$ by the equations $h(0)=b_0$ and $h(Sn)=g(n)(h(n))$. The formula $h(n)\Vdash_{\mathrm{mr}}B(n)$ is an admissible formula of $\mathrm{HA}^{\omega}_{\mathrm{int}}$ by the structural definition of modified realizability. Hence the internal induction scheme applies to it. The base case follows from $h(0)=b_0$ and the base realizing hypothesis. For the successor step, assume $h(n)\Vdash_{\mathrm{mr}}B(n)$. The step realizing hypothesis gives $g(n)(h(n))\Vdash_{\mathrm{mr}}B(Sn)$, and the recursion equation $h(Sn)=g(n)(h(n))$ converts this into $h(Sn)\Vdash_{\mathrm{mr}}B(Sn)$. Internal induction proves \begin{align*} \forall n:\mathbb{N}\, h(n)\Vdash_{\mathrm{mr}}B(n). \end{align*} By the universal clause, $h$ realizes $\forall n:\mathbb{N}\,B(n)$. [/step]

[step:Specialize the open-context theorem to closed derivations] The preceding cases cover assumptions, structural rules, all rules for $\land$, $\lor$, $\to$, $\bot$, quantifiers over finite types, intensional equality and substitution, primitive-recursive defining equations, arithmetic axioms, and natural-number induction. Therefore the derivation induction proves the open-context soundness claim. Now assume $A$ is closed and $\mathrm{HA}^{\omega}_{\mathrm{int}}\vdash A$. Apply the open-context result with $\Gamma$ empty. The constructed term has no free assumption-realizer variables; since the derivation is closed, it has no free object variables either. Thus the resulting term $r:|A|$ is closed, and the open-context conclusion becomes \begin{align*} \mathrm{HA}^{\omega}_{\mathrm{int}}\vdash r\Vdash_{\mathrm{mr}}A. \end{align*} This is exactly the claimed modified-realizability soundness theorem. [/step]