[FOM] Friedman's Simplified Foundations

[Harvey Friedman]

Reply to Taylor 7:21PM 5/13/03.

Taylor:

>A few days ago Harvey Friedman made a post which I was expecting to see
>a lot of follow-up to, but as there has been none, I will make a naive
>comment or two.
>
>It was his approach to the problem of what the reals etc "really" are,
>(Benacerraf style).


Friedman

>
>>  This is an old, but interesting issue. Of course, it is one
>  > that mathematicians have learned to be totally uninterested in.
>


Friedman

>
>
>>  My favorite way of trying to deal with this unpleasant philosophical
>  > situation, is as follows.
>
>...

Friedman

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

Taylor


>Wonderful, IMHO.   I have a query or two, though, if Harvey or others
>would like to enlighten my naivety.
>
>(a) How does one get multiplication very easily?  Or at all?
>
>I think this fails the "as is actually done" test - most mathies would
>put + and x on equal terms, and give axioms for both together.

Just define dot as the unique function such that

(reals,+,dot,<,0,1) is an ordered ring.

Obviously, there is a strong sense in which whether to have dot as 
primitive or not on top of 1-11 is arbitrary.

>
>(b) Whereabouts is Induction?  
>
>I can't detect how it is supposed to come out of the above.
>Does the "set of reals" axiom stand in for the usual axiom of infinity
>here?  Does that not make it very cumbersome to extract Induction?

Just define the integers as the least subgroup of the reals containing 1.

Induction is derived immediately from 9.
>
>(c) There remains a Benacerraf-style criticism of the distinction made
>between ordered pairs and ordered triples (and higher).  Most mathies
>would regard ordered pairs and triples as being virtually coeval.
>Yet ordered pairs retain their pre-eminence, mainly because of their
>necessary use in defining functions extensionally.  It may be that this
>problem is insuperable; but still it is a minor aesthetic blemish.

A "mathie" still needs to define n-tuples, where n is an arbitrary 
integer >= 1.

I strongly recommend, pedagogically and foundationally, that this be 
done by a function whose domain is {1,2,...,n}. I think mathies would 
agree that this is probably the best way to do it uniformly in n, and 
would at least reluctantly agree that it needs to be done in a non ad 
hoc way. They would reluctantly agree that my recommendation is 
better than leaving it as primitive.

Here is my reasoning in more detail.

You don't want some special way of treating 3-tuples that does not 
lift generally to n-tuples.

So the competing idea would be to treat n-tuples as an iteration of 
ordered pairing (say associated to the left).

However, this is ad hoc: e.g., why not associate to the right?

But the way I recommend n-tuples as functions, no ad hoc feature of 
this kind appears.

>
>(d) Above, there is only one sort of variable, with predicates
>for being numbers, pairs, or sets.  This is very un-everyday-like. 
>
>Most mathies would (I suspect) be happier with (essentially) three sorts
>of variables for these, distinguished (as almost always) by notation -
>small letters for numbers; caps for sets; and bracketted pairs for pairs.


This is a big issue. I didn't want to go down this path, and bundle 
all such issues up as one. This kind of issue occurs across the 
logical landscape, well beyond math.

For instance, one should be able to - and does in practice - use all 
sorts of abbreviations, and all sorts of conventions about letting 
variables range over certain things, even just temporarily, and also 
the introduction of incompletely defined function symbols, and also 
various variable binding operators, like {x+y: x in G and y in H}, 
etc.

My 1-11 was meant to address a particular perplexing and notorious 
issue, and NOT EVERY logical issue surrounding actual mathematical 
practice.

>
>(e) I don't understand the following at all - would someone please explain:
>
>>  One proves that every sentence is provably equivalent to a sentence
>  > that mentions only epsilon.

What's the problem? Play with this to try to give a counterexample, 
and you will fail (unless I have made a mistake), and get a feel for 
why this is true.

One defines a formal translation of every formula in the language of 
1-11 into the language of epsilon,=. One proves an appropriate 
equivalence of the translation within 1-11, that is enough to show 
that the translation of every sentence in the language of 1-11 is 
outright equivalent to a sentence in epsilon,=.

One uses the crucial fact that one can prove in 1-11 that there is a 
unique isomorphism from the primitive reals of 1-11 into your 
favorite purely set theoretic real numbers.

There is also a conservativity result. There is such a thing as T = 
"ZFC with a set of urelements of cardinality the continuum". Then 
every sentence with epsilon,= is provable in 1-11 if and only if it 
is provable in T.