A conservative extension of Peano Arithmetic

Question

Ulrich Kohlenbach makes the following intriguing comment here:

"In the 70s S. Feferman introduced a mathematically strong system S=restricted(PA^omega)+QF-AC+mu for classical mathematics (and in particular analysis) and showed that S is conservative over Peano arithmetic PA."

I spent some time looking for a source for this at MathSciNet in the work of Feferman, Kohlenbach, and Sanders, but was unable to find precisely what Kohlenbach seems to be referring to.

What is the history of conservative extensions of Peano Arithmetic that incorporate the existence of an infinite integer, and what are the most relevant papers?

Some results in this direction can be found in Palmgren:

Palmgren, Erik. An effective conservation result for nonstandard arithmetic. MLQ Math. Log. Q. 46 (2000), no. 1, 17–23.

Here Proposition 2.1 on page 18 asserts that "*PA is a conservative extension of PA." The theory *PA, as might be expected, incorporates the standardness predicate as well as other axioms elaborated there.

Answer 1

In the classical setting, the result of the type that is asked in the question was established by Harvey Friedman, answering a question of Abraham Robinson; Friedman's results is reported in the following paper of Kreisel:

Axiomatizations of nonstandard analysis that are conservative extensions of formal systems for classical standard analysis, by G. Kreisel, in Applications of Model theory to Algebra, Analysis, and Probability (W. A. J. Luxemburg, editor), Holt, Rinehart and Winston, New York, 1969, pp. 93-106.

Friedman's result says that a particular theory $^*\mathsf{PA}$ of nonstandard numbers, together with the so-called $^*\Pi_{\infty}\mathsf{-Induction}$ is conservative over $\mathsf{PA}$. $^*\mathsf{PA}$ is formulated in an extension of $\mathsf{PA}$ with a new unary predicate $N(x)$, its axioms asserts the existence of an element outside of $N(x)$ [i.e., an "infinite" element], the transfer principle [that asserts through infinitely many axioms that the submodel determined by $N(x)$ is an elementary submodel of the whole model], and an axioms that says that the model determined by $N(x)$ is an initial segment of the whole model.

Models of $^*\mathsf{PA}$ are of the form $(M,+,*,N)$, where $(M,+,*,<)\models \mathsf{PA}$, $N$ is a proper initial segment of $M$ that is closed under $+$ and $*$, and $(N,+,*,<)$ is an elementary submodel of $(M,+,*,<)$. In this context, $(M,+,*,N)$ satisfies $^{*}\Pi_{\infty}\mathsf{-Induction}$, if for every parametrically definable subset $D$ of $(M,+,*,N)$, $(N,+,*,<,D\cap M)$ satisfies $\mathsf{PA}$ in the extended language that includes an extra predicate interpreted by $D\cap M$.

Friedman gave a direct proof of his conservatity result, but his proof can be made shorter by using Phillips' refinement of the MacDowell-Specker Theorem; the refinement states that every model of $\mathcal{M}$ of $\mathsf{PA}$ has a conservative elementary end extension $\mathcal{N}$ [i.e., $\mathcal{N}$ is an elementary end extension of $\mathcal{M}$ with the property that if $D$ is a parametrically definable subset of the universe of $\mathcal{N}$, then the intersection of $D$ with the universe of $\mathcal{M}$ is parametrically definable in $\mathcal{M}$].

Friedman's result is stated as a starting point of the process of gauging the strength of saturation principles in nonstandard theories of arithmetic in the following paper (see Proposition 2.3 for the statement of Friedman's result).

The strength of nonstandard methods in arithmetic, by C.W. Henson, M. Kaufmann, and H.J. Keisler, Journal of Symbolic Logic, Dec. 1984.

A more recent result that generalizes Friedman's theorem pertains to a nonstandard variant of $\mathsf{ACA_0}$, here $\mathsf{ACA_0}$ is a well-known subsystem of the first order formulation of second order number theory that is conservative over $\mathsf{PA}$. This result is reported as Theorem 7.10 of the following paper (and is an immediate corollary of a result of mine, as mentioned by Keisler).

Nonstandard Arithmetic and reverse mathematics, by H.J. Keisler, The Bulletin of Symbolic Logic, March 2006.

Answer 2

I was referring to the 2nd Theorem in section 8.7 in Feferman's 1977 article "Theories of finite type related to mathematical practice" in:
J. Barwise (ed.), Handbook of Mathematical Logic, North Holland 1977.

