FOM: second-order logic is a myth

[Pat Hayes]

Steve Simpson writes:

> ...Logic existed long before set theory.
>Logic goes back to Aristotle; set theory goes back to Cantor.

Predicate calculus goes back to Frege, or maybe Peirce. (Choose your
historian to settle this issue; in any case, it started in the 19th
century, not with Aristotle.)

> > Without set theory you cannot motivate your systems of formal,
> > first order proof, because you can't formulate completeness in a
> > natural way, or establish it.
>
>.....  First-order logic (it's
>better to call it predicate calculus) can and should be motivated
>independently of set theory, as a general framework for reasoning
>about any subject whatsoever.  For instance, if you want to reason
>about cars and trucks, you lay down primitive predicates Cx (`x is a
>car') and Tx (`x is a truck') and maybe Vx (`x is a vehicle') and go
>from there.  If you want to also reason about sets of vehicles, you
>will probably also want an additional predicate Sx (`x is a set of
>vehicles') but you can go a long way without this.

Indeed you can. There is a flourishing industry devoted to using logics
(usually syntactically restricted subsets of 1PC) to formalise various
aspects of human thought in ways that are suitable for use by automatic
reasoners, much in the spirit of Carnap's 1954 textbook. These axioms
rarely need to mention sets explicitly. However, that isnt the point. Set
theory is used in the metalanguage of logic, to establish what 'truth'
means and prove completeness theorems.

Simpson's position seems to me to have a central difficulty. On the one
hand, he characterises a logic as a set of rules, ie a formal process for
moving from antecedents to conclusions, and claims that this
characterisation of what makes a logic into a logic is both historically
and intellectually prior to any analysis of the validity or completeness of
those rules. That is a coherent position to adopt, indeed. However, he also
emphasises repeatedly that when he says 'second-order logic' he means to
refer not to Henkin's logic but to full classical second-order logic. The
trouble is, that this distinction makes sense only if we understand 'logic'
to be defined semantically. The inference rules of Henkin's logic are
classically valid, and constitute a useful and powerful set of inference
rules for (classical) second-order logic. They happen to be incomplete, of
course, but that distinction must, by Simpson's own criteria, be a
secondary issue. (In fact to talk of Henkin's 'logic' is actually rather
misleading. What Henkin did was provide an alternative model theory for
second-order logic (ie, predicate calculus with quantified variables in
relation positions plus lambda-notation, with suitable inference rules for
abstraction and lambda-application) relative to which the inference rules
are complete. It's the same *logic*, though, in Simpson's sense.)

You can't have it both ways. If a logic is a way of drawing conclusions,
then 1PC is really a logic (actually several logics: natural deduction,
Gentzen tableaux, etc.) but so is Church's lambda-calculus, second-order
logic, modal logics and even, for that matter, such modern exotica as
nonmonotonic or linear logics. There are more logics than you can shake a
stick at. If, on the other hand, it is the fact of completeness relative to
a formal account of truth that makes a logic what it 'really' is, then 1PC
does seem to be more central than the others; but then I don't see how one
can re-do Tarski without mentioning sets.

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