[FOM] The Derivability Conditions, Again

[Richard Heck]

Thanks to everyone who replied to my post about the derivability
conditions, and the argument for G2 given in that note. As I
expected, the argument is folklore. What I hadn't expected, and
was pointed out by Albert Visser, is that the argument can easily
be generalized to one for Löb's Theorem. Analyzing that situation
a bit more, what seems to me to be a moderately interesting point
emerges.

Visser's observation was that we can think of ~P(G) as instead
written as:

     P(G) --> F

(where F is some logical falsehood), and then generalize the argument
I gave so that F is replaced by some arbitrary sentence B. Most of that
argument then goes through unchanged. Depending upon how you finish
the argument, you then get either a proof of G2 or a proof of Löb's
Theorem.

To spell out the details, we start by diagonalizing on P(x) --> B to get a
formula G such that:

(0) T |- G <--> (P(G) --> B)

In particular:

(1) T |- G --> (P(G) --> B)

So we have, by (D1):

T |- P(G --> (P(G) --> B))

and so, by (D2):

(2) T |- P(G) --> P(P(G) --> B)

But, by (D3):

(3) T |- P(G) --> P(P(G))

Now certainly

     T |- P(G) --> [(P(G) --> B)  --> B]

so, by (D1) and two applications of (D2):

     T |- P(P(G)) --> [P(P(G)--> B) --> P(B)]

So by (2) and (3), we have

(4) T |- P(G) --> P(B)

Nothing so far has depended upon any assumptions about B. We get
(4) no matter what B is. (Of course, what G is depends upon what B is.
But there is such a G, given by (0) above, for each choice of B.)

We can now proceed in two different ways. One gets us Löb's Theorem,
and one gets us G2, and the routes are somewhat different.

For Löb's Theorem, suppose that:

     T |- P(B) --> B

Then by (4):

(5) T |- P(G) --> B

But then by (0):

     T |- G

and by (D1):

     T |- P(G)

and so by (5):

     T |- B

Now, of course, we can get G2 by following that path and then taking B
to be F, in which case, if:

     T |- ~P(F)

then also:

     T |- P(F) --> F

and so:

    T |- F

That's the usual derivation of G2 from Löb. But there's a different route
we can take.

Go back to (4), and take B to be F:

(4') T |- P(G) --> P(F)

By logic:

     T |- ~P(F) --> (P(G) --> F)

So by (0):

     T |- ~P(F) --> G

That is:

     T |- Con(T) --> G

But we know from G1 that T does not prove G, so T does not prove
Con(T).

What this makes clear to me is not just that G2 and Löb's Theorem are
closely related---we all knew that---and not just that Löb's Theorem is
a kind of generalization of G2---we knew that, too---but that the proof
of Löb's Theorem is a natural generalization of what looks to me like the
most direct proof of G2 from the derivability conditions. That may well
have been known to the experts, but it is news to me and perhaps to others
as well, and it will change how I present these two classic results: Give
this proof of G2, and then show how it can be generalized to give us Löb's
Theorem.

Richard Heck