FOM: finite axiomatizability; ACA_0; categorical dis-foundations

[Stephen G Simpson]

Soren Riis writes:
 > Thus ACA_0 (or any other system for analysis) must as far as 
 > I can see contain infinitely many axioms.
 > Sometimes this fact is somewhat disguised because one is using 
 > higher order logic and thus have smuggled in an infinite 
 > axiom-schema in the underlying rules.

Actually, ACA_0 is finitely axiomatizable.  

Since there seems to be some confusion about what ACA_0 is, let me
explain it.  The language of ACA_0 is that of second order arithmetic.
There are two sorts of variables: number variables m, n, ... intended
to range over the natural numbers, and set variables X, Y,
... intended to range over sets of natural numbers.  Numerical terms
are number variables, 0, 1, s + t, s*t.  Atomic formulas are s = t, s
< t, t in X.  Here s and t are numerical terms.  (Note that "in" is
written as epsilon, the membership symbol.)  Formulas are built up
from atomic formulas by means of propositional connectives, number
quantifiers, set quantifiers.

The rules of ACA_0 are the usual rules of predicate calculus,
i.e. classical first order logic.  The axioms of ACA_0 are the
universal closures of:

  1. a finite set of basic arithmetical axioms, e.g.
      m*0 = 0, m*(n+1) = m*n+m, not m < 0, m < n+1 iff (m < n or m = n).

  2. (0 in X and (forall n) (n in X implies n+1 in X))
         implies (forall n) (n in X)

  3. (exists X) (forall n) (n in X iff A(n))

Here A(n) is any arithmetical formula (i.e. no set quantifiers) in
which X is not free.  Note that 3 is an infinite axiom scheme.  It is
known as arithmetical comprehension.  It can be replaced by a finite
set of axioms.

Regarding finite axiomatizability, an appropriate analogy is

       ACA_0 / PA  =  NGB / ZF .  

Here NBG is von Neumann-G"odel-Bernays set theory, with sets and
classes.  ZF is Zermelo-Fraenkel set theory.  ACA_0 is conservative
over PA, just as NGB is conservative over ZF.  ACA_0 and NGB are
finitely axiomatizable; PA and ZF are not finitely axiomatizable.

Riis is saying that finite axiomatizability may be a defect of
McLarty's topos setup.  I don't view this as necessarily a defect.  On
the other hand, I don't regard it as a huge virtue either.  McLarty
wants to make something of the fact that the ZF includes an infinite
axiom scheme, replacement, but in my opinion the replacement scheme is
perfectly natural and doesn't seriously compromise understandability
or readability.

The real question for proponents of "categorical foundations" is, what
do the topos axioms mean?  What picture do they refer to?  Is there an
underlying foundational conception?  I don't think there is one.  In
my opinion, this is a place where topos theory qua "categorical
foundations" falls apart.

-- Steve