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?