[FOM] Friedman's Simplified Foundations

[Roger Bishop Jones]

Bill Taylor wrote in appreciation of Harvey's
attempt to rewrite the foundations of mathematics,
apparently to avoid the problem of giving the
wrong idea of what the reals really are.

I should like to disagree with both that this is
a good idea, and point out how easy it is to
resolve this kind of problem within classical
set theory.

The first step is to admit (as has long been common)
arbitrary, loose, conservative extensions as
definitions.

i.e. for any property P such that there exists
some x satisfying P to allow "|- P A" as 
"definition" of A.

Starting with the definition of an ordered pair
and working up from there this permits concepts
to be defined without giving too much information
resulting from arbitrary choice among possible
ways of encoding the concepts in set theory.

The reals are then ultimately definable as any
collection which satisfies the relevant axioms,
and any particular representation of the reals
as sets is required only to justify the definition
not as the definiens.

This still leaves everything as a set.
If you don't like that then its easily fixed,
you just weaken the extensionality axiom to allow
urelements.
Having done this the reals could be (but need not
be) urelements.

This is all well understood, involves no
innovation, nor any need to debate which principles
such as induction may have been missed out.
It eliminates any possible misidentification of the
reals or other mathematical entities (by not
saying what they are at all).

Of course, if you prefer a many sorted set theory,
or a type theory (which in fact I do) then those
also are viable approaches (and the desirable
level of abstraction in respect of "what the reals
are" is now pretty much standard in mechanised
developments of mathematics in HOL).

But the simplest complete solution to this problem
is just ZFCU used appropriately.

Roger Jones