[FOM] Apartness topology and (constructive) nonstandard analysis

[Frank Waaldijk]

Mikhail Katz wrote:


> Hi Frank,
>
> Thanks for your post.  Note that one should neither conflate the
> notions of "structure" and "construction" nor assume that there are
> any ultrafilter products to be found in the outside world.  If there
> is any message that should have come through clearly in Sam Sanders'
> posting is that Nelson's system represents a syntactic approach.  Here
> infinitesimals are found within the ordinary real number system
> itself.  The system does not suffer from nonconstructive aspects
> any more than the traditional real numbers.  If this seems to be a
> philosophical challenge to the customary platonist intuitions about
> the real numbers, then so be it.
>
> MK
>

I'm sure that if you read my post again, and the ones preceding it, you
will find that I do not conflate `structure' and `construction' nor assume
that there is a non-trivial ultrafilter on N somewhere in the galaxy.
Personally I even doubt I can find pi in the outside world, in that sense
my thoughts tend to ultrafinitism.

I read Nelson's clear paper on IST and the syntactic approach was never in
doubt.

I merely wished to clarify that although IST is not a constructive theory,
I still like it a lot. I also like non-trivial ultrafilters (they are such
fun), and would surely put one above a model train on my Santa Claus wish
list. If some physicist manages to match a phenomenon in physics to a
mathematical theory involving ultrafilter products, then I will enjoy that.
It might set me thinking about whether a simpler constructive theory might
also provide a similar or better match, but that is secondary.

So, once more: although I am primarily interested in constructive
mathematics, I can also enjoy mathematical structures that can only be
defined in classical mathematics. The discussion was whether IST can be,
and perhaps already is, `constructivized' to a theory that is valid in BISH
(say). One of the questions I raised was whether it could be possible to
have a constructive theory in which the statement `there exists an
infinitesimal' is true. [Perhaps this statement is unnecessary in a
suitable constructive syntax-enriching approach, but the question still
interests me.].

Harvey writes:

>  Here
> > infinitesimals are found within the ordinary real number system
> > itself.  The system does not suffer from nonconstructive aspects
> > any more than the traditional real numbers.  If this seems to be a
> > philosophical challenge to the customary platonist intuitions about
> > the real numbers, then so be it.
>
> 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.
>
> 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.


I was raising similar concerns, but Sam Sanders' reply convinced me that I
should first study his references, and ask for some clarifications, before
pursuing this matter further on FoM. (I do have some unripe ideas how to
meet with Harvey's condition of an explicitly defined witness. I'm
completely unsure however if this has not already been done and better than
my unripe ideas.).

Best wishes,
Frank Waaldijk
http://www.fwaaldijk.nl/mathematics.html
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20150907/79743600/attachment-0001.html>