### Introduction

For reasons best left to psychologists and historians, a number of big names in mathematics have claimed that Nonstandard Analysis (NSA) is fundamentally non-constructive. In this post, I sketch how NSA has lots of computational content based on [Sa18, Sa20] .

Here, NSA refers to any approach to mathematics in which *infinitesimals* (aka infinitely small quantities) are used explicitly. The approach should be rigorous and (in principle) based on some formal system, like e.g. an extension of ZFC or Peano arithmetic. It is a matter of the historical record that most of physics is still done via an *informal* infinitesimal calculus, while the same was true for mathematics until the (slow) adoption of Weierstrass ‘epsilon-delta’ framework.

Abraham Robinson‘s *model-theoretic* framework [Ro66] was the first milestone in NSA. The best-known *syntactic* approach to NSA is Ed Nelson‘s *internal set theory* ([Ne77]; IST for short), an extension of ZFC with a new predicate ‘ is standard’. The system IST is the focus of this post.

### Nelson’s internal set theory, and fragments

The usual foundation of mathematics, ZFC set theory, involves a primitive symbol , which we all agree to read as ‘is an element of’. The properties of are governed by the ZFC axioms. Nelson’s IST adds an extra primitive symbol ‘st’, which we agree to read as ‘is standard’. On top of ZFC, the axioms I*dealisation*, S*tandardisation*, and T*ransfer*, govern the properties of ‘st’. One can show that ZFC and IST prove the same *internal* theorems, i.e. not involving the new predicate ‘st’.

The main conceptual point is that we are free to interpret ‘st’ in IST in whichever way we please, as long as it accords with (some of) the external (=non-internal) axioms of IST. Intuitively speaking, the approach taken in [VBS12] is to interpret ‘st‘ as ‘ can be computed’. Instead of full ZFC, the nonstandard system, called , is based on the finite type extension of Peano Arithmetic .

Due to the extension of the language with ‘st’, the system has two extra quantifiers as follows: define as and as . Intuitively speaking, the quantifier means that ‘an object can be computed’, while means ‘for all computable objects ‘.

The above view is motivated by the main ‘term extraction’ theorem of [VBS12] as follows.

From a proof in of a sentence

, (*)

for internal , a

primitive recursiveterm can be extracted such that proves, (**)

where is a finite sequence of objects.

In a nutshell, an NSA-proof in of (*) gives rise to an algorithm as in (**), provided by a primitive recursive term . The input variables of are determined by the standard variables in (*), while the output variables are determined by the standard variables in (**).

### The scope of the term extraction theorem

An obvious question is now: how general is the class of formulas of the form (*) ? As it happens, this class is quite large and includes many of the ‘nonstandard’ definitions of fundamental mathematical concepts, like continuity and compactness, as can be gleaned from the below table. I will discuss a couple of nonstandard definitions for completeness. The following is the **nonstandard** definition of (pointwise) continuity:

(%)

where means that for any standard , i.e. is an infinitesimal.

The following sentence expresses the **nonstandard** compactness of the unit interval:

(%%)

The following is the **nonstandard** definition of uniform continuity:

which also follows by combining the two above formulas (%) and (%%).

The following is the **nonstandard** definition of convergence of a sequence to a finite limit :

(&)

Note that nonstandard are also called ‘infinite’, which gives ‘true’ meaning to ‘the limit as tends towards infinity’.

To be absolutely clear, the above four formulas can be brought into the form (*) from the term extraction theorem, working inside . Moreover, an implication between two formulas of the form (*), can be brought into the form (*), again working in .

Finally, the following table provides an overview of some nonstandard concepts that can be brought into the form (*) above, and therefore have computational content. The second column describes what (usual) concepts the first column are translated to by the above term extraction theorem from [VBS12]. The concepts in the same row are also equivalent over the right base theory, as explored in [VS19, Sa18b].

