[FOM] Apartness topology and (constructive) nonstandard analysis

[Harvey Friedman]

On Mon, Sep 7, 2015 at 10:17 AM,  <katzmik at macs.biu.ac.il> wrote:
>  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.

When I get going on my numbered postings on NONSTANDARDISM, I will get
clear about the hypotheses needed for the above.

Harvey Friedman