FOM: second-order logic is a myth

[Martin Davis]

At 04:16 PM 2/22/99 -0500, simpson at math.psu.edu wrote:

>
>Among f.o.m. researchers, it's widely recognized that `second-order
>logic' (involving quantification over arbitrary subsets of or
>predicates on the domain of individuals) is not really a well-defined
>logic, because it involves many hidden assumptions. 

I'm delighted by this comment. Some history: In 1949 Leon Henkin in his
dissertation gave his now famous proof of the completenss theorem using
"Henkin constants". After showing how to apply compactness to algebra, he
went on to give a completeness proof for logic of order \omega. This was
completeness relative a to a particlar set of structures, because of course,
relative to the intended interpretation, it is incomplete. Church in his
textbook gave Henkin's treatment for second order logic.

In those years, people were still hung up over rules of substitution for
predicate variables, and in particular Church (in his book) formulated
second order logic (following Hilbert-Ackermann) using a very complicated
rule of substitution (people were always getting it wrong). Henkin published
a paper "Banishing the Rule of Substitution" in which he pointed out that
substitution could be replaced by the comprehension scheme. Aha! 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.

I never wrote this up, but I did give an invited ASL address on the matter.
Kreisel, who was there, told me that I had "trivialized" an important
subject. Be that as it may, 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.

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".

Martin