[FOM] Friedman's Simplified Foundations

[W.Taylor@math.canterbury.ac.nz]

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

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

This is so glaringly true, that I wonder it doesn't have more influence
over the way math-philosophers do their philosophy.  Perhaps it is less
of a motivating factor for strict FOMers, as opposed to math-philossies.

> Also, it has fueled attempts to give categorical foundations and other 
> structuralist attempts.

It might fairly be said that Category theory is the off-mainstream's
definitive answer to the question of providing a serious foundation
for informal structuralist ideas.  It at least provides a very useful
lingua franca for these matters, in distinction to the orthodox ZF one,
which does have some Benacerraf-weaknesses, at least philosophically. Alas,

> when they don't [get complicated], they look too much like set theory
> to really serve as an alternative foundation for mathematics.

...this is also a seriously troubling criticism, I feel.

------

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

This is the part I chiefly wanted to comment on.  It strikes me as
a *very* well-chosen basis for math *as it is actually done* by
practising mathies, and, perhaps more importantly, by teachers.
Certainly it accords uncannily well with the way I approach
undergraduate teaching.

I reproduce it here for ease of reference:


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


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.

(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?

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

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

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

------

And finally, let me praise again this final summary sentence...

> This system puts us pretty much where almost all mathematicians are 
> when they wish to develop mathematics rigorously at the appropriate 
> level of the  undergraduate curriculum (or early graduate).

This is EXACTLY my feeling, and perhaps modulo the minor quibbles in
(a) (c) (d) above, I endorse it whole-heartedly.


> let's see where the discussion leads us.

I too hope there will be other comment!

------------------------------------------------------------------------------
       Bill Taylor                     W.Taylor at math.canterbury.ac.nz
------------------------------------------------------------------------------
            Logic - used by mathematicians but not talked about,
                    & talked about by philosophers but not used.
------------------------------------------------------------------------------