FOM: second-order logic is a myth

[Stephen G Simpson]

John Mayberry 24 Mar 1999 17:13:28 writes:

 > I say that the very formal axioms and rules that are complete for
 > Henkin semantics are sound for standard semantics. "Not so." says
 > Simpson "It depend on the meta-theory." Now what possible meaning
 > could we attach to Simpson's words ... ?

You could attach the following meaning: 

  "The question of whether the axioms and rules of second-order logic
  are sound for the standard semantics has different answers,
  depending on the metatheory."

That is the meaning I had in mind.

For example, one of the axioms in Shapiro's book on second-order logic
is

  (R)(ES)[(x)(y)(Sxy -> Rxy) & (x)(y)(Rxy -> (Ez)Sxz)

          & (x)(y)(z)((Sxy & Sxz) -> y = z)]

where R and S are binary relation variables and x,y,z are individual
variables.  

Question: Is this axiom sound for the standard semantics?  Answer: Yes
if and only if the axiom of choice holds in `the real world'.  In
other words, the answer depends on `the real world'.  What is `the
real world'?  The universe of the metatheory, of course.  In other
words, the answer depends on the metatheory.

Why does this formulation irritate Mayberry so much?

Instead of

  "it depends on the metatheory"

I could have said

  "it depends on which real world we are living in."

However, if 

  "it depends on the metatheory"

is enough to severely irritate Mayberry, then what would 

  "it depends on the real world" 

have done to him?  I could be wrong, but I imagine that the latter
formulation would have been much more irritating.

Another formulation might be

  "we don't know whether this axiom is sound"

but this one is much less informative than the others.

 > Is it that the meaning of "standard 2nd order semantics" varies
 > from model to model of 1st order ZF?

That's correct, and it's another way of making my point.

 > Or is it that what we can formally prove about standard second
 > order semantics depends upon which consistent extension of 1st
 > order ZF we choose as our meta-theory.

That's also correct, and that's yet another way of making my point.

 > [ psychoanalysis of Simpson omitted ]

Let me try to put the point in a broader, more philosophical, more
speculative way.  This will probably irritate Mayberry even more!

The entire concept of `*the* standard semantics' or `absolute standard
semantics' for second-order logic seems to make sense only if you are
a set-theoretic realist or Platonist.  In other words, `absolute
standard semantics' assumes that infinite sets exist, the powerset
operation applied to infinite sets is real and meaningful, the
continuum hypothesis has a definite truth value, etc etc.  These
assumptions have to be part of the metatheory.

Thus it seems that, in order to accept `second-order logic with
standard semantics', you must first take a strong stand on many
questions in the philosophy of mathematics that are prima facie
important.  Thus your logic is not neutral with respect to such
questions.  Instead, your logic carries a lot of realist/Platonist
baggage.  Thus the scope and nature of logic have been severely and
sadly diminished.  Logic is no longer a common meeting ground that all
parties can agree on.  Instead it has become the exclusive instrument
of a particular philosophical faction.

This is another reason why `second-order logic with standard
semantics' is an inappropriate vehicle for philosophical and
foundational studies.

Mayberry says

 > ... being a formalist ... [is] going to prevent you from giving a
 > coherent account of the foundations of mathematics.

It seems that Mayberry has judged the formalist doctrine to be fatally
incoherent.  Why?  Can Mayberry give reasons, beyond the fact that the
Platonist/realist doctrine is apparently already built into his
logical framework?

I am neither a formalist nor a realist/Platonist.  I only want all
sides to get a fair hearing.

-- Steve