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 numeral n are given, the operation of constructing the formula where the numeral 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 numeral ^⌈n^⌉, the Gödel number of the formula in which the numeral 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 subst(^⌈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 subst(^⌈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 subst(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.