[FOM] Extended response to Friedman (Comp. NSA)

[Sam Sanders]

Dear Harvey, dear FOM,

So the previous email got stuck somewhere.  Here we go again:

> So I can tell that you are living in a different galaxy than classical nonstandard analysis in the sense of Abraham Robinson with his ultra power constructions. 
> Since your are talking about nonstandard analysis is a very fine grained delicate setting, we need to proceed with SLOW explanations.

I hope the following is OK:

Nelson's IST is indeed different from Robinson’s NSA (as explained next), but proofs from the latter can “often" be imported into the former. 
The “often” can be given a rather precise meaning, as we will see.  Using your metaphor, Robinson’s NSA and Nelson’s IST are parallel universes which look very similar in many places
but can be very different in some places.  (I would make a comparison between countries as an illustration)


> So I would like to understand what you are doing SLOWLY. Very few readers have any idea what IST is and what Nelson was up to. We need to start with your explanation of Nelson. 

Nelson’s IST was developed in answer to Robinson’s NSA as follows:


ROBINSON’S NSA

Robinson’s “semantic” approach to NSA is based on the construction of a nonstandard model (nowadays usually via the well-known ultrafilter construction).  Nonstandard models were known to Skolem already,
but they are not so useful from a mathematical point of view.  Robinson’s contribution was to prove various theorems which *connect* the nonstandard model and 
the original structure.  With these theorems in place, one can jump “back and forth” between the original structure (“the standard world” consisting of standard sets) and the nonstandard model ("the nonstandard world” in which also nonstandard sets live).   In particular, these *connections* between the standard and nonstandard world allow one to do “infinitesimal calculus a la Leibniz” and NSA in general.  


The following are three important theorems (going back to Robinson) connecting the standard and nonstandard world:

TRANSFER:  A formula from the original language (say of ZFC) holds in the standard world IFF it holds in the nonstandard world (parameters from the standard world are allowed)  

STANDARD PART:  For every set (from the nonstandard world), there is a set from the standard world which has the same standard elements.   

IDEALISATION:  An intuitive description is best: One can bring all quantifiers pertaining to standard objects up front, i.e. “pull them through” normal quantifiers (pertaining to the entire universe).  

(We are ignoring “saturation” for the moment).  

Transfer expresses that the standard and nonstandard world have the same properties (in the original language), going back to Leibniz’ similar idea.  

Standard Part allows one to “go back” to the standard world after a construction in the nonstandard world.  It is a kind of inverse of the well-known “star morphism”.  


NELSON’S IST

Nelson’s “syntactic” approach to NSA is essentially an axiomatic version of Robinson’s NSA:  Nelson adds a new predicate “st( x ) “ to the language of ZFC, to be read “x is standard” 
and extends ZFC with three new axioms governing “st( x )", namely Transfer, Standard Part, and Idealisation, which are versions of the above theorems.  The new system is called IST, 
and is a conservative extension of ZFC.   IST has a lot more nice properties beyond the scope of this email.  


By the previous, IST certainly LOOKS like Robinson’s NSA, but there are some important (IMHO fundamental) differences too 

1) EXTENSION: Robinson’s NSA provides an *extension* of the original structure.  Lots of new elements are added:  The sets *N and *R (the hypernaturals and hyperreals) have rather high cardinality compared to N and R (the naturals and the reals in the original structure).    Nelson’s IST does not involve an extension:  It just labels some elements "standard", but does not introduce any new ones.  

2) COMPREHENSION: In IST, one CANNOT form the set:  { x : st(x) AND A(x) } where A is a formula in L_ZFC.  Such a set is an example of what Nelson calls “illegal set formation”.  

By contract, in Robinson’s NSA, one of course has N and *N (the naturals and the hypernaturals), and the former is the set of all standard numbers in the latter.  
In general, one can always form the “external" set {x : x is standard AND A(x)} in Robinson’s NSA.  

3) LOEB MEASURE:  Due to the absence of external sets, the Loeb measure is not available in IST.  


SOME PROPERTIES OF IST

Because of 1) and 2), IST does not have the oft-cited problems Robinson’s NSA has.  An obvious example: 

Tennenbaum’s thm states that plus and times +_M and x_M from a nonstandard model M of PA are not recursive in the plus and times from the standard model of PA.  This theorem does not apply to (NSA in the spirit of) IST:  IST simply does not allow one to form the set “+ limited to the standard numbers”.    


Because of 3), one has to pay a price when using IST:  One cannot have the (full) Loeb measure.  
By contrast, Simpson and Yokoyama have studied weak versions of the Loeb measure in sosoa (in the same way one studies the Lebesgue measure).    


