Having thought a bit more about Kripke’s short note on diagonalization, linked in the last post, it seems to me that the situation is this, in rough headline terms.
How do we get from a Diagonalization Lemma to the incompleteness theorem? The usual route takes two steps
(1) The Lemma tells us that for the right kind of theory T, there is a fixed point G in T for the negation of T‘s provability predicate.
(2) We then invoke Theorem X: if G is a fixed point for the negation of the provability predicate Prov for T, then (i) if T is consistent, it can’t prove G, and (ii) if T is omega-consistent, it can’t prove not-G.
The usual proof for the Diagonalization Lemma invoked in (1) is, as Kripke says, (not hard but) a little bit indirect and tricksy. So Kripke offers us a variant Lemma which has the form: for the right kind of the theory T, there is a fixed point in TK for any T-predicate where TK is T augmented with lots of constants and axioms involving them. The axioms are chosen to make the variant Lemma trivial. But now the application of Theorem X becomes more delicate. We get a fixed point for the negation of TK‘s provability predicate and apply Theorem X to get an incompleteness in TK. And we then have to bring that back to T by massaging away the constants. Not difficult, of course, but equally not very ‘direct’.
So you either go old-school, prove the original Diagonalization Lemma for T in its tricksy way, and directly apply Theorem X. Or you go for Kripke’s variant which more directly uses wffs which are ‘about’ themselves, but have to indirectly use Theorem X, going via TK, to get incompletness for the theory T we start off from. You pays your money and you takes your choice.
For a worked out version of these headline remarks see the last section of the revised draft Diagonalization Lemma chapter for Gödel Without Tears. Have I got this right?
The Hilbert paper is now available here:
https://arxiv.org/pdf/2102.08346.pdf
I printed this for Saul and will get back to you if he has something to say.
A bit about the background of this note. Alfred Visser wrote to us asking for Saul’s direct approach and Saul wrote the paper as a reply. Sometimes thinks work out nicely.
Sorry Logical Troubles is taking so long. He is now working on “The Collapse of Hilbert’s Program” and needs to finish “A Model Theoretic Approach to Godel’s Theorem”. The latter is probably one of the most important papers in the collection because it is an application of his notion of fulfillability, which is not well-known. In case you haven’t seen it, here is an old and very good thesis by Quinsey developing it:
https://arxiv.org/pdf/1904.10540.pdf
We think it should still be published. If you can suggest where to send it it would be great.
There’s a minor issue about the wording of Defn 53 on p 102.
Saying “adding all the new constants” works because we’ve already been told about the new constants. Wording such as “all the ___” seems to refer to something introduced earlier. So “together with all the new axioms” also seems (at least for a moment) to be about something that’s already been introduced, and it isn’t.
It might be better to say something like “together with new axioms (same formula as before), one for each constant.” Or perhaps without the “one for each constant”.
The nonstandard numbering approach keeps both parts neat though. You remain in the theory and avoid the tricksy diagonalization lemma. The new axioms approach makes the unprovable sentence ‘about’ some other theory and is thus not really good in my opinion.
Do many people find it enlightening or clarifying (or otherwise helpful) to be told that G or similar is a fixed point?
If so, is there an intuitive explanation of why it’s helpful that might help the rest of us to see it too?
Speaking for myself, I don’t think stretching the “fixed point” terminology to this case is *enlightening*. But I thought that I should at least mention it (in an intro for students) as it is so commonly used — and I suppose it is *helpful* in the banal sense of being occasionally useful shorthand. Are R.M. and I both missing something?
I do think that’s right. I would note that O3 is doing the heavy lifting, via the constant axioms, whose role is to insure (=make provable) that the new constants might as well be the standard numerals.
“Constant-free” means “Newconstant-free”?
Thanks! And yes I should make it absolutely clear that constant-free always mean c-constant (nee constant) free.