[FOM] Answer to Friedman, Paulson, and Caballero

[Sam Sanders]

Dear FOM,

I second Larry Paulson’s claim that his results, obtained together with Fleuriot, are of the following nature: 

> Moreover, results derived using non-standard methods can be transferred (again making no additional assumptions) to the standard real numbers. Surely this leaves no room for philosophical objections, provided one accepts higher order logic, which is a weak fragment of set theory.


However, experience bears out that criticism of Nonstandard Analysis (NSA hereafter) is not always based on rational argument.  

My answer to Connes’ criticism of NSA is: (essentially RTFM)

> Connes criticizes Leibnitz's approach as follows (free translation from French): Every nonstandard real number determines, in a canonical way, a subset of [0,1]
> which is not Lebesgue measurable, hence such numbers do not exist. 

I discuss Connes’ criticism of NSA in excruciating detail (and debunk it) in the papers that were mentioned earlier in this thread.  
Just so we are on the same page, here are two papers those interested in Connes’ criticism may consider reading: 

The paper “Formalism16” was published in Synthese and discusses (and debunks) the criticism of Bishop and Connes on (what José calls Leibniz style) NSA:

https://arxiv.org/pdf/1701.05066.pdf

This paper is written (or should be so) for a philosophy audience, so is therefore fairly elementary.  

The paper “To be or not to be constructive” is a very introductory and very detailed study of the constructive content of NSA.  The latter
is not constructive math, but contains so much constructive content that it can be said to inhabit the twilight zone between constructive and
non-constructive (and hence the title):

https://arxiv.org/abs/1704.00462

This paper was published in the “Indigationes Mathematica” journal, as part of the “Brouwer, 50 years later” volume. Hence, the least
one can say is that constructivists "not not approve of it".    


The above content in a nutshell (but do read the aforementioned papers):  Connes criticism starts from an incorrect interpretation of NSA, namely:

On one hand, the “non-constructive nature" Connes points out, pertains to models of NSA, not the theory itself.  
Do we reject theories of math or physics because the models are non-constructive? I think/hope not.  Also,
Connes freely uses strong axioms of set theory for his theories; these same axioms allow you to build
the models of NSA he criticises.  So Connes’ criticism seems metaphysical rather than logical in nature.

On the other hand, there is a syntactical approach to NSA, pioneered independently by Nelson and Hrbacek, 
in which the problem of models (by definition almost) goes away.  The most famous system is Nelson’s IST.  
IST is a conservative extension of ZFC and any sentence of IST can be translated (by an algorithm) to a sentence of ZFC.  
It should also be noted that most results in IST and Robinsonian NSA can be routinely translated back and forth. 


Next, as to the earlier question by Friedman on the computational content of NSA:

If one restricts everything to the finite type part of IST, then (a delicate refinement of) Nelson's algorithm even yields computational content:
based on work by Benno van de Berg et al (APAL 2012), I show in the above papers that this algorithm converts theorems of NSA to 
theorems of constructive/computable mathematics.  In particular, the algorithm makes the following conversions:

nonstandard continuity 	<=> 	eps-delta-continuity with a modulus  
Transfer 				<=>  comprehension (with a dash of choice)
Standardisation for reals	<=>  open-cover compactness
nonstandard convergence <=> convergence with a modulus
space can be divided    	<=> totally boundedness
into infinitesimal-size pieces

Note that the realisers for the right-hand side can be ‘read off’ from the proofs in NSA.
Moreover, only the nonstandard axioms of IST contribute to these realisers: the axioms
of ZFC do not.  

> By the way, I am not sure if Connes criticism apply to Moerdijk's intuitionistic approach to nonstandard analysis: https://repository.ubn.ru.nl//bitstream/handle/2066/129065/129065.pdf?sequence=1

It all depends on how hard it is to build one of their models.  I seem to recall these models can be built within Martin-Loef type theory  (the official metatheory).  
On the other hand, some of their models do satisfy LLPO, a non-constructive principle.  

Best,

Sam