FOM: second-order logic is a myth

[Stephen G Simpson]

It seems that Robert Black's argument for second-order logic is
leading him to make some very odd remarks.

Robert Black 13 Mar 1999 14:14:05 writes:
 > From this point of view, second-order logic is an essential tool
 > for the *expression* of mathematical theories.  It can do this, and
 > first-order logic can't, ...

It's very odd, if not absurd, to say that first-order logic can't
express mathematical theories.  All of mathematics can be formalized
in ZFC.  This is very well-understood and well-established
conventional wisdom in f.o.m.  If you insist on contradicting this
conventional wisdom, you need to make a very strong and novel case
against it.  You haven't even tried to do that.

 > ... for the realist, it's not just that you can prove in
 > first-order ZF that, say, second-order arithmetic is categorical,
 > but that it really *is* categorical ...

This is a very odd remark, because for the realist, the fact that a
statement X is provable in ZF *implies* (i.e., is stronger than) the
fact that X is true, but not the other way around.

A more correct remark would be the reverse: `For the realist, not only
is categoricity true, but in addition it's provable in ZF.'

 > [second-order logic] is active in providing the premises from which
 > we then reason in first-order logic.  For example, I think the
 > intuitive justification of the induction schema in first-order PA
 > is the induction axiom of second-order PA, and I think the
 > intuitive justification of the separation schema in first-order ZF
 > is given by the second-order separation axiom.

This is an often-stated point, but I don't think it's correct, either
historically or logically.

It seems to me that the induction scheme in PA and the separation
scheme of ZF are justified not by second-order logic but rather by
naive (i.e., informal) considerations about sets and classes, followed
by straightforward formalization of these naive considerations within
the predicate calculus.

One naively believes that any set of nonnegative integers has a least
element, so one asserts this for all sets describable in the language
{+,x,0,1,<,=} and this is the induction scheme of PA.  (Compare also
the close relationship between PA and ACA_0.)  One naively believes
that the intersection of any class with a set is a set, so one asserts
this for all classes describable in the language {epsilon,=} and this
is the separation scheme of ZF.  Similarly for the replacement scheme
of ZF.  (Compare also the close relationship between ZF set theory and
VNBG set-class theory.  Morse-Kelley set-class theory came later.)

Historically I think this is pretty close to how PA and ZF were
arrived at.  Historically, second-order logic didn't play a role.  Did
it?  In any case, even if it did play a historical role, that role was
not logically essential.  Naive considerations about sets and classes
would have been sufficient.

[ Throughout this posting, when I say second-order logic, I am
referring to second-order logic with `standard' rather than Henkin
semantics.  My remarks do not apply at all to second-order logic with
Henkin semantics, which is really a system of first-order logic.
Advocates of second-order logic frequently ambiguate on this important
distinction. ]

-- Steve