Re: SUO: Re: Peirce's MS 514
> Yes, sorry, Goedel (1930) proved the completeness of FOL for
> his PhD dissertation, and the next year he proved ...
> incompleteness ...
The first two of three feats, any one of which would have placed
Goedel in the logical pantheon. (The third was his development of the
"constructible universe" in set theory and his use of it to prove the
consistency of the generalized continuum hypothesis. Some would argue
that his work on the interpretation of intuitionistic logic
constitutes a fourth such feat.)
> But then perhaps I should have mentioned that Leon Henkin (1950)
> proved the completeness of higher-order logic if you allow
> nonstandard models. But that is another story.
I have niggled, John, now I shall quibble:
<quibble>
I think it's best to reserve the the term "higher-order logic" to mean
the study of higher-order languages WITH a genuinely higher-order
semantics. Thus, I would say that Henkin proved the completeness, not
of higher-order logic, but of a certain proof procedure for
higher-order *languages* relative to the class of so-called "general"
models for those languages. As you note, they are "nonstandard" in
the sense that they are not in general truly higher-order. In fact,
it is easy to show that this higher-order system is really just a
first-order theory in disguise.
</quibble>
Best,
-chris
--
Christopher Menzel # web: philebus.tamu.edu/~cmenzel
Philosophy, Texas A&M University # net: chris.menzel@tamu.edu
College Station, TX 77843-4237 # vox: (979) 845-8764