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]
This is another of the chapters I like best. Two small things:
p 91, 1st par after Theorem 45: “unless it stops ω-consistent” should be “unless it stops being ω-consistent”.
p 91, next par: the comma before “being ω-consistent is another syntactic property” should be a semicolon.
Thanks for this!