An Effective Conservation Result for Nonstandard Arithmetic (Q4939397)

The theory *PA introduced by \textit{C. W. Henson, M. Kaufmann} and \textit{H. J. Keisler} [J. Symb. Log. 49, 1039-1058 (1984; Zbl 0587.03048)] is Peano arithmetic formulated in the language of arithmetic augmented with function symbols for all primitive recursive functions and the standardness predicate. The axioms express: that the standard part is a model of PA; a transfer principle saying that the nonstandard part is an elementary extension the standard part (in the language of PA); the existence of nonstandard elements; and the axiom stating that the nonstandard part is an end extension of the standard one. An easy model-theoretic argument shows that \(^*\text{PA}\) is a conservative extension of PA. The paper is devoted to the proof that \(^*\text{PA}\) + \(^*\Pi_\infty\) is also conservative over PA, where \(^*\Pi_\infty\) is the axiom scheme \[ (\forall \bar x)(\varphi (\bar x, 0)\land (\forall^{\text{st}}y) (\varphi(\bar x,y)\rightarrow \varphi(\bar x,y+1))\rightarrow (\forall^{ \text{st}}y) \varphi(\bar x,y)), \] where \(\varphi\) is a formula of the language of \(^*\text{PA}\). The proof uses an internal definable ultrapower construction to build an extension of a given model of PA with the desired properties. Interpretability results for the second-order variants of the considered theories are also given.