Let $\mathrm{HA}^{\omega}_{\mathrm{int}}$ be many-sorted intuitionistic arithmetic over the finite types generated from $\mathbb{N}$ by the type formers $1$, $\times$, $+$, and $\to$. Assume its term calculus contains the corresponding unit, product, sum, and function constructors and eliminators, a closed default element $d_\sigma:\sigma$ for every finite type $\sigma$, and primitive recursion on $\mathbb{N}$ at every finite type. Equality is the intensional equality predicate at each finite type, with reflexivity, congruence, substitution, and the defining equations for the term formers and primitive recursion; no functional extensionality axiom is included. Formulas are built from atomic equalities and arithmetic predicates by $\land$, $\lor$, $\to$, $\bot$, and quantifiers over arbitrary finite types. Define the modified-realizability type $|A|$ and formula $r\Vdash_{\mathrm{mr}}A$ by structural recursion: atomic formulas and $\bot$ have realizer type $1$, with $u\Vdash_{\mathrm{mr}}P$ equal to $P$ for atomic $P$ and $u\Vdash_{\mathrm{mr}}\bot$ equal to $\bot$; $|A\land B|:=|A|\times |B|$, $|A\lor B|:=|A|+|B|$, $|A\to B|:=|A|\to |B|$, $|\forall x^\sigma A(x)|:=\sigma\to |A(x)|$, and $|\exists x^\sigma A(x)|:=\sigma\times |A(x)|$, with the standard product, sum, function, universal, and existential clauses. If $A$ is closed and $\mathrm{HA}^{\omega}_{\mathrm{int}}\vdash A$, then there is a closed finite-type term $r:|A|$ such that $\mathrm{HA}^{\omega}_{\mathrm{int}}\vdash r\Vdash_{\mathrm{mr}}A$.