As an example, if proves (%) above for some given by a term in , we can bring (%) into the form (*), and the term extraction theorem provides a modulus of continuity.

In a follow-up post, I will discuss some more examples, including results from *Reverse Mathematics*.

### References

[VBS12] Benno van den Berg, Eyvind Briseid, and Pavol Safarik, A functional interpretation for nonstandard arithmetic, Ann. Pure Appl. Logic 163 (2012), no. 12, 1962–1994. [VS19] Benno van den Berg and Sam Sanders, Reverse mathematics and parameter-free transfer, Ann. Pure Appl. Logic 170 (2019), no. 3, 273–296. [Ne77] Edward Nelson, Internal set theory: a new approach to nonstandard analysis, Bull. Amer. Math. Soc. 83 (1977), no. 6, 1165–1198. [Ro66] Abraham Robinson, Non-standard analysis, North-Holland, Amsterdam, 1966. [Sa18] Sanders, Sam To be or not to be constructive, that is not the question.*Indag. Math. (N.S.)*29 (2018), no. 1, 313–381. [Sa18b] Sanders, Sam Some nonstandard equivalences in reverse mathematics, Sailing routes in the world of computation, Lecture Notes in Comput. Sci., vol. 10936, Springer, Cham, 2018, pp. 365–375. [Sa20] Sanders, Sam The unreasonable effectiveness of Nonstandard Analysis.

*J. Logic Comput.*30 (2020), no. 1, 459–524

I think the reason for which non-standard analysis is regarded to be non-constructive is nothing more than the fact that in order to construct the usual models of non-standard reals in ZF (e.g. non-trivial ultrapowers of R), one requires weak forms of the axiom of choice.

Sure, but there are plenty of statements, like the countable additivity of the Lebesgue measure, that similarly require some fragment of AC but are not the subject of an all-out academic flamewar.

Hi Sam, thanks for the interesting post. I never looked at non-standard analysis, so it’s nice to see it from the point of view of proof mining… Some questions:

1. Does the ackronym IST simultaneously abbreviate ‘Internal Set Theory’ and ‘Idealisation, Standardisation, Transfer’?

2. How does one prove that IST is conservative over ZFC? Can it be done by cut-elimination?

I am still trying to wrap my head around the ‘scope of the term extraction theorem’….

Hi Anupam,

Welcome to the NSA club ^_^. Tom Powell has a good (and detailed) description of the sketch I gave. As to your questions:

1) I think Nelson indeed intended for that ‘simultaneous’ meaning of IST.

2) For conservation of IST over ZFC, there are model-theoretic proofs (Nelson’s original ’77 paper) and proof-theoretic results. The latter actually provides an algorithm of the following kind:

Let A be a sentence in the language of ZFC. There is an algorithm that takes as input “a proof in IST of A” and produces as output “a proof in ZFC of A”.

This can be found in follow-up papers, and on Nelson’s website.

Re (2), the model-theoretic proof must also give such an algorithm, since the statement itelf is ! (Can we call this meta-proof-mining? 😉 )

But I suppose the complexity might be different: extracting such an algorithm for the model theoretic proof, a priori, relies on the Completeness theorem, so apparently requires , and so the immediate obvious bound is only primitive recursive. Using cut-elimination requires only the superexponential/tetration function. So there is a meta-question: are the two proofs *measurably* different, e.g. in terms of complexity of the induced algorithm? It’s only a curiosity, but one that would satisfy the structural proof theorist in me.

I have no idea about the different complexities. There are a number of theorems about the “speed-up” provided by an NSA-proof. If I recall correctly, the NSA formalism does not provide much of a speed-up in the general case. Individual proofs are of course a different matter (as shown by proof mining). I tend towards the following position:

1) Speed-up theorems are interesting metamathematical results that in general however have little impact on actual mathematics (like Goedel’s incompleteness theorems).

2) The study of particular proofs (and non-formal classes thereof) shall yield a picture closer to actual mathematics.