[FOM] The Derivability Conditions

[Richard Heck]

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/