[FOM] Apartness topology and (constructive) nonstandard analysis

[Sam Sanders]

Dear Harvey,

This is another glimpse at the “strange” world of NSA.  

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

I agree that the existence property (if something exists, we can construct it) 
is a hallmark of constructive systems.  Now, constructive systems of 
Nonstandard Analysis (like the system H discussed in van den Berg et al, APAL2012)
DO have the existence property for *internal* sentences (i.e. not involving the 
new “standardness” predicate).  In fact, a stronger property, called
the “Transfer rule” holds; See Prop. 5.12 in the aforementioned paper.   

For external sentences (i.e. involving the new standardness predicate) like “there exists an infinitesimal"), 
the existence property may not hold.  This is not a surprise, as constructively the standard and entire universe 
"must be” different.  For instance, the Transfer principle cannot hold (as it implies the Turing, Suslin etc functionals), 
implying that the standard and nonstandard world can be different.  

By way of example of this difference, the system H mentioned above proves LLPO^st and MP^st 
(i.e. an omniscience and Markov’s principle relative to ‘st’).  But H proves 
the same internal formulas as E-HA^\omega, i.e. H cannot prove LLPO or LPO.  

Another example, H includes the axiom NCR (again see above paper), which is classically false, yet
H does not prove anything internal which is classically false (as E-HA^\omega does not).  

In other words, H and E-HA^\omega have the same “usual” (that is internal) constructive
content, but the external properties may (must) be very different.  

Best,

Sam