And, at last ….
Cue drumroll …
‘The First Incompleteness Theorem, syntactic version’
This is the version of the theorem that Gödel highlights in his epochal 1931 paper, and which people usually have in mind when they talk of ‘the’ incompleteness theorem. We have to do a little more work than for the semantic version, but again — once we have grasped the trick of constructing a Gödel sentence, and understood the idea of capturing/representing/defining primitive recursive relations in a formal theory, the proof is delightfully simple. Which is not to diminish Gödel’s achievement in the slightest: on the contrary, it was very important to him that the ideas involved are straightforward to handle once you grasp them.
[Link now removed]