[FOM] Kreisel, Löb, and G2
Aatu.Koskensilta at uta.fi
Mon Apr 2 08:41:39 EDT 2012
Quoting John Kadvany <jkadvany at sbcglobal.net>:
> In George Boolos, The Unprovability of Consistency (p.11), Boolos cites p.155
> of Kreisel's 'Mathematical Logic', published in T. L. Saaty, ed. Lectures on
> Modern Mathematics vol. III (1965) as the source for this direction of the
> equivalence. For the converse (i.e. Second Incompleteness implies Lob's
> Theorem) Boolos cites a conversation with Kripke, who Boolos says
> was 'perhaps the first' to make the observation.
I'd always associated the derivation of Löb's theorem from the
second incompleteness theorem with Kreisel, and apparently I'm not
alone, since Torkel Franzén says, on p. 177 of _Inexhaustibility_,
before giving Löb's original proof, that "Kreisel found a simple
argument using the second incompleteness theorem". Smorynski, however,
agrees with Boolos on this, writing
There are some mini-developments related to Löb's theorem that
may merit consideration. Foremost among these is a "new" proof of
Löb's theorem which first become well known in the latter half
of the 1970's but which had been known for several years by a
number of people. The earliest discovery of it that I know of was
by Saul Kripke who hit upon it in 1967 and showed it to a number
of people at the UCLA Set Theory Meeting that year.
in /The Development of Self-Reference: Löb's Theorem/ (_Perspectives
on the History of Mathematical Logic_ p. 130).
As for the observation that the second incompleteness theorem
follows from Löb's theorem by considering the sentence Prov("0=1") -->
0 = 1, i.e. ~Prov("0=1"), according to G.F. Kent's JSL review of Löb's
paper, Kreisel and Levy make it in /Reflection principles and their
use for establishing complexity of axiomatic systems/. From a modern
perspective, it's a triviality, but perhaps this was not so clear
before the development of provability logic.
Aatu Koskensilta (aatu.koskensilta at uta.fi)
"Wovon man nicht sprechen kann, darüber muss man schweigen"
- Ludwig Wittgenstein, Tractatus Logico-Philosophicus
More information about the FOM