Challenge from Harvey Friedman

[categories <cat-dist@mta.ca>]

Date: Fri, 23 Jan 1998 11:11:28 -0800
From: Vaughan Pratt <pratt@cs.stanford.edu>


I'm taking the liberty of forwarding to the categories mailing list
the following challenge posted by Harvey Friedman to Steve Simpson's
Foundations of Mathematics mailing list.

This is the latest in a long-running engagement about sets vs.
categories on the latter list, recent postings to which can be read at

	http://www.math.psu.edu/simpson/fom/postings/9801.html

Postings with "categor{y,ical}" in their subject lines are the relevant
ones.

Information about the fom list (how to subscribe etc.) can be found at

	http://www.math.psu.edu/simpson/fom/fom-info

As we were fond of saying quarter of a century ago,

Peace
Vaughan Pratt

------- Forwarded Message

Date: Fri, 23 Jan 1998 00:54:20 +0100
To: fom@math.psu.edu
From: Harvey Friedman <friedman@math.ohio-state.edu>
Subject: FOM: Set Theory Axioms

The point of this posting is to give some entirely conventional axioms for
set theory that are a bit simpler than many that are normally given. They
are fully formal. By comparison, look at the axioms of elementary topoi
that are given in MacLane/Moerdijk, Sheaves in Geometry and Logic, A first
Introduction to Topos Theory, Springer-Verlag, 1994, on p. 163. The
difference in complexity is strikingly grotesque.

I challenge anyone to write down their favorite fully formal axioms for
topoi that are sufficient to do real analysis, so we can compare them side
by side with the fully formal axioms I write down here.

Topos theory with natural number object is insufficient to develop
undergraduate real analysis - although many fom postings conceal this fact.
One has to add to topoi: natural number object, well pointedness, and
choice. The latter two are nothing more than slavish translations of set
theory into the topos framework. The "idea" is to take a fatally flawed
foundational idea and force it to "work" by transporting important ideas
from set theoretic foundations.

But the axioms of elementary topoi are already incomparably more
complicated than the axioms for set theory presented here.

Let me start with the dramatically simple axioms of finite set theory.
These amazingly simple axioms are tremendously powerful. We work in the
usual classical predicate calculus with equality and one binary relation
symbol epsilon - which we abbreviate here by "in." It is also useful to use
the constant symbol 0 (for the empty set), the unary function symbol { }
(for singletons), and the binary function symbol U (for pairwise union).
Note that axioms 2-4 amount to the most trivial of definitions.

1. (forall x)(x in a iff x in b) implies a = b.
2. (forall x)(not(x in 0)).
3. x in {a} iff x = a.
4. x in a U b if and only if (x in a or x in b).
5. [phi(0) & (forall x,y)((phi(x) & phi(y)) implies phi(x U {y}))] implies
phi(x).

Here phi(x) is any formula in the language in which y is not free.

That's all! One ***derives*** pairing, union, power set, foundation,
replacement, and choice, from these axioms alone!!! Also, when
appropriately formalized, "every set is finite" and things like "every set
has a transitive closure." These axioms are "practically" complete - an
informal concept that I have alluded to before on the fom.

Now for ZFC. We take a different tack and only use epsilon.

1. (forall x)(x in a iff x in b) implies a = b.
2. (therexists x)(a in x & b in x).
3. (therexists x)(forall y in a)(forall z in y)(z in x).
4. (therexists x)(forall y)((forall z in a)(z in y) implies y in x).
5. (forall x,y)(x in y implies (therexists z in y)(forall w in z)(w notin y)).
6. (therexists x,y)(x in y & (forall z in y)(therexists w in y)(z in w)).
7. (therexists x)(forall y)(y in x iff (y in a & phi)), where phi is any
formula in the language in which x is not free.
8. (forall x in a)(therexists y)(phi) & (forall x,y,z)((phi(x,z) &
phi(y,z)) implies x = y) implies (therexists w)(forall x in a)(therexists
unique y in w)(phi),

A novelty is the axiom of infinity, 6, is simpler than usual; and also
choice and replacement are combined nicely by 8. This allows such a simple
axiomatization in purely primitive notation. Try to right down the axioms
of a topos with natural number object, well pointed, and choice, in simple
primitive notation!! Good luck.

As is well known, ZFC is "practically" complete.

The version in the book on p.163 - which does not even include natural
number object, well pointedness, or choice - requires a very substantial
amount of preliminary abbreviations in order to formalize.



------- End of Forwarded Message