[FOM] Higher-order arithmetic as an alternative to ZFC

[Anthony Coulter]

When we make ZFC the foundation of mathematics we use it for four
things:
  1. As a set theory, ZFC provides a background set theory for
     abstract algebra and topology.
  2. As an inductive structure, ZFC provides sufficiently large ordinals
     to justify powerful forms of induction.
  3. As a theory which makes existence claims, ZFC provides "building
     blocks" from which other kinds of objects (e.g. the number systems)
     can be constructed.
  4. As a convenient place to write the axiom of choice.

While there is certainly great appeal in being able to use a single
theory in multiple ways, the "mathematical mindset" encourages us to try
to separate these uses from each other in the hope that doing so will
improve our understanding of how they work. My reflex here would be to
provide these features differently:
  1. Provide sets, functions, and tuples via higher-order logic. We can
     allow sets
  2. Provide ZFC (really ZF) and the set of natural numbers separately,
     so that people can use only as much induction as they need.
  3. Same as (2): the number systems (Z, Q, R, C) are built from the
     well-typed hierarchy of functions, and tuples of natural numbers,
     so if we provide natural numbers separately people can avoid using
     ZFC when it isn't really required.
  4. Rewrite the axiom of chocie in the language of higher-order logic,
     since that's how most sets will be expressed.

My official rationale is that second-order logic is simpler and more
natural than ZFC but it's still powerful enough to do most of your
interesting mathematics. (Many undergraduate textbooks have an
appendix with remedial set theory, but only rarely mention ZFC; all you
really need are the axioms of extensionality and separation, plus an
assumption that there exists some set containing all the objects you're
going to study in the textbook.) Occasionally you need to perform
induction on an unusually complex structure (that is, on a very large
ordinal) and when that happens, ZFC is still there and you can use it,
but now invoking super-powerful induction is like invoking the axiom
of choice---you have to do it explicitly and you're made to feel a
little guilty to encourage you to find a way to redo the proof without
it.

My unofficial rationale may be more philosophically appealing. Reverse
mathematics shows us that you can do an awful lot of math using only
the natural numbers and sets thereof. It *also* shows us that you can
do a lot of math using weaker inductive assumptions; it highlights five
interesting "levels" of induction (the celebrated RCA, WKL, ACA, ATR,
and Pi11CA theories) and Simpson's book hints that a few weaker systems
like EFA might turn out to be of similar interest. So I personally see
induction over the ordinals in ZFC as one of many points on a spectrum
of induction that's bounded below by RCA (or maybe EFA) and unbounded
above by Godel's incompleteness theorem.

Harvey addresses my unofficial rationale by noting that we are free to
add large cardinal axioms whenever we find that plain ZFC doesn't give
us big enough structures to work with. But I would say that if you're
going to keep adding stuff *anyway,* we might as well start weaker and
let ZFC itself be one of the additions. The obvious counterargument
would be that ZFC provides more than induction---it also gives us sets
for abstract algebra---but like I said above I would prefer to get my
sets from higher-order logic.

I believe that this proposal is similar in spirit to Harvey's vision of
sugared ZFC. It's still predicate logic augmented with a set theory and
a traditional inductive structure. The only real differences are that I
want to split set theory from induction, and I want to provide two
sources of induction (natural numbers and ZFC) because in practice I
expect that 98% of the theorems will use the natural numbers only.

Anthony