[FOM] Coding in Z(F)C

[Robert Smith]

Recent posts by Avron and McCarthy, as well as joeshipman, raise questions
about "avoiding coding".

One point is that objects such as ordered pairs and von Newmann ordinals are
introduced by a kind of coding. joeshipman responds that we could
alternatively add axioms for ordered pairs and integers and get a similar
result without the appearance of "coding".

An underlying issue here is the relation between axioms and (non-creative)
definitions in a theory.  We seem to treat definitions as totally
transparent, justified by their eliminability in the sense of Beth's
theorem.

Definitions certainly add something to a theory in the overall sense.  They
increase the expressive power and reduce the computational complexity of
statements, and identify objects that need to be given further study.

For example, a proof checker/theorem prover has to contend with definitions
and theorems in very much the same way as it treats the primitive axioms.

By themselves, the axioms of ZFC (this is especially true of just Z) simply
suggest a universe of sets.  The fact that natural numbers, rationals,
reals, etc. (and on from there) can be constructed out of these raw
materials is remarkable.  But that construction--the definitions and
resulting theorems and metatheorems--is important conceptually along with
the power of the initial axioms.


Bob Smith