# FOM: second-order logic is a myth

Stephen G Simpson simpson at math.psu.edu
Mon Feb 22 21:27:17 EST 1999

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

```