[FOM] real numbers/flexible set theory

[Harvey Friedman]

Reply to Blass 9:13PM 6/19/03 and Tennant 2:04PM 6/20/03.

This is just a clarifying remark.

Recall my axiomatization of set theory from 1:23AM 5/4/03:

>
>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.
>

And my followup of 5:35AM 5/14/03:

In light of Blass's posting, it seems like a good idea to consider 
the weakening of this system in the following obvious way:

SIMPLY REMOVE AXIOM 1 ENTIRELY.
REPHRASE AXIOM 2 AS "ANYTHING WITH AN ELEMENT MUST BE A SET".

This rephrasing is merely suggestive.

This accommodates the possibility of unforseen new kinds of 
urelements, and also doesn't commit us to anything about what orderd 
pairs are, really, or what real numbers are, really.

One might distinguish this system from the original one with axiom 1, 
by giving descriptive names like "committed set theory" and 
"uncommitted set theory", or some such thing.

Then

"the real numbers are exactly the Dedkind cuts of rationals"

is neither provable nor refutable in the above theory (without 1). Also

"the real numbers are exactly the equivalence classes of Cauchy 
sequences of rationals under the appropriate equivalence relation"

is neither provable nor refutable in the above theory (without 1).

Then a crucial question is this. When is it legal to declare some 
urelements and some principles about them?

Answer: when you can prove existence and uniqueness up to appropriate 
isomorphism of the structure one is introducing.

RADICAL answer: when you can prove existence of the structure one is 
introducing, up to isomorphism.

Obvious theorems show that for existence and uniqueness above, one 
need only consider the purely set theoretic part of the universe, 
inside this system.

This whole thread "Real numbers" in which a lot of FOM subscribers 
have participated, makes me think that there is a profitable subject 
that might be called

"flexible set theoretic foundations"
"flexible set theory".

There are still some nonobvious issues. Principally: how do we 
organize this into a unified gold standard? One needs to work out in 
great detail the model of mathematical practice that all of this 
suggests, that even takes account the existence of independent 
research mathematicians who don't always cooperate with the same 
terminology. One needs reconciliation protocols.

What is nice about the (less than honest) approach in pure set 
theory, ZFC, is that it serves as a (less than honest) unified gold 
standard. We would like to inject honesty.

Harvey Friedman