[FOM] The Derivability Conditions, Again

[Harry Deutsch]

Isn't your proof of G2 in your first post on this subject pretty much the same as the provability logical proof Boolos gives at the end of "Goedel's Second Incompleteness Theorem Explained in Words of One Syllable"...? Harry
On Sep 30, 2012, at 4:27 PM, Richard Heck wrote:

> 
> 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
> 
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom