Supplement: The Diagonalization Lemma

The proof of the Diagonalization Lemma centers on the operation of substitution (of a numeral for a variable in a formula): If a formula with one free variable, A(x), and a number n are given, the operation of constructing the formula where the numeral for n has been substituted for the (free occurrences of the) variable x, that is, A(n), is purely mechanical. So is the analogous arithmetical operation which produces, given the Gödel number of a formula (with one free variable) ^⌈A(x)^⌉ and of a number n, the Gödel number of the formula in which the numeral n has been substituted for the variable in the original formula, that is, ^⌈A(n)^⌉. The latter operation can be expressed in the language of arithmetic. Note, in particular, that nothing prevents n from being the Gödel number of A(x) itself, that is, ^⌈A(x)^⌉ (in the usual coding schemes, though, n cannot be ^⌈A(n)^⌉). This operation of substitution is applied here again and again.

Let us refer to the arithmetized substitution function as substn(^⌈A(x)^⌉, n) = ^⌈A(n)^⌉, and let S(x, y, z) be a formula which strongly represents this operation, as a relation, in the language of our theory F. In other words, S is true of x, y, and z, if and only if:

• x = ^⌈A(x)^⌉, y = n, and z = ^⌈A(n)^⌉.

Again, nothing prevents us from considering substn(^⌈A(x)^⌉, ^⌈A(x)^⌉), or, analogously, S(x, x, y).

Given any formula A(x), we can now construct another formula ∃y[A(y) ∧ S(x, x, y)] with one free variable x. Let us abbreviate it as B(x).

This formula has a Gödel number, say, k = ^⌈B(x)^⌉. By substituting the numeral k denoting it for x in B(x), we get B(k); let us call this sentence D. Looking back the chain definitions, we see that:

• D := B(k) := ∃y[A(y) ∧ S(k, k, y)].

If m = ^⌈B(k)^⌉, then substn(k, k) = m, and (assuming F contains a sufficient amount of arithmetic; F can then also prove that the result of the arithmetized substitution function is unique)

• F ⊢ ∀y[S(k,k, y) ↔ y = m]

As k was the Gödel number of the formula B(x) and m is the Gödel number of the sentence which results when k is substituted for x in B(x), i.e., m = ^⌈B(k)^⌉, we can write this as:

• F ⊢ ∀y[S(k,k, y) ↔ y = ^⌈B(k)^⌉]

By a little logic, we have

• F ⊢ D ↔ ∃y[A(y) ∧ y = ^⌈B(k)^⌉], and from this
• F ⊢ D ↔ A(^⌈B(k)^⌉), i.e.,
• F ⊢ D ↔ A(^⌈D^⌉).

This completes the proof.

For the relations of the Gödelian Diagonalization Lemma to Cantor's method of diagonalization in set theory, see Gaifman 2006.