[FOM] First- Vs Second-Order Logic: Origins of the Distinction?

[Curtis Franks]

> [...]

After all, Godel's completeness theorem is frequently described as having
> shown that any sentence x that was entailed by a set of sentences S in FOL
> is derivable from them by the standard deductive rules, or equivalently
> that for any sentence x not so derivable, so that ~x was consistent with S,
> was false in some model of S so that it was not semantically entailed.
>
> Are you maintaining that prior to 1929 there was not a clear enough
> understanding of the concept "every model of S is also a model of x" that
> the question of whether that concept implied x was deducible from S was
> considered an actual open question? In other words, that Godel's paper on
> the completeness theorem decisively solved for FOL a problem that it also
> was the first to clearly formulate?
>
> If so, Godel  is even more impressive than I had realized.
>
> -- JS
>

Yes, this is just about right. Bill Tait mentions Hilbert's 1917--18
lectures in part because the question of semantic completeness seems to
have been clearly formulated there for the first time. But no one else was
posing the question, and Hilbert himself expressed serious misgivings about
the semantic notions involved. For example, in Hilbert and Ackermann 1928
(largely redacted from those lectures), after presenting Ackermann's
argument that the predicate calculus is incomplete in the sense of
"Post-completeness," one finds the remark that this argument makes the
underivability of the relevant formula "plausible" followed by a completely
semantics-free proof of the same result. And the tone throughout suggests
that Hilbert considers the "Post completeness" formulation the properly
scientific one so that while semantic methods were a convenient gimmick for
the investigation of propositional logic (because of the coincidence of
semantic completeness and Post-completeness), the separation of Post
completeness and semantic completeness in quantification theory left little
interest for him in the latter notion.

To see how prevalent this way of thinking was in those days, one can notice
that not only Hilbert but Poincare and many other great thinkers as well
(Frege and Brouwer being notable exceptions) customarily inferred without
argument or justification from the formal consistency of a set of axioms
(of any order) something like a model of things satisfying those axioms.
That's why Goedel began his thesis with some remarks about how this old way
of thinking gets in the way of seeing the problem of semantic completeness
clearly. And it is worth appreciating that this is another major part of
the story about the origins of the distinction between first and second
order logic: Goedel seems to have fastened on this suspicious inference,
noticed that at the very least it needs justification, that in fact it
cannot be justified in general (his incompleteness theorem), but that for a
special class of axioms the justification is available (his completeness
theorem).

It also seems that the now customary description of Goedel's completeness
theorem that Joe Shipman provides was unavailable even for Goedel. Nowhere
in his thesis or in the 1930 publication does he use a notion of semantic
consequence. According to John Dawson, it was not until 1951 (twenty years
after Godel's proof!), in Robinson's ``On the Metamathematics of Algebra,''
that anyone formulated the notion of "strong completeness," the
derivability from an arbitrary set of first-order formulas of all their
logical consequences. (And amazingly, Goodstein reviewed Robinson's book
and explicitly remarked that this whole portion of the book "could with
advantage have been omitted.")

Here is how I put the point in my essay in the Juliette Kennedy's
"Interpreting Goedel" volume: "Goedel’s work is revolutionary not because
of what questions he answered so much as because he managed, in answering
them, to demonstrate the value of a particular way of asking them."

Curtis
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20160531/0c66ea50/attachment-0001.html>