[FOM] Harvey's Categorical Imperative and Nonstandard Analysis

[Sam Sanders]

Dear Harvey,

Neil Tennant quoted you as follows:  

> "I generally don't read technical accounts of anything UNTIL I see a reason 
> to believe that it is worth the effort up front. And that reason normally is
> *do I see a simple short synopsis of what is being accomplished, in
> nontechnical standard language, that is easily digestible and
> reasonably compelling about an issue of fundamental importance?*"

Then let me peek your interest for NSA as follows:  

The so-called Friedman A-translation establishes that Peano Arithmetic (PA)
and Heyting Arithmetic (HA) prove the same Pi_2^0-formulas.   Since HA has
the existence property, the innermost existential quantifier can be witnessed.  
Arguably, Pi_2^0 is only a small class of the arithmetical hierarchy, and includes 
very few mathematical theorems.  

A similar “translation" result holds for fragments of Nelson’s IST and PA (and HA), BUT the associated 
formula class is VERY large: it includes all theorems of PURE NSA, i.e. formulated
with nonstandard definitions (of continuity, compactness, …) rather than “epsilon-delta” definitions. 

Two steps clarify the previous paragraph:


First of all, we have TERM EXTRACTION:

van den Berg et al (APAL2012) define a translation from a fragment of Nelson’s IST to PA (and HA).  
Nelson’s IST is just a syntactical reformulation of Robinson’s NSA, where the language is extended with a new 
predicate ‘st. We write “forall^st x” and “exists^st” for “for all standard x” and “there is standard y”.  

The results by van den Berg et al are similar to those for the Friedman A translation as follows:

IF nonstandard PA (or HA) proves (\forall^st x)(\exists^st y)A(x,y) 

THEN PA (or HA) in all finite types proves (forall x)(\exists y\in t(x))A(x,y)

where the term t is primitive recursive and is extracted from the first proof.  A does not involve “st”.


Secondly, the formula class to which TERM EXTRACTION applies, is VERY WIDE in scope:

Any theorem of “pure” NSA (as defined above) can be brought into the 
“normal form” (\forall^st x)(\exists^st y)A(x,y).  Hence, we can extract
numerical information (the terms t) from proofs in pure NSA.  

CONCLUSION:

The term extraction theorem gives a nice “numerical” interpretation 
to any theorem in Nonstandard Analysis.  In this way, one often produces 
theorems of constructive/comp. math, or (explicit) equivalences from Reverse Math.

Best,

Sam Sanders