FOM: second-order logic is a myth

[Stephen G Simpson]

Martin Davis 22 Feb 1999 14:36:21 writes:
 > I instantly realized that Henkin completeness was an immediate
 > corollary of G"odel completeness and that Henkin models were just
 > arbitrary structures that satisfied comprehension and
 > extensionality.

Yes.  The so-called logic of order omega (sometimes called type
theory) is just a species of first-order logic, with omega sorts and
with full comprehension and extensionality.  This was the key to
understanding it.  It seems so trivial now, but ...

 > I believe that autonomous formalization of second (and higher)
 > order logic is important in the context of proving such things as
 > cut elimination theorems for Gentzen style rules. That is, for
 > certain topics in proof theory. But for other purposes the slogan
 > is: second order logic is just 1st order logic plus a weak set
 > theory.

Near the beginning of my book `Subsystems of Second Order Arithmetic'
<http://www.math.psu.edu/simpson/sosoa/>, I patiently explain that
second-order arithmetic and its subsystems are really two-sorted
first-order theories.  Even in a proof-theoretic context, it's clear
that so-called `higher-order logics' are much better thought of in
terms of many-sorted first-order logic.  In particular, the
G"odel/Henkin completeness theorem applies to them, continental
philosophers notwithstanding.  There seems to be rampant confusion on
this point ....

 > Final historical remark on the word "logicism": the separation of
 > 1st order logic did not emerge in the work of the logicists proper:
 > Frege and Russell.  It came out of Hilbert's program. Hence my
 > suggestion that the identification of basic logical reasoning with
 > 1st order logic be called "Hilbert's Thesis".

Fair enough.  My proposal to call it `the logicist thesis' was a
little off-base.  Let's call it `Hilbert's thesis', as originally
proposed by Martin Davis.  Martin, where is the article in which you
proposed it?  I was trying to remember where I read that ....

-- Steve