FOM: second-order logic is a myth

[Stephen G Simpson]

Pat Hayes 17 Mar 1999 12:12:57 writes:

 > Had you posted my full message, everyone would have seen the
 > explanation, ...

As FOM moderator, I am under the impression that all your messages to
FOM have been posted in full to the entire FOM list, so everybody has
already had an opportunity to read them.  If some message or part of a
message from you is not in the FOM archives at
<http://www.math.psu.edu/simpson/fom/>, please let me know.

When we reply to a message on FOM, it's considered bad form to quote
the entire message.  It's better to quote only enough to briefly
indicate the context of the reply.  FOM readers are expected to refer
to previous postings as necessary.

Turning now to the substance of your 17 Mar 1999 12:12:57 posting, I'm
finding it difficult to sort out and understand the many points that
you seem to be trying to make.  Could you please try to express
yourself more clearly?

 > > Now I'm really confused.  Do you accept Shapiro's distinction
 > > between standard semantics and Henkin semantics, or don't you?
 > 
 > Of course I accept the distinction between the
 > *semantics*. However, this very word makes my point: they are both
 > semantic theories for the same *logic*, if by "logic" one means a
 > syntax and a formal specification of inferences (by means of rules
 > of inference, tableau, sequents or whatever.)

No, this is not correct.  The syntax is the same, but an inference
(i.e., something of the form A => B where A and B are formulas) can be
valid in the standard semantics without being valid in the Henkin
semantics.  It appears that you are somehow conflating standard with
Henkin.  Perhaps the confusion proceeds from Shapiro's ambiguities on
this point.  Or, perhaps the confusion proceeds from misleading
semantical terminology used by Shapiro.  My excuse for this is that
I'm following Shapiro's book, even though I don't agree with it, so
that we can have some common basis for discussion.

Let me try to clear this up.

We can all agree on what the second-order formulas are.  They are
built up inductively from atomic formulas using propositional
connectives &,v,~,->,<-> and individual quantifiers (x),(Ex) and
relation quantifiers (R),(ER).

One can also write down intuitively motivated axioms for second-order
logic, e.g., a comprehension scheme, which is the universal closure of

    (ER)(x1)...(xn)(Rx1...xn <-> F)

where F is any formula which does not contain R.  Other possible
axioms that can be written down are various formalizations of the
axiom of choice, a well ordering principle, etc.  One can also write
down explicit rules of inference.  Let S be the system of axioms and
rules that we write down.  S is recursive, and the set of formulas
that can be deduced via S is an r.e. set.  We can refer to S as
second-order logic.

Now, what about semantics?  There are two: `standard' and `Henkin'.
Both are based on the well known Tarski semantics for predicate
calculus.

If you act like a Platonist and insist that the relation quantifiers
range over *all* relations on the domain of individuals, you obtain
what is called the standard semantics.  This gives notions of logical
validity, logical consequence, etc., all with respect to the standard
semantics.  Note that the axioms and rules of S play no role here.
The standard semantics is what it is, regardless of which axioms and
rules we write down.

The other approach is to transform second-order formulas in an obvious
way into many-sorted, first-order formulas.  Then S becomes a system
of many-sorted, first-order logic.  The Henkin semantics is obtained
by considering many-sorted models in which the axioms and rules of S
are valid.  The Henkin semantics is then sound and complete for S.
This is a special case of the completeness theorem for first-order
logic.  The notions of logical validity, logical consequence, etc.,
are defined accordingly, all with respect to S or, equivalently, with
respect to the Henkin semantics.  

(I am blurring some fine distinctions here, but this is the basic
idea.  Details are in Shapiro's book.)

To summarize, there are (1) the standard semantics -- no axioms and
rules, only semantics -- and (2) the Henkin semantics, which are sound
and complete for the axioms and rules of S.  When I say `second-order
logic with the Henkin semantics', I refer to this many-sorted
first-order logical system based on S or an equivalent system.  This
terminology may be somewhat confusing, but I am following Shapiro.
Maybe you don't like this terminology, but let's try to follow it.

My basic position is that (1) is inadequate as a system of logic,
because the axioms and rules of inference are not specified.  On the
other hand, (2) is a perfectly good system based on many-sorted,
first-order logic.

This is what I mean by saying that `second-order logic' is a myth.

Now, perhaps you could try to restate your points in these terms.

-- Steve