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
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
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 ....
More information about the FOM