[FOM] The computational content of Nonstandard Analysis

[Sam Sanders]

Dear Harvey, dear FOM,

Here is a new attempt at explaining the computational content of Nonstandard Analysis (NSA) in approximately five steps:


0) I take it everyone has (vaguely) heard of constructive math and the underlying so-called intuitionistic logic.  I also assume that 
everyone has heard of “Nonstandard Analysis”, where (somehow) a distinction between standard and nonstandard objects is made.  
   
1) First of all, constructive approaches to math and logic are different from the mainstream (or ‘classical’) approach in the following way (among other ways):

From a proof of “there exists x such that A(x)”, one can extract some term t such that A(t).  By contrast, classical logic and classical mathematics do not have this “existence property”.  

This existence property is often touted as an advantage of constructive math, as one can in principle implement the latter's results in a suitable programming language (like Agda)
and extract the computational information carried by the existential quantifiers.  

2) Secondly, one *can* of course translate theorems proved using classical logic into (modified) theorems with constructive proofs (See Goedel-Gentzen and H. Friedman’s work).
However, the resulting (modified) theorems are generally quite different from and more complicated than the original theorems, with the exception of classes of 
’simple' formulas, like 

“For all natural numbers x, there is a natural number y such that A(x,y)”,  (*)

where A is decidable.  As a result of the aforementioned proof translations, (*) does have the “existence property”, i.e. there is a computable function f such that A(x,f(x)) from a given x, and
this f can be extracted (after translation) from a classical proof of (*).  

3) Thirdly, as it turns out, proofs of theorems in fragments of Nonstandard Analysis (in Nelson’s internal set theory) can *also* be translated into (modified) theorems in “standard” mathematics (not involving NSA).  Again, the resulting (modified) theorems are generally much more complicated and different from the original ones, except for a specific formula class which also turns out to have a kind of existence property.  This special formula class is as follows:    

“For all standard x, there is a standard y such that A(x,y)”, where A does not involve the notion “standard”.  (**)

These results may be found in van den Berg et al (APAL, 2012).  


4) And now comes the crux:  The formula class given by (*) from 2) is “relatively small”, while the formula class given by (**) from 3) encompasses all theorems of “pure” Nonstandard Analysis (and much more).  A theorem is part of “pure NSA” if it is formulated solely with the nonstandard definitions (of continuity, open set, compactness, differentiability, Riemann integration, etc). 

In particular, any theorem of pure NSA can be brought into the form (**), and applying the existence 
property to the latter provides a term t such that the associated "standard" system (not involving NSA) proves 

“For all x, we have A(x,t(x))” 

(with slight simplification regarding the witnesses t(x) to increase readability).

5) In conclusion, similar to the proof translations from classical to intuitionistic logic, there are proof translations from fragments of NSA to “standard mathematics” (not involving NSA).
In particular, the former translations bestow the existence property onto certain classically proved formulas (so-called Pi_2^0-formulas like (*)), while the latter translations do the same 
for a certain class of nonstandard formulas (like (**)).  However, the latter class encompasses all of “pure” NSA, i.e. nonstandard theorems formulated solely with nonstandard definitions (rather than the epsilon-delta variety).  


With kind regards,

Sam Sanders