[FOM] The Derivability Conditions

[sambin at math.unipd.it]

Very nice proof!  I agree, it sounds as "folklore", but I don't  
remember any place where it was actually made public (true, my memory  
is not so trustable now since those days are now very long ago...)

A quick look at Boolos' book (The logic of provability, pages 56-58)  
shows that his proof of G2 passes through Löb's theorem. Boolos' proof  
of Löb's theorem is not so much longer than your proof of G2.

Rautenberg's proof of G2 (A concise introduction to mathematical  
logic, page 280) avoids the use of Löb's theorem and uses instead  
uniqueness of some fixed points (lemma 3.1)

I agree with your excitement: your proof is a further improvement on  
the proof of G2, and perhaps I will use it in my course. However, I  
would need more explanations to be able to share your claim that "in  
no way involves the sort reasoning that is involved in the proof of  
[Löb's] theorem".

Giovanni Sambin

Quoting Richard Heck <richard_heck at brown.edu>:

>
> Hi, all,
>
> I've been teaching a course on Gödel's second and so have been  
> thinking a fair bit about the derivability conditions and their  
> history. As the story is usually told, Hilbert and Bernays isolated  
> four conditions in the /Grundlagen/ which they showed were  
> sufficient for G2, and then these conditions were simplified due to  
> work by Löb. The story is complicated, however, by the fact that Löb  
> does not actually prove G2 in his paper, though of course the proof  
> isn't very hard. (There was some discussion here a while ago that  
> suggested maybe Kreisel was the first to realize how to get G2 from  
> Löb's Theorem.)
>
> What I've been wondering about is how Löb's three conditions relate  
> to the derivation of G2 from the four conditions in Hilbert and  
> Bernays. Löb shows that his condition P(A) --> P(P(A)) follows from  
> the others that Hilbert and Bernays isolate, and it's clear that  
> it's weaker than their other conditions, too. So that makes me  
> wonder whether the argument that Hilbert and Bernays give for G2 can  
> be carried out just given Löb's three conditions. Unfortunately, I  
> do not have access to a copy of the /Grundlagen/, and I'm not sure  
> how much it would help if I did, since my German is not very good.  
> So if someone could answer that question, I'd be grateful.
>
> In any event, it occurred to me the other day that there is a direct  
> argument for G2 from Löb's three conditions that does /not/ go via  
> Löb's Theorem, and in no way involves the sort reasoning that is  
> involved in the proof of that theorem.
>
> Here's the argument. We assume that
>
> D1: T |- P(A), whenever T |- A
> D2: T |- P(A --> B) & P(A) --> P(B)
> D3: T |- P(A) --> P(P(A))
>
> Diagonalize on ¬P(x) to get a formula G such that
>
> T |- G <--> ¬P(G)
>
> In particular:
>
> (1) T |- G --> ¬P(G)
>
> So we have, by (D1):
>
> T |- P(G --> ¬P(G))
>
> and so, by (D2):
>
> (2) T |- P(G) --> P(¬P(G))
>
> But, by (D3):
>
> (3) T |- P(G) --> P(P(G))
>
> Now certainly
>
> T |- P(G) --> [¬P(G) --> ?x¬(x = x)]
>
> so, by (D1) and two applications of (D2):
>
> T |- P(P(G)) --> [P(¬P(G)) --> P(?x¬(x = x))]
>
> So by (2) and (3), we have
>
> T |- P(G) --> P(?x¬(x = x))
>
> so by contraposition and (1):
>
> T |- ¬P(¬?x(x = x)) --> G
>
> But, as usual, we know that T does not prove G.
>
> I don't claim any originality for this argument. I'm just curious if  
> there's a source for it, or if it would be characterized as  
> "folklore", or something of the sort. It's similar in spirit to the  
> argument Jeroslow gives in "Redundancies in the Hilbert-Bernays  
> Derivability Conditions", and might even be said to be a version of  
> that argument, but without the use of the "strong" diagonal lemma  
> that gives us a term t for which: t = *A(t)*.
>
> At the very least, I'm glad to know of this argument, for  
> pedagogical reasons, as it's a lot easier to explain Löb's Theorem,  
> and I can then introduce Löb's Theorem separately, and explore the  
> relations between the two results.
>
> Any thoughts welcome.
>
> Richard Heck
>
>
> -- 
> -----------------------
> Richard G Heck Jr
> Romeo Elton Professor of Natural Theology
> Brown University
>
> Check out my book Frege's Theorem:
>   http://tinyurl.com/fregestheorem
> Visit my website:
>   http://frege.brown.edu/heck/
>
>
> -- 
> -----------------------
> Richard G Heck Jr
> Romeo Elton Professor of Natural Theology
> Brown University
>
> Check out my book Frege's Theorem:
>   http://tinyurl.com/fregestheorem
> Visit my website:
>   http://frege.brown.edu/heck/
>
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom
>


----------------------------------------------------------------
This message was sent using IMP, the Internet Messaging Program.