[FOM] The Derivability Conditions

[Craig Smorynski]

1. The Grundlagen is slowly being translated into English for College Publications. So far only Part A of volume I has appeared. The proof of G2 doesn't come until volume II, so you will have to wait!

2. The proof you give is indeed well-known. I have no idea where it originates. I probably learned it from Kreisel.

On Sep 29, 2012, at 12:37 PM, Richard Heck wrote:

> 
> 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

Craig



-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20120930/95718043/attachment.html>