About Goodman's theorem (Q1942040)

In 1978, Nicholas Goodman published a proof of the statement that \(\mathrm{HA}^{\omega}+\mathrm{ AC}\) is conservative over \(\mathrm{HA}\). Here \(\mathrm{ HA}^{\omega}\) is ``intuitionistic arithmetic in all finite types'', and AC is the ``Axiom of Choice'': \[ \forall x^{\sigma}\exists y^{\tau}\phi (x,y)\;\to\;\exists z^{\sigma\to\tau}\forall x^{\sigma}\phi (x,zx). \] Goodman's proof was an intricate mixture of a kind of forcing and realizability. The metamathematics is non-constructive. The present paper is concerned with a \textit{constructive} version of this proof. The technique of proof consists in separating the realizability part from the forcing part, and define forcing \textit{locally}, that is: for a given formula \(\psi\) such that \({\mathrm{ HA}}^{\omega}+{\mathrm{ AC}}\vdash\psi\), a notion of forcing is defined with nice properties. First, following Renardel de Lavalette, a system \(\mathrm{TAPP}\) is defined (basically, axioms for ``arithmetic plus a combinatory algebra structure'') which can easily be seen to be a conservative extension of \(\mathrm{ HA}^{\omega}\), hence also of \(\mathrm{HA}\). The theory \(\mathrm{TAPP}\) has a built-in realizability, and \(\mathrm{AC}\) is provably realized in it. As a consequence, whenever \(\mathrm{ HA}^{\omega}+\mathrm{ AC}\) proves a formula \(\phi\), \(\mathrm{TAPP}\) proves that \(\phi\) is realizable. Then, relative to a proof of a formula \(\psi\) in \(\mathrm{ HA}^{\omega}+\mathrm{ AC}\), the author defines a definitional extension of \(\mathrm{TAPP}\) with an extra sort of ``forcing conditions'' and some special constants \(c\). The constants \(c\) are meant to encode explicit choices for existential formulas occurring in the hypothetical proof, so for such a formula \(\exists nB(m,n)\) we have an axiom \[ (\exists nB(m,n))\to N(cm)\wedge B(m,cm), \] where \(cm\) is the action of \(c\) on the natural number \(m\), and \(N(cm)\) is the statement that \(cm\) is a natural number. The idea is now that the sentence ``\((\psi \text{ has a realizer})\to\psi\)'' will be forced, provably in this conservative extension. This holds since \(\psi \) is a formula in the language of \(\mathrm{HA}\). Since the sentence \((\psi \text{ has a realizer})\) is provable (by soundness of the realizability notion), and therefore forced, we get that \(\psi\) is forced. But \(\psi\) is arithmetical, so its being forced is equivalent to \(\psi\) itself, and we are done. A very neat, compact paper with a nice result.