FOM: second-order logic is a myth

[Pat Hayes]

On re-reading Simpson's messages, I think that there has been some mutual
confusion on purely terminological matters. There are several distinct
things to consider. (1) a formal second-order language, ie predicate logic
with quantification over relation names and a typed version of Church's
lambda-operator. (2) a formal logic, which is this language plus suitable
rules of inference including abstraction and application of
lambda-expressions denoting relations, sufficient to conclude the existence
of a relation expressed by any appropriate wellformed expression in the
language. (3) the set of all classical interpretations of this language, ie
those in which quantification over properties ranges over the power set of
the domain of the interpretation. And finally (4) the set of Henkin
interpretations, in which the range of second-order quantification may be
any subset of the power set sufficiently large to guarantee that every
lambda-term has a denotation. Henkin interpretations include classical
ones, so a conclusion is classically valid if it is Henkin valid. The logic
is complete w.r.t Henkin interpretations but not w.r.t. classical
interpretations. So far nothing should be at all controversial.

Simpson uses 'second-order logic' to refer to the notion of classical
validity (3) applied to the language (1), and since there is no system of
rules which captures this properly, concludes that the term 'second-order
logic' is meaningless. Others, including myself, have long been in the
habit of referring to (2) as 'second-order logic', and distinguishing two
different semantics for this logic (3 and 4). However, this is just a
matter of terminology, of no real importance as long as we can all learn to
understand each other; nobody disagrees on the mathematical facts.

For many years I have also argued that second-order logic with the Henkin
semantics is 'really' first-order, but I've come to think that this is
really rather misleading, even though it has a germ of truth in it.
Certainly that logic with the Henkin semantics is translateable into
first-order, so that everything that can be said in it can be said in a
purely first-order theory, in a purely semantic sense: one might say that
there is a first-order account of Henkin validity. But 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.

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