FOM: second-order logic is a myth

[Pat Hayes]

Steve Simpson writes:

>.... 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?

An attempt to clarify crossed with your message, so it may help. I learned
of Henkin's work from Henkin, however, rather than Shapiro (which I have
not read); and this may be the basis of our confusion. I gather from your
message that Shapiro *defines* the Henkin semantics by first translating
second-order language into a typed first-order language. While this
approach is in many ways elegant and semantically insightful, I think it
rather begs the question. Henkin himself did not do this, but rather gave a
semantics for the syntax of second-order logic as it was, with second-order
inference rules. As my previous message tried to emphasise, this gives a
different proof theory from the first-order translation (with which I am
familiar, though not from Shapiro.) So there are two distinct logics here:
second-order syntax with the Henkin semantics, and a first-order theory
expressed in predicate calculus. They are closely related, but not
identical.

> > > 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.

Read what I wrote more carefully, especially the part following "if by
"logic" one means...". Yes, there are formulas which are valid in the
standard semantics but not in the Henkin semantics. But the *language* and
*rules* of second-order logic are valid in both, and complete with respect
to the latter: and it is the *same* language and set of inference rules
(not valid implications) which (following Henkin) I am speaking of here, no
matter which semantics is thought to be appropriate for it. (Later in your
message you seem to be talking about a different logic, however.)
...
>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).

Ah, this may be real source of the misunderstanding. Unlike the first-order
case, there are syntactically distinct ways to define formulae in second
(or higher-) order logic, and they have rather different proof theories. I
was referring to Church's notation, in which the formula recursion also
includes a lambda variable-binder which forms relational terms. This is
what I mean by second-order logic, as did Church and Henkin. It has an
elegant natural-deduction style formulation. Lambda abstraction (the lambda
introduction rule) then plays the role of the comprehension scheme, but it
is an inference rule rather than a scheme, and does not straighforwardly
submit to translation into a first-order schema. The Henkin semantics fits
very naturally onto this proof-theoretic framework: indeed, it can be seen
as being generated by a extension of Herbrand's theorem to these proof
structures.
...
>One can also write down intuitively motivated axioms for second-order
>logic, e.g., a comprehension scheme, ...
...
>.  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.

Well, there are several second-order logics, it seems. However, I note that
you here use 'second-order logic' to refer to a system of formulae and
inference rules, so my earlier point about wanting to have it both ways
still stands.

>Now, what about semantics?  There are two: `standard' and `Henkin'.
....
>.... 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.

Yes, but care is needed. One does need to specify the language, ie the set
of formulas. It doesnt make sense to talk of a semantics unless one first
says what language it is a semantics of. This 'standard semantics' applies
to a second-order language, not a first-order one; but when we turn to
Henkin, you change your rules:

>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. .... (2)

No, S is what it was: it doesn't "become" anything. That's a different
language. It is first-order, while S is second-order. Its semantics is not
a semantics for the S (the one that you called 'second-order logic'.) There
is a way to map the semantics back, as it were, in an 'obvious way', but
there are nevertheless two distinct languages here: one second-order, the
other first-order.

There is a third approach, which is historically accurate and seems to me
to be more natural, which is (3) to eschew any 'transforming', leave the
language and rules of second-order logic unchanged, and give a different
reading to 'forall' when applied to relations (where it means something
like "all relations that could possibly be referred to by an expression of
the language currently being used." One might call this a Tractatus view of
what 'forall' means.) This is what Henkin did: he did not rewrite
second-order logic into a first-order theory, but gave a nonstandard
semantics for a (natural deduction-style) second-order logic with
lambda-conversion.
....
>
>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.

And (3) is also a perfectly good, non-mythical, system, but based on
second-order logic; which, it seems to me, is a reasonable basis for having
a valid claim to be called "second-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.

Well, no, because in *these* terms, second-order logic would indeed be a
myth. You and Shapiro have simply redefined it in such a way that it no
longer seems to exist. That is rather like what Stalin tried to do to
Trotsky.

Best wishes

Pat Hayes

---------------------------------------------------------------------
IHMC, University of West Florida		(850)434 8903   home
11000 University Parkway			(850)474 2091   office
Pensacola,  FL 32514			(850)474 3023   fax
phayes at ai.uwf.edu
http://www.coginst.uwf.edu/~phayes