The computational content of Nonstandard Analysis

Posted on by Sam Sanders

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 ‘x 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 \in, which we all agree to read as ‘is an element of’. The properties of \in 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(x)‘ as ‘x can be computed’. Instead of full ZFC, the nonstandard system, called P, is based on the finite type extension of Peano Arithmetic \textsf{E-PA}^\omega.

Due to the extension of the language with ‘st’, the system P has two extra quantifiers as follows: define (\exists^{st} x)(\dots) as (\exists x)(st(x) \wedge \dots) and (\forall^{st} y)(\dots) as (\forall y)(st(y) \rightarrow \dots). Intuitively speaking, the quantifier (\exists^{st}x) means that ‘an object x can be computed’, while (\forall^{st} y) means ‘for all computable objects y‘.

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

From a proof in P of a sentence

(\forall^{st} x)(\exists^{st}y)A(x,y), (*)

for internal A(x,y), a primitive recursive term t can be extracted such that \textsf{E-PA}^\omega proves

(\forall x)(\exists y \in t(x))A(x,y), (**)

where t(x) is a finite sequence of objects.

In a nutshell, an NSA-proof in P of (*) gives rise to an algorithm as in (**), provided by a primitive recursive term t. The input variables of t are determined by the standard variables x in (*), while the output variables are determined by the standard variables y 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:

(\forall^{st} x\in [0,1])(\forall y\in [0,1])(x\approx y \rightarrow f(x)\approx f(y)), (%)

where x\approx y means that |x-y|<\epsilon for any standard \epsilon>0, i.e. x-y is an infinitesimal.

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

(\forall x\in [0,1])(\exists^{st} y)(x\approx y) (%%)

The following is the nonstandard definition of uniform continuity:

(\forall x, y\in [0,1])(x\approx y \rightarrow f(x)\approx f(y)),

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

The following is the nonstandard definition of convergence of a sequence (x_n)_{n\in \mathbb{N}} to a finite limit x\in \mathbb{R}:

(\forall N\in \mathbb{N})( \neg st(N) \rightarrow x\approx x_N). (&)

Note that nonstandard N\in \mathbb{N} are also called ‘infinite’, which gives ‘true’ meaning to ‘the limit as n tends towards infinity’.

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

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].

Rendered by QuickLaTeX.com

As an example, if P proves (%) above for some f:[0,1]\rightarrow \mathbb{R} given by a term in P, 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

7 thoughts on “The computational content of Nonstandard Analysis”

  1. 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.

  3. 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’….

  4. 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.

    1. Re (2), the model-theoretic proof must also give such an algorithm, since the statement itelf is \Pi^0_2 ! (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 \mathsf{WKL}_0, 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.

      1. 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.

  5. There is another reason why analysis with infinitesimals a la Robinson is in fact effective (in the sense of staying within the bounds of ZF): Karel Hrbacek and I developed an axiomatic theory SPOT in the st-\in-language, which is a conservative extention of ZF (without choice). The theory is sufficient to do infinitesimal analysis. See https://u.math.biu.ac.il/~katzmik/spot.html

Leave a Reply