Answer 3

I believe Feferman's theory S (under a different name) is used here by Feferman to formalise mathematics in a predicative setting.

Erik Palmgren used to have a list on his webpage with papers on (constructive-ish) NSA. However, this is now gone and the wayback machine also does not have it.

The most relevant systems (classical and constructive) are due to van den Berg et al:

B. van den Berg, E. Briseid, and P. Safarik, A functional interpretation for nonstandard arithmetic, Annals of pure and applied logic 163 (2012), no. 12, 1962–1994.

Their interpretation was implemented in Agda by Chuangjie Xu.

A slightly different approach is here:

Benno van den Berg, Sam Sanders: Reverse Mathematics and parameter-free Transfer. Ann. Pure Appl. Log. 170(3): 273-296 (2019)

No extraction algorithm is available (by design), but one does get the transfer principle for sentences.

The history of these things is not written down anywhere in detail and there is a lot of folklore in general.

I hope that helps.

Answer 4

The following is an addendum to Sam Sanders’ answer, too long for a comment: It’s a short bibliography of constructive NSA and related theories of nonstandardness, taken from Erik Palmgren’s now-defunct webpage at Uppsala University (https://www2.math.uu.se/∼palmgren/biblio/nonstd.html), last modified Dec 2010 according to the file timestamp. Erik’s later webpage at Stockholm University remains extant here.

---

Constructive nonstandard mathematics

Chuaqui, R., Suppes, P.: Free-variable axiomatic foundations of infinitesimal analysis: A fragment with finitary consistency proof. J. Symbolic Logic 60(1995), 122 - 159.

Chwistek, L.: The Limits of Science, Kegan Paul, London 1948.

Dragalin, A.G.: An explicit boolean-valued model for the non-standard arithmetic, Publ. Math. Debrecen 42(1993), 369 - 389.

Laugwitz, D. : Omega-calculus as a generalisation of field extension - an alternative approach to nonstandard analysis, in: A.E. Hurd (ed.) Non-standard Analysis - Recent Developments, Lecture Notes in Mathematics, Vol. 983, Springer, Berlin 1983.

Liu, S.-C.: A proof-theoretic approach to nonstandard analysis with emphasis on distinguishing between constructive and non-constructive results, in: H.J. Keisler and K. Kunen (eds.), The Kleene Symposium, North-Holland, Amsterdam 1980, 391 - 414.

Martin-Löf, P.: Mathematics of Infinity, in: P. Martin-Löf and G.E. Mints (eds.) COLOG-88 Computer Logic, Lecture Notes in Computer Science, vol. 417, Springer, Berlin 1989.

Moerdijk, I.: A model for intuitionistic non-standard arithmetic, Ann. Pure Appl. Logic 73(1995), 37 --51.

Moerdijk, I., Palmgren, E.: Minimal models of Heyting arithmetic, Uppsala University, Department of Mathematics Report 1995:25 (accepted for publication in J. Symbolic Logic).

Mycielski, J.: Analysis without actual infinity, Journal of Symbolic Logic 46(1981), 625-633.

Palmgren, E.: A note on 'Mathematics of Infinity', Journal of Symbolic Logic 58(1993), 1195 -- 1200.

Palmgren, E.: A constructive approach to nonstandard analysis, Ann. Pure Appl. Logic 73(1995), 297 -- 325.

Palmgren, E.: Constructive nonstandard analysis, Cahiers du Centre de Logique, vol. 9, Academia, Louvain, 1996.

Palmgren, E.: A sheaf-theoretic foundation for nonstandard analysis, Uppsala University, Department of Mathematics Report 1995:43 (to appear in Ann. Pure Appl. Logic).

Palmgren, E.: Sheaf-theoretic nonstandard analysis: constructive aspects. Uppsala University, Department of Mathematics Report 1996:28.

Schmieden, C., Laugwitz, D.: Eine Erweiterung der Infinitesimalrechnung, Math. Zeitschrift 69(1958), 1-39.

Vesley, R.: An intuitionistic infinitesimal calculus, in: F. Richman (ed.) Constructive Mathematics, Lecture Notes in Mathematics, Vol. 873, Springer, 1983.

Wattenberg, F.: Nonstandard analysis and constructivism? Studia Logica 47(1988), 303 -- 309.