[FOM] Coding in Z(F)C; "Heavy-duty" axioms
joeshipman at aol.com
Tue Feb 28 23:03:38 EST 2006
Replying to Avron and McCarthy together:
The way to avoid coding is to have urelements and appropriate axioms
for the integers and the set of integers, and to add "ordered pair" to
the language as a 2-place function. And of course you can introduce
rationals, reals, and complex numbers as primitives, with the
appropriate axioms. The "official" ZFC used in proof theory is shown
once and for all to be equivalent, and no one needs to do any difficult
coding after that if they are working in "ordinary mathematics".
This mirrors mathematical practice, and the five essential
set-theoretical axioms of Union, Powerset, Comprehension, Replacement,
and Choice, which really do all the important work, are unchanged.
If you want a set of axioms that is even more "heavy-duty", you can
introduce Classes as collections of sets defined by formulas, and a
Global Choice function, and Von Neumann's axiom that a class is proper
(that is, not also a set) iff there is another class bijecting it with
the class of all sets. And you can add abbreviations that make the
recursive definition of functions more straightforward, and cardinal
and ordinal notations with the usual properties.
If you are working in Grothendieck-style Algebraic Geometry you can add
the super-industrial-strength Universes axiom, but as others have
noted, that area is so far away from being formalized in ZFC that
there's not much point.
Regarding the earlier point about coding and ZC: what bugs some
mathematicians is the untyped nature of set theory, and the perceived
unnaturalness of sets of different "levels" promiscuously coexisting as
elements of the same set. As long as you stay in ZC, this can be
avoided; it is only for theorems which are too strong for ZC and need
Replacement, where you need to work with limit cardinals, that things
get unavoidably "settish".
More information about the FOM