FOM: second-order logic is a sterile myth

[Stephen G Simpson]

John Mayberry 23 Mar 1999 16:00:50 writes:

 > Steve Simpson really ought to cease his incessant repetition of the
 > mantra "Second order logic isn't logic because it lacks rules of
 > inference".

Oh, but it's a wonderful mantra.  I like it a lot.  I plan to repeat
it at every opportunity.  I recommend that other people help me by
doing the same.

Another wonderful mantra that I recently discovered is:

      "Second-order logic is useless and sterile."

I plan to repeat this mantra many times also.  See below.

[ 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 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.  Is Mayberry ambiguating on this important distinction? ]

 > Quite apart from being irrelevant to the point at issue, 

No.  I have already demonstrated the relevance.

One aspect of the relevance is that virtually all of the major modern
f.o.m. advances (G"odel etc) involve inference and take place in the
context of first-order logic.  These major advances can't take place
in the context of second-order logic, because second-order logic is
divorced from inference and is therefore useless and sterile.  This is
a key insight of modern f.o.m. research.

How can the advocates of second-order logic shrug off this and other
key insights of modern f.o.m. research?  What is the source of their
confusion?  Could somebody please explain them to me?

 > The very same formal axioms and rules that are complete for Henkin
 > semantics are *sound* for standard semantics.

No, these axioms are not necessarily sound for standard semantics.

It depends on the metatheory.  For example, suppose the axiom of
choice fails in the metatheory.  (The metatheory might reasonably be
something like ZF + DC + AD, which is generally regarded as providing
an interesting alternative to the axiom of choice.)  Suppose also that
our axioms of second-order logic include a choice scheme, as in
Shapiro's system D2, for instance.  Then the axioms for second-order
logic will *not* be sound for the standard semantics.  To say that
Shapiro's choice scheme is sound for the standard semantics is easily
seen to be equivalent to the axiom of choice holding in the
metatheory.  We know that this need not be the case, thanks to modern
f.o.m. research, specifically to Cohen's important work on the axiom
of choice in the context of (first-order!) f.o.m.  Thus Cohen's work
can save us from embarrassment and confusion, provided we take it to
heart.

Similar remarks apply if the metatheory is something like ZFC and our
axioms for second-order logic include an axiom expressing the
generalized continuum hypothesis (GCH).

The previous two paragraphs provide yet another example of the
following well known phenomenon: 

  Virtually every question about second-order logic with standard
  semantics ultimately must be considered in the context of
  first-order logic and first-order axiomatic set theory, in order to
  make any real progress or gain any real insight.

This phenomenon justifies my mantra:

  "Second-order logic with standard semantics is sterile."

 > Might it not be fruitful, for some purposes, to think of ZFC with
 > urelements, as logic of absolutely infinite order, order On, over
 > the set of urelements?

This was a fad for a while in the late 1960's.  I remember a paper by
Barwise, Gandy and Moschovakis on admissible infinitary logics with an
arbitrary structure embedded as a set of urelements.  It was one of
those fads that came and went.  It was sterile.

By the way, I have been accused of being hostile to urelements, but
actually I have no objection at all to set theory with urelements.  In
fact, I always introduce set theory to students in this way, because I
think it puts set theory in the best possible light.  See my lecture
notes at <http://www.math.psu.edu/simpson/courses/math558/>.

However, my considered opinion based on experience is that it's not
very useful or fruitful to try to view the universe of set theory
(with or without urelements) as a `logic'.  Experience of modern
f.o.m. research has shown that this approach is in the last analysis
sterile.  Much more progress has and will be made by considering
first-order logic.

 > Simpson is muddled here. 

I don't think I'm muddled.  

 > ZFC does not provide the foundation for mathematics. *Set theory*
 > provides the foundation for mathematics, and ZFC is a first order
 > formalisation of set theory.

Yes, your distinction between set theory and its first-order
formalizations may be valid at some level, at least for realists or
Platonists.  However, the fruitful approach that has yielded a lot of
serious insight (G"odel, Cohen, ...) is to study the first-order
formalizations.  Experience has shown that alternative approaches via
second-order logic are ultimately sterile, because they are
disconnected from inference.

You seem to be overlooking this hard-won lesson or insight that has
been gained from modern f.o.m. research.

 > What makes the formal theory ZFC so important for foundations is
 > the fact that any proof in ordinary mathematics has a formal
 > counterpart in ZFC.

This statement of the importance of ZFC is inadequate.  There's more
to it than that, especially from the Platonist or realist viewpoint.
Not only can ZFC formalize all mathematical proofs, but in addition,
ZFC is the strongest axiomatic theory that we can write down in the
language {epsilon,=} that is directly based on certain informal
insights or naive intuitions about the universe of set theory
(informal replacement, informal axiom of choice, etc).  Thus ZFC is
unique in an appropriate, relevant sense.  This should be viewed as
another aspect of why ZFC is so important for f.o.m.

 > The categoricity theorems for Peano systems (models of second order
 > PA) and complete ordered fields are ... an essential ingredient in
 > the argument to establish that the foundations of ordinary
 > mathematics lie in the theory of sets.

No, these categoricity results for second-order logic are not an
essential ingredient in that argument.  They can be replaced by the
observation that the isomorphism types of the structures in question
are straightforwardly definable in set theory.  This observation is
easily proved, with no reference to second-order logic.  Thus, in this
context as elsewhere, second-order logic is useless.

 > the old fashioned formalism that Simpson seems to be advocating ...

Why do you categorize my position as old-fashioned?  I'm using a lot
of modern f.o.m. research to make my points.

And why do you classify my position as formalism?  I don't see myself
as advocating formalism over any other foundational position, at least
not in this discussion.

I see myself as simply making some common-sense observations based on
experience and understanding of modern f.o.m. research.

I can summarize my observations as follows: Experience in modern
f.o.m. research has shown that first-order logic is fruitful and
second-order logic is sterile.

-- Steve