[FOM] Coding in Z(F)C; "Heavy-duty" axioms

[joeshipman@aol.com]

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

-- JS