[FOM] Friedman's Simplified Foundations

[Sandy Hodges]

I reproduce them again:

>>>>>>>>>>>>>>
We have variables of only one sort, but with the following 7
nonlogical symbols (in addition to the logical symbols
not, and, or, implies, iff, forall, therexists, =).

Sets. (Unary predicate symbol).
Membership. (Binary relation symbol).
Ordered pairing (Binary function symbol).
Real numbers. (Unary predicate symbol).
0,1. (Constant symbols).
<. (Binary relation symbol for ordering of reals).
+. (Ternary relation symbol for addition on reals).

1. Everything is exactly one of: a set, an ordered pair, or a real
number,
2. Only sets can have an element.
3. If two sets have the same elements then they are equal.
4. <x,y> = <z,w> iff (x = z and y = x).
5. 0,1 are distinct real numbers.
6. +(x,y,z) implies x,y,z are reals.
7. x < y implies x,y are reals.
8. Usual axioms that reals are an ordered group with 0,1,+,<.
9. Every nonempty set of reals bounded above has a least upper bound.
10. The set of all reals numbers exists.
11. Pairing, union, power set, separation, replacement, foundation,
choice.

Rationals, integers, natural numbers, are all defined as certain real
numbers. Functions are sets of ordered pairs.
<<<<<<<<<<<<<<

A few minor points:

The "{ x e r | phi(x) }" notation might be worth mentioning.

<x, y> = x + iy
seems like something a mathie wouldn't say, but if reals exist and
complex numbers must be defined, it is true.

"Everything is exactly one of: a set, an ordered pair, or a real number"

To have this as an axiom just means that the set of axioms for math
makes an assertion about the real world which math has no business to
make, an assertion which is in any case false (it denies the existence
of the person making it, for one thing).   Rather, one should say that
only reals, the null set, and constructions of sets and pairs based on
these urelements are the subject of mathematics.

To have "Everything is exactly one of: a set, an ordered pair, or a real
number" as an axiom gives rise to another, more subtle problem.   In
group theory, for example, we say : Let X be any set on which is defined
any ternary relation z, satisfying such and such properties. [ such as
(\/ a, b, v, w) ( z(w,a,b) & z(v,a,b) => w=v) ]  In that case, we say, X
has such and such a property.   If it were the case that everything is
exactly one of: a set, an ordered pair, or a real number, then we would
know that the set X is ultimately decomposable to the urelements of the
null set and the real numbers.   But to make use of this fact would be
illegitimate in group theory.

Is a point in plane geometry really an ordered pair of reals?   What is
a point in non-Euclidean geometry?   I think it is always legitimate to
postulate a class of urelements which shall have only those properties
the mathematician chooses to give them.

Non-constructive existence proofs are usually labeled as such, and a
later constructive proof of the same result is always important.   It
might be best to reserve the term "axiom" for those things about which
there is a very strong consensus.  Then a proof of some T using AC, for
example, could be regarded as a proof of AC=>T.   Mere courtesy to those
who doubt AC suggests that a proof using it should be labeled as such,
and writing "AC=>" in front of it is as easy a way to do that as any.
------- -- ---- - --- -- --------- -----
Sandy Hodges / Alameda,  California,   USA
Remove THESE WORDS from SandyTHESEhodges at AlamedaWORDSnet.net for e-mail
address.
Note: this is a new address as of 20 June 2003