FOM: second-order logic is a myth

[Martin Davis]

At 07:06 PM 2/24/99 -0500, simpson at math.psu.edu wrote:

>Dubucs:
> > I can't consider mathematical pieces as Henkin's famous 1950 paper
> > "Completeness in the theory of types" (JSL, XV-1950, 81-91) as
> > contributions to mythology.
>
>I don't understand the thrust of this remark.  Henkin's 1950 paper
>supports my (standard) view of the matter, not the continental or
>pro-second-order view.  The underlying point of Henkin's paper is that
>higher-order logic is best viewed in terms of plain, old,
>garden-variety, first-order, predicate calculus.  When this is done,
>the Henkin completeness theorem for higher-order logic immediately
>falls out, as a corollary of the G"odel/Henkin completeness theorem
>for predicate calculus.  Martin Davis explained this in 22 Feb 1999
>14:36:21.
>
To clarify: this SHOULD HAVE BEEN THE POINT of Henkin's 1950 paper, but it
wasn't. He gave a rather long detailed separate argument.

The lack of understanding of these simple matters generated a great deal of
misunderstanding, especially in computer science. Alan Robinson (famed for
the "resolution" principle as a basis for automated deduction systems) wrote
a confused paper some years ago, based on Henkin's notion of higher order
validity.

Martin