[FOM] Apartness topology and (constructive) nonstandard analysis

[Sam Sanders]

Dear Frank,

> I've been interested to see the recent discussions moving from `pathology' to IST and nonstandard analysis.
> 
> Although I really like the idea of IST (and likewise Karel Hrbacek's approach), the drawback to me as a constructivist is precisely its concurrence with ZFC.

There are plenty constructive fragments of IST, just like there are plenty of constructive fragments of ZFC;  For instance: 

van den Berg, Safarik, and Briseid define a system H in their paper “A functional interpretation for nonstandard arithmetic” (APAL, 2012).

The system H is an extension of Heyting arithmetic with fragments of IST and proves the same (internal, i.e. not involving ‘st’) formulas as E-HA^\omega (=Heyting Arithmetic in all finite types with the axiom).  

The latter system is even constructive in the sense of Bishop.  van den Berg et al prove that their approach also works for extensions of H (including adding the law of excluded middle).  

There is something peculiar about H, namely that Markov’s principle, LLPO, and independence of premise (in a certain technical sense) hold for the standard objects.
This however DOES NOT influence the conservation over E-HA^\omega.  Furthermore, without these “non-constructive” axioms (relative to ’st’_, one could not do much with H.  

> And I think at least on the meta-level there is some discord in IST, in the following sense. `Standard' numbers are supposed to be the numbers that we can really define, as opposed to nonstandard numbers which in a sense involve too much effort to pinpoint. In the book mentioned by John Baldwin (Analysis with Ultrasmall numbers), Hrbacek calls the standard numbers `observable'. He uses `ultrasmall' rather than `infinitesimal' because he -like Nelson- doesn't want to really expand the real numbers (through ultrafilter products or such). Then, like in Harvey Friedman's 1966 axioms, we also have the statement: `there exists a nonstandard number'. In Hrbacek's book this is specified as `there exists an ultrasmall number', but one could equally specify `there exists an ultralarge integer’.

I disagree:  As Nelson has pointed out many times, IST does not introduce new objects, in contrast to Robinson’s approach.  In IST (and fragments), one just introduces a new predicate “x is standard”, which some
objects satisfy, and some do not. 

By the way, in the constructive system H, there is no axiom st(x) OR NOT st(x), so certain objects have an unknown status wrt standardness  constructively.  

> Clearly, the existence here cannot be taken constructively,

IST is of course a classical system. In the system H, existence is just the usual constructive existence asw in E-HA^\omega

> because any number that we can explicitly construct should be `standard' or `observable’.

There are more subtle interpretations of “standard”, one is as follows:  

As mentioned above, “there exists” in the constructive system H is just constructive existence.

One can interpret “there exists a standard object” as “this object is relevant for the computation of the objects in the consequent"

For instance, the existence of an object may be a necessary condition of the antecedent of a theorem, but said object
may not be relevant for constructing the objects in the consequent.  

> In NSA one obtains continuity of a real function f by demanding: if x ~ y then f(x) ~ f(y), where x ~ y means that x-y is infinitesimally small.
> In apartness topology, one obtains continuity of a morphism f by demanding: if f(x) # f(y), then x # y.

Well, since Markov’s principle holds relative to ‘st’, these two notions are equivalent in the constructive system H.  

> This latter would seem to correspond more to physics: if f(x) is observably apart from f(y), then x must be observably apart from y.

True, but the two notions you mention are one and the same constructively.  

Best,

Sam