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 Idealisation, Standardisation, and Transfer, 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 recursive term 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.