[FOM] Computational Nonstandard Analysis

[Sam Sanders]

Dear Harvey,

> In 1966 when I was an undergrad at MIT, I formulated the following
> system PA*, and proved that it is a conservative extension of PA. The
> language is 0,S,+,dot, and a predicate for "being standard".
> 
> 1 The usual axioms for successor, +,dot.
> 2. Induction for all formulas in the extended language.
> 3. There exists a nonstandard integer.
> 
> I remember sitting in Gerald Sacks' office at MIT and telling him
> about this system and the conservative extension proof. He was
> interested, and spoke to A. Robinson about it, Sacks told me that A.
> Robinson was disappointed that it was a conservative extension. All
> three of us of course were well aware that this did not preclude that
> nonstandard arguments could be useful even though they can be
> systematically a priori eliminated.
> 
> Does this fit into the history?

The system you describe here is a very special case of a fragment of Nelson’s IST (based on Peano Arithmetic).   

More general conservative extensions (with fragments of IST) of PA and HA in all finite types and extensionality are studied in the following paper:


Benno van den Berg et al, A functional interpretation for nonstandard arithmetic, APAL, 2012.


The systems by van den Berg et al are special/new/great in that they come with a “term extraction theorem” as follows:  


TERM EXTRACTION THM

Let A  be a formula which does not involve the standardness predicate.

If the nonstandard extension of E-PA^\omega proves “for all standard x, there is standard y such that A(x,y)” , 

then from this proof, a term t from Goedel’s T can be extracted such that E-PA^omega proves “for all x, there is y \in t(x) such that A(x,y)”


TWO NOTES:

The term t provides a finite sequence of witnesses, i.e. t(x) is not a witness to “exists y”, but a finite sequence of possible witnesses.  

A similar “term extraction theorem" holds for E-HA^omega, and the recent system by Ferreira and Gaspar (APAL2015). 


MATHEMATICAL RELEVANCE OF TERM EXTRACTION

The term extraction theorem allows us to extract computational info (terms from Goedel’s T) from proofs in NSA of a specific formula class, 
namely formulas of the form  “for all standard x, there is standard y such that A(x,y)” , where A does not involve the standardness predicate.  

An essential question is:  WHICH MATHEMATICAL THEOREMS FALL INTO THIS CLASS OF FORMULAS?

ANSWER:  ALL theorems of *pure* Nonstandard Analysis, i.e. theorems formulated solely with the nonstandard definitions of 
continuity, differentiability, compactness, Riemann integration, ….

Again, see the paper http://arxiv.org/abs/1508.07434 for more details.  
An example is provided below.  

> And I think the FOM subscribers would be interested in Sanders
> continuing with a SLOW explanation of at least a couple fundamental
> results of his or more or less his. I think Sanders thinks a lot about
> Reverse NSA? But I don't think Sanders wants to sit on top of ZFC.

Indeed, Reverse NSA is the topic of study, using (fragments of) the systems by van den Berg et al.  
From equivalences in Reverse NSA, one can extract “explicit” equivalences in normal RM.  

AN EXAMPLE of such an extraction:

a) NONSTANDARD EQUIVALENCE:

Here is a nice equivalence from *pure* NSA, provable in a weak system of NSA based on PRA:

“The Transfer principle limited to Pi_1^0-formulas” <=> "Every standard monotone sequence of reals in the unit interval, nonstandard converges”  (D)


(A sequence x_n nonstandard converges if for all nonstandard N, M, x_N ≈ x_M., i.e. the terms of the sequence of infinite index are infinitesimally close).  


b) TERM EXTRACTION:

From a proof of the equivalence (D), one can extract terms s, t  from Goedel’s T such that Kohlenbach’s base theory  RCA_0^\omega proves

"If mu is Feferman’s non-constructive search operator, then t(mu) is the rate of convergence for any monotone sequence in the unit interval."  (E)

and 

“if xi of type 1->1 provides the rate of convergence for any monotone sequence in the unit interval, then s(xi) is Feferman’s non-constructive search operator. " (F)


Note that the non-constructive search operator is essentially the functional version of ACA_0


c) CONCLUSION:  Equivalences like (D) involving NSA can be “mined” to obtain “explicit” equivalences like "(E) AND (F)”.  


I hope this hints at what I am trying to do.


Best,

Sam