FOM: sharp boundaries/tameness

[Harvey Friedman]

Some mathematicians do mathematics sometimes without the intention of it
being "completely rigorous". In fact, this is norm

i) when trying to settle a mathematical question;
ii) even after it is settled, in preparation for writing down or lecturing
on a "proof";
iii) when doing computer assisted areas of mathematics roughly called
"experimental mathematics".

The resurrection of the infinitesmal idea via Abraham Robinson is a
contribution to f.o.m. in that clearly many people use this idea - even
without considering or knowing any rigorous treatment of it - in connection
with at least i) and ii), and even perhaps iii).

However, the importance of this contribution to f.o.m., although real, is
limited by the following considerations and observations.

1. When presenting "completely rigorous" proofs, mathematicians obviously
avoid use of infinitesmals, and "essentially" work within the standard set
theoretic f.o.m. framework. The precise meaning of "essentially" here leads
to a lot of issues that have been discussed on the f.o.m. relating to
automated proof checking systems, Mizar, etcetera.

2. In their "completely rigorous" mode - the normal polished professional
mode - mathematicians insist on using only concepts with sharp or precise
or absolute boundaries. Infinitesmals fail on this account because of such
questions as "which reals are infinitesmal and which are not infinitesmal?"

3. Although there was a lot of initial promise, the infinitesmal idea has
not proved to be a generally recognized effective technique for proving new
theorems or simplifying existing proofs of theorems. It would be
interesting to see just how the case stacks up in 2002. I recognize that
some people would challenge the correctness of this conventional wisdom.

4. Skipping a bit in the discussion, Robinson considers a proper elementary
extension of the real line augmented with all multivariate relations on the
real line. Using the axiom of choice, one proves the existence of such a
proper elementary extension.

5. In connection with the "sharp boundary" criteria, we know that there is
no explicit definition of such a proper elementary extension. More
precisely, there is no formula of set theory, phi(x), such that ZFC proves

i) there exists a unique x such that phi(x);
ii) x is such a proper elementary extension.

6. This leads to the following line of investigation. We know that if we
wish to find a proper elementary extension of the reals with just certain
relations on the reals, then we CAN find an explicit elementary extension.

7. Specifically, the field of reals (in this context, the reals with the
addition and multiplication relations) does have an explicit proper
elementary extension (in the sense above, and even stronger senses). It is
written R[x], where x > 0,1,2,... .

8. However, if we also add a predicate for "being an integer" then it is
well known that there is no explicit proper elementary extension.

9. WHAT IS THE RELATIONSHIP BETWEEN AN EXPANSION OF THE FIELD OF REALS
BEING "TAME" AND IT HAVING AN EXPLICIT PROPER ELEMENTARY EXTENSION?