[FOM] Apartness topology and (constructive) nonstandard analysis

[Sam Sanders]

Dear Harvey,

The results in my arXiv paper “The unreasonable effectiveness of NSA” apply to what you say below.  
It is perhaps a nice elementary application, which I therefore spell out in detail.  

> I think that the "are found" is misleading. Where are they? If this is
> "constructive" in the usual sense, then the existential statement
> "there exists an infinitesimal" should have an explicitly defined
> witness. The so called existential property is a hallmark of
> constructive systems.

As you point out in the below THEOREM, one cannot find a formula which defines a nonstandard integer.  Similarly, one can never
find an internal formula defining the formula “x is infinitesimal”  (This is called the overflow- and underflow principle btw).  

HOWEVER, it is possible to replace the formula “x is infinitesimal” in MATHEMATICAL theorems by a numerical predicate " |x| < r “  (where r may depend on parameters of the theorem).  

VERY BASIC EXAMPLE:  

a) Suppose the system H (See again van den Berg et al, APAL2012) proves (forall x, y in [0,1])( x ≈ y => f(x) ≈ f(y) ) (f is nonstandard uniform continuous).

b) From the proof in a), one can extract a term t from Goedel’s T such that E-HA^\omega proves (forall k)(\forall x, y in [0,1])( |x-y| < 1/ t(k) => |f(x)-f(y)| <1/k ).  (note that the latter involves no NSA and is the usual constructive definition of (uniform) continuity).  

c) From the proof in b), one ALSO can also conclude that H proves (forall x, y in [0,1])( x ≈ y => f(x) ≈ f(y) ) (since H believes the term t from b) is standard)

Thus, in the case of continuity, all instances of  “z≈0” can be equivalently replaced by the “numerical” predicate “|z| < r”,  where r may involve extra parameters. 

The theme of my paper “The unreasonable…" is that this can be done for all theorems from *pure* NSA, i.e. solely formulated with the nonstandard definitions (of continuity, compactness, diff., …) 

CONCLUSION:  While the standardness predicate cannot be capture by an internal formula, and indeed no single infinitesimal can be captured in a much wider sense, 
one can replace every occurrence of “x is infinitesimal” IN MATHEMATICAL THEOREMS by a numerical formula “ |x| <r” (with parameters .  

This was the “Reverse Mathematics theme” I was hinting at:  Something nice happens when one restricts oneself to mathematical theorems (rather than some formula class).  

Best,

Sam

> 
> THEOREM. In any reasonable extension of systems like ZF by st, a
> predicate for standard objects (or just for standard objects of a
> certain kind, including integers), there is not going to be a formula
> even with st, which, provably in the system, defines a nonstandard
> integer. This is true even if we allow standard objects as parameters.
> 
> When I get going on my numbered postings on NONSTANDARDISM, I will get
> clear about the hypotheses needed for the above.
> 
> Harvey Friedman