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.

  • 2
    $\begingroup$ There appears to be two separate bodies of work relating to conservativity results concerning the metamathematics of nonstandard arithmetic, namely the classical tradition (specified in my answer below), and the constructive/intuitionistic tradition. Each tradition has its own nomenclature and methodology, and each seems to "blissfully" ignore the other one due to the minimal overlap between their methods and goals. $\endgroup$
    – Ali Enayat
    Commented Mar 7 at 16:27

4 Answers 4


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.


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.

  • 2
    $\begingroup$ Ulrich, Welcome to MO! Honored to see you here. This result is on page 967 in that volume. I would appreciate additional details if possible because the notation is not easy to decipher. $\endgroup$ Commented Mar 5 at 15:57

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.

  • 1
    $\begingroup$ I should probably be able to dig up that old page from Erik Palmgren’s website — I have an archive of most of his work files. I may not get around to it today as I’m a bit busy, but if I haven’t dug it up within 48hours, please ping me to remind! $\endgroup$ Commented Mar 4 at 8:42
  • 1
    $\begingroup$ Thanks, that's helpful. I lot of these papers are written in a fairly technical way. For example, the issue of conservativity seems to be rarely discussed explicitly, as the papers are addressed to experts to whom this is "obvious". It would be nice to have a more accessible survey aimed at a general interested mathematical reader rather than aimed to impress the specialists in the field. $\endgroup$ Commented Mar 4 at 11:37
  • $\begingroup$ @PeterLeFanuLumsdaine "ping" $\endgroup$ Commented Mar 6 at 13:12
  • $\begingroup$ @MikhailKatz: Thanks for the ping! I’ve added Erik’s list in a separate answer since it was too long for a comment. $\endgroup$ Commented Mar 6 at 14:45

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.

  • $\begingroup$ This focuses mostly on constructivism and intuitionistic logic. I was hoping at some point to get a summary in the simpler context of classical logic, focusing on conservativity results. I believe Feferman's 1977 result was of this t ype. $\endgroup$ Commented Mar 6 at 15:08

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.