[FOM] Apartness topology and (constructive) nonstandard analysis

[Frank Waaldijk]

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.

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

Clearly, the existence here cannot be taken constructively, because any
number that we can explicitly construct should be `standard' or
`observable'. Also any ultrasmall number still is apart from 0, which to me
seems in discordance with physics, since when we really measure / observe
phenomena, then the (finitist) idea would be that we cannot tell 0 from an
ultrasmall number.

So it seems that we find ourselves again in the situation that Martin Davis
described some posts ago (regarding `pathology'):

It is certainly worthwhile to study mathematical entities whose existence
> can be proved but for which it can be proved that explicit examples (using
> acceptable mathematical language) can not be given.


In IST and/or Hrbacek's system we can prove the existence of nonstandard
numbers (from the axioms), but we cannot specify a nonstandard number.

My hope was that IST might provide a basis for (ultra)finitism, but such
finitism in my eyes should be constructive. This leaves (in my eyes) a
constructive challenge: can one somehow `constructivize' IST such that the
idea of `vague' elements is preserved yet at the same time the constructive
contradiction: `there exists a vague element' is avoided?

But closer to my home, I do see a partial constructive variant / analogue
of nonstandard analysis (NSA). The use of infinitesimals to define
continuity finds a natural constructive analogue in apartness topology as
developed in my recent monograph Natural Topology (NToP, see
http://arxiv.org/abs/1210.6288, or visit my math page
http://www.fwaaldijk.nl/mathematics.html).

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.

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.

The `natural real numbers' as defined in NToP are equivalent to the usual
real numbers, and the apartness topology on the natural reals is equivalent
to the metric topology. The definitions are simple, so I will give them
below, to meet with Harvey Friedman's question to give examples directly on
FoM, instead of referring to papers.

A. Let Rat = {[p,q] | p, q in Q, p<q} be the collection of closed rational
intervals of positive length. Let O be a formal element, to be thought of
as the infinite interval (-infty, infty). Let Rat* be the union of Rat and
{O}.

For [p,q], [r,s] in Rat put [p,q] # [r,s] iff (s<p or q<r) (the interval
[p,q] is completely apart from the interval [r,s]). By definition, no
interval is apart from the infinite interval O.

Put [p,q] ≺= [r,s] iff (r<=p and q<=s). (the interval [p,q] is contained in
the interval [r,s], we also say [p,q] is a refinement of [r,s]). By
definition, any interval is a refinement of O.

B. A `natural real number' is a sequence x = x_0, x_1,... in Rat* such that:

   1. for all indices n we have: x_(n+1) ≺= x_n and there is an index m
with x_m ≺ x_n (x is a shrinking sequence of nested intervals)

   2. if a, b in Rat satisfy a # b, then there is an index s such that (x_s
# a or x_s # b) (x `chooses' between all apart intervals)

Notice that if x satisfies 1. and 2., then the infinite intersection of
{x_i| i in N} contains precisely one real number. The nice apartness trick
here is that we do not use any metric concept to define convergence.

C. Let Rnat be the set of natural real numbers. For x = x_0, x_1,... y =
y_0, y_1,... in Rnat we put: x # y iff there is an index n such that x_n #
y_n. We put x ~ y iff not (x # y) (this is an equivalence relation).

For [p,q] in Rat* we put: x ≺ [p,q] iff there is an index m such that x_m ≺
[p,q]. We then also say: x belongs to [p,q]. For any b in Rat* we put: [b]
= { x in Rnat | x ≺ b }

A subset U of Rnat is called #-open iff for all x in U and all y = y_0,
y_1,... in Rnat, we can determine at least one of the following two
conditions:

    (i) y # x
    (ii) there is an index m such that { z in Rnat | z belongs to y_m} is a
subset of U.

The collection of all #-open sets (denoted T_#) is called the apartness
topology on Rnat, and also the natural topology on Rnat.

For the classical theorist we should move to the ~ equivalence classes of
Rnat (Rnat/~), and the induced collection T_(#,~). Constructively we
usually just work with the representatives directly.

THEOREM: (Rnat/~, T_(#,~) is homeomorphic to the usual metric topology on
the real numbers.

D. A function f from Rat* to Rat* is called a refinement morphism iff for
all natural reals x, y in Rnat:

    (i) f*(x) = f(x_0), f(x_1), ... is in Rnat (is a natural real)
    (ii) f*(x) # f*( y) implies that x # y

THEOREM: every refinement morphism f induces a continuous function f* from
(Rnat, T#) to (Rnat, T_#).

Of course, the condition (ii) is the constructive formulation of `x ~ y
implies f*(x) ~ f(y)'. One might see a correspondence here with the
nonstandard approach, and one might view the above treatment as `leaving
all infinite things vague'.

A much harder theorem is the following (and I can only prove it using some
Lindelöf-type axiom which holds in CLASS, INT and RUSS):

THEOREM: every continuous function from (Rnat, T_#) to (Rnat, T_#) can be
represented by a function f* induced by a refinement morphism f.

(We can prove in BISH that real functions which are uniformly continuous on
compact intervals can be represented by a refinement morphism, we then do
not need the Lindelöf-type axiom).

There is a lot more to be said, but this post is long enough.

Best wishes,

Frank Waaldijk
http://www.fwaaldijk.nl/mathematics.html
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20150903/2d4a9443/attachment-0001.html>