FOM: second-order logic

[Stephen G Simpson]

Pat Hayes 18 Mar 1999 20:32:25 writes:

 > On re-reading Simpson's messages, I think that there has been some
 > mutual confusion on purely terminological matters. ...  of no real
 > importance as long as we can all learn to understand each other;
 > nobody disagrees on the mathematical facts.

Yes, I think that's right.  Although we need a clearer terminology,
most FOMers probably agree on the underlying mathematical facts.

However, I think you are underestimating the value attached by some
people (Shapiro? Holmes?) to `second-order logic with the standard
semantics'.  They insist on calling this a `logic', even though it is
not characterized by axioms and rules of inference.  They ascribe
stupendous importance to the useless, sterile fact that various
well-known mathematical structures such as the natural numbers, the
real numbers, plane geometry, etc., are categorical with respect to
this `logic'.

Be that as it may, putting the `standard semantics' aside, I'm
somewhat intrigued by your point that there are significant
distinctions arising from different syntactical possibilities.  Here
we are entirely within the realm of what I (following Shapiro) have
called `second-order logic with Henkin semantics'.  This kind of
second-order logic is properly called `logic'.

You seem to be saying that, within this Henkin realm, one can consider
on the one hand formalisms (syntax and axioms and rules of inference)
based on lambda abstraction, and on the other hand formalisms based on
quantifiers.  You seem to be saying that formalisms of these two kinds
can be in a sense equivalent, i.e., they may give the same sets of
theorems under an appropriate biinterpretation, yet the structure of
proofs in the two systems can be very different.  I would like to
follow up on that proof-theoretic aspect.

You say:

 > ... the two languages are really very different in the kinds of
 > inference they sanction and in their proof-theoretic and
 > computational properties. There is no unification algorithm for
 > second-order logic, for example, so proofs using that formal
 > language are very different in their fundamental structure from
 > first-order proofs; there is nothing in first-order logic that
 > directly corresponds to the rule of lambda-abstraction.

Could you please give some formal details here?  You had better start
from the beginning.  I'm probably not sufficiently familiar with the
lambda abstraction setup for second-order logic (though I'm quite
familiar with typed and untyped lambda calculus as presented for
instance in Barendregt's book).  I'm much more familiar with the setup
based on quantifiers and many-sorted first-order logic, which I
described in 17 Mar 1999 16:56:43.  I have read accounts by Church and
Henkin based on lambda abstraction, but like Martin Davis in 22 Feb
1999 14:36:21, I find the many-sorted first-order logic approach much
more illuminating and flexible.

-- Steve