[FOM] Kreisel, Löb, and G2

[Aatu Koskensilta]

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