In general, proofs/techniques/constructions not exploiting external sets in an essential way, can be translated from Robinson’s NSA to Nelson’s IST.  

I am neutral on the topic which approach (Robinson or Nelson) is ultimately “best”.  That said, Nelson’s IST, being syntactic in nature, is more amenable
to proof-theoretic analysis, as shown in my paper:  

https://dl.dropboxusercontent.com/u/4558565/Sanders_Unreasonable%20effectiveness%20of%20NSA.pdf

> 2) In the case of Nelson’s IST, the following is meant by “computational foundation”:
> From the proof of a theorem of *pure* Nonstandard Analysis (i.e. only involving the nonstandard notions of continuity, compactness,…), one can extract
> the proof of the associated “effective” theorem.  The latter is either a theorem of constructive/computable analysis, OR an equivalence/implication from
> Reverse Math.  The “effective” theorem has its existential quantifiers witnessed by terms also extracted from the original proof.  
> Conclusion: In other words, one can just “do pure Nonstandard Analysis” and extract the effective version at the end.  This effective version gives one
> a lot of computational content (as good as the proof can provide).  In this way, NSA provides a “computational” foundation.  
> 
> ​We need some slowly presented nice examples of such extractions. 

The simplest example is perhaps the following:  

(i) Let P_0 be the conservative extension (as defined in the above paper) of Kohlenbach’s system RCA_0^\omega (which in turn is a conservative extension of RCA_0).  

(ii) The system P_0 proves the following equivalence:

“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).  

(iii) From a proof of the equivalence (D) in P_0, one can extract terms s, t  from Goedel’s T such that Kohlenbach’s 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)

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

> 
> This usual kind of nonstandard analysis has been mostly used for doing rather abstract analysis, far far far above what you are concerned with, which is computational issues. 

Agreed, but in the aforementioned paper, relatively “strong” principles are treated too.  An example deals with equivalences from the RM of Pi_1^1-CA

Consider the following nonstandard equivalence:

“The Transfer principle limited to Pi_1^1-formulas” <=> “Every standard countable Abelian group, is a the sum of a (standard and divisible group) and a (standard and reduced group)”  (A)

From a proof of (A) in P_0, one extracts two terms s, t from Goedel’s T such that, provable in RCA_0^\omega, 

If mu_1 is Feferman’s version of the Suslin functional, then t(mu_1) provides a divisible and a reduced group for every countable Abelian group.  (B)

and

If xi  provides a divisible and a reduced group for every countable Abelian group, then s(xi) is Feferman’s version of the Suslin functional.   (C)


> HOWEVER, I am vaguely aware of some situations where sometimes people like to use nonstandard arguments to get some computational information out at the end, arguably "easier" or "differently" than they would if they got their hands really dirty. WHAT are the best examples of this? WHAT about forging tools to eliminate this, and retain any computational content? 

Well, I provide examples of such in the paper:   From a proof of a nonstandard theorem, one can extract the associated “highly constructive” Herbrandisation (not involving NSA).  
In turn, a proof of the Hebrandisation allows one to re-obtain the nonstandard theorem.  

An example of such an Herbrandisation is given above:  

" (B) AND (C) “ is the Herbrandisation of (A).  

and 

“ (F) AND (E) “ is the Herbrandisation of (D).  

In other words, one can extract from the proof of (A) in P_0, two terms s, t of Goedel’s T such that "(B) AND (C)" is provable in Kohlenbach’s RCA_0^\omega.  
Vice versa, a proof of "(B) AND (C)” in the latter (for fixed terms s, t) yields a proof of (A) in P_0.  

Of course, these “Herbrandisations” can be obtained as theorems “an sich” without NSA, but that would be a lot harder, I think. 
The reason is that the Herbrandisations contain a lot of computational information.  

Furthermore, the above paper treats two examples of these Herbrandisations in detail:

“nonstandard uniform continuity => nonstandard Riemann integration”  (Section 3.1 at the end)

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

> Also "computational" is a very multifaceted word. All the way from just about any countable piece of mathematics, all the way down to something that can be implemented by a computer in less than a day, available from a major computer company in 2015 for a reasonable price. ​

So my notion of “computational” is closer to the latter:  These extracted terms are in Goedel’s T and are obtained via a specific proof interpretation; I am looking for someone to implement the associated algorithm.  
This should be possible as the proof interpretation seems to only require that one can code finite sequences properly.  

Best,

Sam