This short chapter, ‘Outlining a Gödelian Proof’ gives a first indication of the way that we are going to prove (the semantic version of) the first incompleteness theorem by constructing a Gödel sentence which is true if and only if unprovable. The detailed construction has to wait until a later chapter; but we do meet the key idea of the arithmetization of syntax.
p 14, very near the bottom: should ‘consist in’ be ‘consist of’?
p 15, sequence of digits: Given that the digits can be from an arbitrarily large base — every ASCII character could be treated as a ‘digit’, for example — and that you write at the top of p 15 that the choice of encoding scheme “will depend on considerations of ease of manipulation”, is there a reason why Godel’s own encoding using primes is easier to manipulate?
A digit-based scheme seems much more straightforward to me, and you write that its mapping “is the simplest of algorithms”.
Also, if we think of an algorithm being carried out by a computer, we’ll already be encoding using what’s effectively a digit-based scheme anyway. Why encode again into something that seems, if anything, harder to manipulate?
In IGT and GWT2f, you even have informal proofs that various things are primitive recursive that begin “Decode n” to get out of the Godel-style encoding before thinking about how to determine whether Term(n), for example, holds.
If there is a strong reason for using Godel-style encoding, it ought to be explained somewhere in GWT. It the main reason only that it’s traditional?
p 16, Defn 15: It feels like there’s something that would include a verb missing after “Then, relative to that numbering scheme,”
p 16, statement of theorem 3:
— ‘T’ appears twice in ‘Suppose T is an effectively axiomatized formal theory T’
— ‘properties/relation’ should have ‘relation’ plural too.
p 16, proof for Theorem 3 for Prf (m, n): we’ve been told how a sequence of expressions could be encoded, but not how a proof array would be.
p 17, Defn 16: “where the quantifier is, if necessary, a restricted quantifier running just over numbers in the domain” — what is the domain in question? And if it’s the natural numbers (which is what I’d have thought), that restriction doesn’t seem very restrictive. For instance, the positive even numbers would be “numbers in the domain”, despite being unending.
p 19: good explanation, and one it’s useful to have at that point.
Thanks once more. About later using Gödel’s powers-of-primes numbering scheme, does it have any more than tradition to recommend it against possible competitors? I doubt it! Smullyan in his Gödel’s Incompleteness Theorems uses a thirteen-letter alphabet for his language for arithmetic, and uses concatenation of base-13 digits to represent strings of symbols. And yes, I agree that it should be said that it is little more than historical piety that recommends sticking with (a version of) Gödel’s original scheme — and I’ll be saying that in a later chapter.
On encoding sequences, yes that needs to be more explicit.
On restricted quantifiers I had in mind the case that we were allowing the case a language with a more inclusive domain: but again, should have been clearer.