[FOM] Apartness topology and (constructive) nonstandard analysis

[Sam Sanders]

> I would like to propose the following thought experiment, extending your
> argument. Every proof using the real numbers can be paraphrased using the
> rational numbers only. I have it on Harvey's authority that this is a feasible
> project.  

Well, the late Pat Suppes proposed such a program (“Dispensing with 
the continuum”) about 25 years ago.  

He and his co-authors (Sommer, Chuaqui, Alper) developed basic math (intended for physics) using only 
the hyperrational numbers *Q, (the fraction field resulting from the hyperintegers), 
i.e. an infinitesimal calculus in which there is no notion of “real number”.    

Then, one proves (either by hand of via meta-theorems) that one can replace in a given theorem
infinitesimals by “very small rationals”, while keeping the theorem true.  

The theorems proved in this style are not too complicated, but complications 
build up along the way.   At some point, the math is no longer manageable.  

> I agree with you
> (Hendrik) though that the mathematical possibility of paraphrazing arguments
> in terms of narrower number systems is interesting in its own right, and is
> close to the spirit of Reverse Mathematics.

One does run into the problem of “faithfulness”, i.e. how faithful 
is the representation?  Even the coding of mathematical objects
in second-order arithmetic as done in RM is not without problems, as discussed
here recently.  

Best,

Sam