Note: Full functionality of this website requires JavaScript to be enabled in your browser.

# The Diagonal Lemma

It is claimed that a statement that is commonly called the Diagonal Lemma, or the Diagonalization Lemma, proves the existence of self-referential sentences in formal systems of natural numbers, and that it can be used to prove incompleteness of certain formal systems. The Diagonal Lemma essentially states, that for any given formula of the formal system with one free variable, that formal system can prove a certain proposition regarding the Gödel numbering system.

The formulas of the formal system have no way of referring to the Gödel numbering function, since, by definition, it is a function that is defined in a meta-language to the formal system. So the idea that it is possible to prove that the formal system can prove a proposition regarding the Gödel numbering system is one that deserves careful scrutiny.

The following proofs of the Diagonal ‘Lemma’ are examined here:

- A proof given in the book,
*‘Computability and Logic’*, by George Boolos, John Burgess, and Richard Jeffrey - A proof given in the book,
*‘Introduction to Mathematical Logic’*, by Elliott Mendelson - A proof on the Wikipedia website
- A proof on the ProofWiki website
- A proof by Panu Raatikainen on the Stanford website
- A proof by Vann McGee of MIT

There is also a proof of the lemma in Peter Smith’s book, *‘An Introduction to Gödel’s Theorems’*. (Footnote:
Peter Smith. *An Introduction to Gödel’s Theorems*. Cambridge University Press, 2006.

ISBN: 9780521857840 See An Introduction to Gödel’s Theorems: Details.)
and also in Smith’s downloadable cut-down version of his book at Logic Matters: Gödel Without (Too Many) Tears. The error in Smith’s “proof” of the lemma is the same error that is dealt with in detail in the paper A Fundamental Flaw in an Incompleteness Proof by Peter Smith. As in the generic proof below, Smith’s error is to assume that certain functions/relations are primitive recursive number-theoretic functions/relations despite the fact that their actual definition defines them as not being primitive recursive number-theoretic functions/relations.

Please note:

- The rest of the content of this page requires a basic knowledge of symbolic logic.
- Some of the symbols used on this page may not display correctly on older browsers.

## The Generic Proof of the Diagonal ‘Lemma’

While the proofs mentioned above are all slightly different, the main core is the same, and they all rely on the same elementary error. Because the main core is the same in all the proofs, a generic proof can be written, and which contains the essence of the four proofs mentioned above. This generic proof of the Diagonal ‘Lemma’ is as follows:

(1)

Let *f*(*x*) be a function.

(2)

There is a relation δ(*x*, *y*) which is logically equivalent to the relation *y* = *f*(*x*), that is, that:

δ(*x*, *y*) ⇔ *y* = *f*(*x*)

(3)

There is a formula that expresses the relation δ in the system *T*, provided that the function *f*(*x*) satisfies certain conditions — usually the condition is that it be a primitive recursive number-theoretic function.

(4)

Now define a formula β(*x*) of the system *T* as:

(5)

β(*x*) ≡ ∀*y* [¬δ(*x*, *y*) ∨ ψ(*y*)]

where ψ(*y*) is any relation of the system *T* with one free variable. (Footnote:
Commonly this is given as β(*x*) ≡ ∀*y* [δ(*x*, *y*) ⇒ ψ(*y*)]. Logically they are equivalent. In natural language, this can be read as: *For all* *y*, *either* δ(*x*, *y*) *does not apply, or* ψ(*y*) *applies, or both.*
)

(6)

The formula β(*x*) is thus logically equivalent to:

∀*y* [ ¬(*y* = *f*(*x*)) ∨ ψ(*y*)]

(7)

Assume that the system *T* is complete and consistent, so that, for any given *n*, the system *T* must prove either β(*n*) or ¬β(*n*)

(8)

Take the first case; that the system *T* proves β(*n*)

(9)

That is, the system *T* proves the formula that expresses the relation ∀*y* [ ¬(*y* = *f*(*n*)) ∨ ψ(*y*)]

(10)

For the case where *y* = *f*(*n*), ¬((*f*(*n*) = *f*(*n*)) does not apply, so that it must be the case that ψ(*f*(*n*)) applies. So that if the system *T* proves the formula β(*n*), then it must also prove ψ(*f*(*n*)). (Footnote:
Strictly speaking, the formula of the system *T* that expresses the concept ψ(*f*(*n*)).
)

(11)

Now, take the second case; that the system *T* proves ¬β(*n*), which is logically equivalent to:

(12)

¬∀*y* [ ¬(*y* = *f*(*n*)) ∨ ψ(*y*)], and to:

(13)

∃*y* ¬[¬(*y* = *f*(*n*)) ∨ ψ(*y*)], and to:

(14)

∃*y* [*y* = *f*(*n*) ∧ ¬ψ(*y*)] (Footnote:
In natural language, this can be read as: *There exists a* *y* *such that* *y* = *f*(*n*) *and* ψ(*y*) *does not apply.*
)

(15)

Now, we know that there is only one value of *y* for which *y* = *f*(*n*), so that for there to be a *y* so that both *y* = *f*(*n*) * and* ¬ψ(

*y*) apply, it has to be this value of

*y*, and that means that ¬ψ(

*y*) applies for this value of

*y*, so that ¬ψ(

*f*(

*n*)) applies. So, if the system

*T*proves ¬β(

*n*), then it must be the case that the system

*T*proves ¬ψ(

*f*(

*n*)).

(16)

From the two cases above, the system *T* either proves β(*n*) and ψ(*f*(*n*)), or else it proves ¬β(*n*) and ¬ψ(*f*(*n*)). Since we are assuming the completeness of the system *T*, the system *T* must prove, for any *n*, either the equivalence of β(*n*) and ψ(*f*(*n*)) or its negation, that is, the system *T* must prove either β(*n*) ⇔ ψ(*f*(*n*)) or ¬[β(*n*) ⇔ ψ(*f*(*n*))]. And since we are assuming the consistency of the system *T*, then it must be the case that, for any natural number *n*, the system *T* proves β(*n*) ⇔ ψ(*f*(*n*)).

This result is a general result that is the underlying basis of all the proofs mentioned above. Given this result the rest of the proof proceeds as follows:

(17)

We now let the function *f*(*x*) be the function *GN*[β(*x*)], where *GN* is the Gödel numbering function, so that *GN*[β(*x*)] is the Gödel number of the formula β(*x*). We now have that the system *T* proves, for any natural number *n*:

(18)

β(*n*) ⇔ ψ(*GN*[β(*n*)])

(19)

Take the formula of the system *T* that expresses β(*n*), that is, the formula of the system *T* that expresses ∀*y* [¬δ(*n*, *y*) ∨ ψ(*y*)], and take the Gödel number of that formula, which is *GN*[β(*n*)]. We now produce a new formula of the system *T* by substituting the *n* in the formula β(*n*) by the Gödel number of the formula itself, that is, by *GN*[β(*n*)]. This gives that the system *T* proves:

(20)

β(*GN*[β(*n*)]) ⇔ ψ(*GN*[β(*GN*[β(*n*)])])

(21)

Giving the name φ to the formula of the system *T* that is β(*GN*[β(*n*)]), we now have the desired result:

(22)

φ ⇔ ψ(*GN*[φ])

The flaw in the proof is obvious. For there to be a formula in the system *T* that expresses the relation δ, the function *f* must satisfy certain conditions (as in step (3) above). But in the above, at step (17), the function *f*(*x*) is defined as the function *GN*[β(*x*)], and so is defined in terms of the Gödel numbering function. Because the Gödel numbering function is a function in the meta-language to the system *T*, there cannot be any such relation δ in the system *T* that contains the information of the definition of the Gödel numbering function and which can unambiguously reference formulas of its own formal system *T*. A full proof of this is given in the paper The Impossibility of Representation of a Gödel Numbering Function by a Formula of the Formal System.

Thus step (17) is a logical absurdity. This absurdity is disguised in the proofs mentioned above by their presentation, which serves to obscure the inherent absurdity.

## Boolos’ Proof of the Diagonal Lemma

This proof is found in the book, *‘Computability and Logic’*, by George Boolos, John Burgess, and Richard Jeffrey, (Footnote:
G Boolos, J Burgess, R Jeffrey. *Computability and Logic*. Cambridge University Press, 5th Edition, 2007.

ISBN‑13 978‑0511366680 Computability and Logic - Boolos: Details.)
and is given as a proof of the lemma 17.1 in the book.

The proof commences by asserting:

“There is a primitive recursive function, *diag*, such that if *a* is the Gödel number of an expression *A*, then *diag*(*a*) is the Gödel number of the diagonalization of *A*.”

The proof goes on to assert that since the function *diag* is a primitive recursive number-theoretic function, it can be represented in the system *T*.

However, Boolos has previously defined the diagonalization of *A* to be the expression ∃*x*(*x* = ^{⌈}*A*^{⌉} & *A*), where ^{⌈}*A*^{⌉} is defined as the Gödel number of *A*. In common with many other authors, he makes the elementary error of assuming that this relation, as it is defined, is a primitive recursive number-theoretic function. That cannot be the case, since it is defined in terms of the Gödel numbering function, which is a function in the meta-language to the system *T*, and is a not a function in the system *T*.

The result is that Boolos’ proof continues as:

Let Diag(*x*, *y*) be a formula representing *diag*, so that for any *m* and *n*, if *diag*(*m*) = *n*, then ├_{ T} ∀*y* (Diag(*m*, *n*) ⇔ *y* = *n*).

├_{ T} ∀*y* (Diag(*m*, *n*) ⇔ *y* = *f*(*m*)) as in the generic proof above,

where *f*(*m*) is any number-theoretic function, Boolos refers to the specific function *diag* to give:

├_{ T} ∀*y* (Diag(*m*, *n*) ⇔ *y* = *diag*(*m*)).

The rest of Boolos’ proof follows the general outline as given in the generic proof above, generating the inevitable result of:

├_{ T} *G* ⇔ *B*(^{⌈}*G*^{⌉})

a result which is completely dependent on the fallacy that the function *diag* can be at the same time a primitive recursive number-theoretic function and also be defined at the same time as the Gödel number of the diagonalization of *A*, that is, as ∃*x*(*x* = ^{⌈}*A*^{⌉} & *A*).

It will be seen that the main part of the proof has nothing whatsoever to do with proving self-reference, and that the self-reference in the proof is that brought about by the invalid introduction of the definition of *diag* as indicated above.

## Mendelson’s Proof of the Diagonal Lemma

This proof of the Diagonal Lemma is given in *‘Introduction to Mathematical Logic’* by Mendelson (Footnote:
E Mendelson. *Introduction to Mathematical Logic*. Chapman & Hall/CRC, 6th edition, 2015

ISBN 9781482237726 Introduction to Mathematical Logic - Mendelson: Details.)
in the section of Proposition 3.34 (Diagonalization Lemma).

Note: Some of the symbols used by Mendelson have been replaced here by different symbols since some are not available in HTML code. Also, Mendelson uses overscores to indicate the numeric notation of the formal system (such as * for **q*); these have been omitted, as they are secondary to the demonstration of the error in the proof.

The statement of the Lemma is given as:

Assume that the diagonal function D is representable in a theory with equality K in the language *L _{A}*. Then, for any wf ξ(

*x*

_{1}) in which

*x*

_{1}is the only free variable, there exists a closed wf φ such that

├_{ K} φ ⇔ ξ(**⌈**φ**⌉**)

where **⌈**φ**⌉** represents the Gödel numbering function, that is, it represents the Gödel number of φ.

The proof proceeds as follows:

Let δ(*x*_{1}, *x*_{2}) be a wf representing D in K. Construct the wf

(∇) (∀*x*_{2}) [δ(*x*_{1}, *x*_{2}) ⇒ ξ(*x*_{2})]

Let *m* be the Gödel number of (δ). Now substitute *m* for *x*_{1} in (∇):

(ζ) (∀*x*_{2}) [δ(*m*, *x*_{2}) ⇒ ξ(*x*_{2})]

Let *q* be the Gödel number of this wf ζ. So, *q* is **⌈**ζ**⌉**. Clearly, D(*m*) = *q*. (In fact, *m* is the Gödel number of a wf *β*(*x*_{1}), namely (∇), and *q* is the Gödel number of *β*(*m*). Since δ represents D in,

(∂) ├_{ K} δ(*m*, *q*)

The pertinent information here is that the relation δ is intended to represent D in the system K, that is that δ(*x*_{1}, *x*_{2}) ≡ *x*_{2} = D(*x*_{1}).

Mendelson provides a proof that D is a primitive recursive number-theoretic function in the section entitled Proposition 3.27, where he defines:

D(*u*) = Sub(*u*, Num(*u*), 21), and Num(*u*) is defined by

Num(0) = 2^{15}

Num(*u* + 1) = 2^{49} · 2^{3} · Num(*u*) · 2^{5}

Sub: defined previously as a primitive recursive number-theoretic function (Mendelson’s Proposition 3.26 (10))

Thus Mendelson defines D in purely number-theoretic terms as a primitive recursive number-theoretic function. (Footnote: It might be noted that Mendelson also makes references to Gödel numbering along with the actual definitions of primitive recursive number-theoretic relations. However, it is only the actual definitions that have applicability in any logical analysis.)

In his proof, Mendelson sets out by logical steps, as in the generic proof given above, that given that:

ζ is a relation defined by (∀*x*_{2}) [δ(*m*, *x*_{2}) ⇒ ξ(*x*_{2})],

ξ is any relation of the system K with one free variable,

δ(*m*, *x*_{2}) ≡ *x*_{2} = D(*m*),

D is a primitive recursive number theoretic function as defined above, and

*q* = D(*m*),

then it can be shown that:

├_{ K} ζ ⇔ ξ(*q*).

However, while Mendelson states that the function D is a primitive recursive number-theoretic function, he also states that *q* is the Gödel number of the formula ζ, that is, he is asserting that:

*q* = *GN*((∀*x*_{2}) [δ(*m*, *x*_{2}) ⇒ ξ(*x*_{2})]) *and**q* = D(*m*)

in other words, that

D(*m*) = *GN*((∀*x*_{2}) [δ(*m*, *x*_{2}) ⇒ ξ(*x*_{2})]).

Here, Mendelson’s proof is logically absurd. It cannot be the case that *D* is defined to be a primitive recursive number-theoretic function, and, at the same time, be defined in terms of the Gödel number of a formula of the system K. The definition of *q* as the Gödel number of a formula is a definition that includes the Gödel numbering function, a function of the meta-language, not of the system K.

As in the Boolos proof, the main part of the proof has nothing whatsoever to do with proving self-reference; the self-reference in the proof is that brought about by the invalid assumption that the function D can be at the same time a primitive recursive number-theoretic function, and * at the same time*, a function that is defined in terms of a meta-language to the system K.

## The Wikipedia Proof of the Diagonal Lemma

This proof of the lemma is that given in Wikipedia, as of 15 August 2012. The current page is Wikipedia - The Diagonal Lemma. The text of the proof of 15 August 2012 is given Wikipedia - The original text: below.

Note: The Wikipedia proof uses underlines to indicate the numeric notation of the formal system (such as *m* for *m*); these have been omitted here, as they are secondary to the demonstration of the error in the proof.

The statement of the Lemma is given as:

Let *T* be a first-order theory in the language of arithmetic and capable of representing all computable functions. Let ψ be a formula in the theory *T* with one free variable. The diagonal lemma states that there is a sentence φ such that φ ⇔ ψ(#(φ)) is provable in *T* (Here, # denotes the Gödel numbering function, that is, #(φ) represents the Gödel number of φ ).

The Proof of the Lemma commences as:

(1)

Let *f*: **N**⇒**N** be the function defined by:

(2)

*f*(#(θ)) = #(θ(#(θ)))

for each *T*-formula θ in one free variable, and

(3)

*f*(*n*) = 0 otherwise

(4)

The function *f* is computable, so there is a formula δ representing *f* in *T*. Thus for each formula θ, *T* proves

(5)

(∀*y*) [δ(#(θ), *y*) ⇔ *y* = *f*(#(θ))]

This proof is nonsensical from the outset. Regardless of the details of the system *T*, all formulas of the system *T* must be constructed from a clearly defined set of symbols. The Gödel numbering function must reference this entire set of symbols and must be in a meta-language to the system *T*, and because of this, it is impossible for a formula of the system *T* to include the definition of the Gödel numbering function.

This proof is yet another example of a ‘proof’ of self-reference being simply an assertion of the existence of self-reference included amongst a few lines of formulas that are dressed up to look like a logical proof.

It might be remarked of the given function that is defined as the outset of the proof by:

(1)

Let *f*: **N**⇒**N** be the function defined by:

(2)

*f*(#(θ)) = #(θ(#(θ)))

for each *T*-formula θ in one free variable, and

(3)

*f*(*n*) = 0 otherwise.

that a similar function can be defined in purely number-theoretic terms. For the first part of the definition (2), the value of the input to the function can be defined as a number that satisfies the condition that it can be factored into consecutive prime numbers (i.e. **2 ^{a}· 3^{b}· 5^{c}· 7^{d}· 11^{e}· 13^{f}** … ), and that the exponents of the prime factors must follow certain conditions. The value of the function if the input satisfies these conditions is a value that can be stated in purely numerical terms.

And, given this purely number-theoretic definition, you can define, in the meta-language, a particular Gödel numbering function. You can then state, ** in the meta-language**, that your previously defined number-theoretic function corresponds to this one particular Gödel numbering function (there are infinitely many Gödel numbering functions). But it must be borne in mind that this is stated in the meta-language, not in the language that this particular Gödel numbering function refers to.

As is the case for the other proofs mentioned here, you cannot have it both ways. You either define the function in terms of the Gödel numbering function, and accept that it is not a function that can be expressed by the formal system in question - or you define a function in purely number-theoretic terms and accept that it is not a function that refers to the Gödel numbering function.

## The ProofWiki Proof of the Diagonal Lemma

This proof of the lemma is that as given in ProofWiki as of 15 August 2012. The current page is ProofWiki - The Diagonal Lemma. The text of the proof of 15 August 2012 is given ProofWiki - The original text: below.

Note: Where the notation for the Gödel numbering function occurs in the original, for example as , this has been replaced by #(*A*), which denotes the Gödel number of *A*.

The statement of the Lemma is:

Let *T* be the set of theorems of some theory in the language of arithmetic which contains minimal arithmetic.

For any formula *B*(*y*) in the language of arithmetic, there is a sentence *G* such that

*T*├ *G* ⇔ *B*(#(*G*))

where #(*G*) is the Gödel number of *G*.

The ProofWiki proof proceeds as follows:

There is a primitive recursive function *diag* which is defined by:

(1)

*diag*(*n*) = #(*A*(#(*A*)))

where *A*(*x*) is the formula such that #(*A*) = *n*

where #( ) denotes the Gödel number of the contained formula. Since *T* contains Q, by *Recursive Sets are Definable in Arithmetic* applied to the graph of *diag*, we have that there is some formula Diag(*x*, *y*) which defines the graph of *diag* in *T*.

As for the Wikipedia proof, the proof is nonsensical from the outset. Although the proof states that *diag* is a primitive recursive function, the function *diag* is actually defined in terms of the Gödel numbering function. And, regardless of the details of the system *T*, all formulas of the system *T* must be constructed from a clearly defined set of symbols. The Gödel numbering function must reference this entire set of symbols and must be in a meta-language to the system *T*, and because of this, it is impossible for a formula of the system *T* to include the definition of a Gödel numbering function. Hence it is impossible for there to be a purported formula, Diag(*x*, *y*) as defined above, in the system *T*.

Incidentally, this proof includes another quite elementary error. At one step (see ProofWiki Step 6 below) the author of the proof adds the formula *G* as an axiom to the system *T* to create a different system *T ′*. Similarly, at another step (see ProofWiki Step 12 below), the author of the proof adds the formula *B*(#(*G*)) as an axiom to the system *T* to create a different system *T ′*.

However, in the first case, this assumes that the system *T* does not already prove the negation of *G* for any formula *B*, and in the second case, that the system *T* does not already prove the negation of *B*(#(*G*)) for any formula *B*. No justification is given to support these assumptions.

## Panu Raatikainen’s Proof of the Diagonal Lemma

In the article The Diagonalization Lemma on the Stanford Encyclopedia of Philosophy website, Panu Raatikainen, an associate professor at the University of Helsinki, gives a ‘proof’ of the Diagonalization Lemma. He proceeds as follows:

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

**are given, the operation of constructing the formula where the numeral for**

*n***has been substituted for the (free occurrences of the) variable**

*n**, that is,*

**x**

**A****(**, is purely mechanical.

*)*__n__

So is the analogous arithmetical operation which produces, given the Gödel number of a formula (with one free variable) ** ^{⌈}A(n)^{⌉}** and of a number

**, the Gödel number of the formula in which the numeral**

*n***has been substituted for the variable in the original formula, that is,**

__n__**.**

^{⌈}*A*(*n*)^{⌉}

The latter operation can be expressed in the language of arithmetic.

Here, Raatikainen claims that ** ^{⌈}A(n)^{⌉}** can be expressed in the “language of arithmetic”, but he declines to furnish any proof of this claim, nor does he provide any sort of logical argument to support the claim. In fact it can be shown that the Gödel numbering function cannot be expressed in the language of arithmetic, see The Impossibility of Representation of a Gödel Numbering Function by a Formula of the Formal System. By simply assuming that

**can be expressed in the language of arithmetic, Raatikainen has assumed that the language of arithmetic can self-reference, and the subsequent self-referential result is a trivial consequence of that assumption. You will see this sort of assumption time and time again used as a cheap trick in order to obtain self-reference.**

^{⌈}*A*(*n*)^{⌉}

## Vann McGee’s Proof of the Diagonal Lemma

Vann McGee is a professor of philosophy at MIT. Among his lecture course notes the following can be found on the MIT website at Gödel’s First Incompleteness Theorem by Vann McGee.

In it McGee starts off by saying (he refers to the Diagonal Lemma as the Self-referential Lemma) :

The following result is a cornerstone of modern logic:

**Self-referential Lemma:** For any formula Ψ(x), there is a sentence Φ such that (Φ ⇔ Ψ([⌈Φ⌉])) is a consequence of Q.

Then he goes on to say:

**Proof:** You would hope that such a deep theorem would have an insightful proof. No such luck. I am going to write down a sentence N and verify that it works. What I won’t do is give you a satisfactory explanation for why I write down the particular formula I do. I write down the formula because Gödel wrote down the formula, and Gödel wrote down the formula because, when he played the logic game he was able to see seven or eight moves ahead, whereas you and I are only able to see one or two moves ahead. I don’t know anyone who thinks he has a fully satisfying understanding of why the Self-referential Lemma works.

It has a rabbit-out-of-a-hat quality for everyone.

Well, in fact, it is very easy to have a very clear understanding of why the Diagonal Lemma does *not* work. It’s because it simply assumes that the Gödel numbering function can be expressed by the formal system, whereas the reality is that every Gödel-type numbering function is a meta-language function, and the formal language cannot express it (see the paper The Impossibility of Representation of a Gödel Numbering Function by a Formula of the Formal System ). And that’s why it might appear to have a “rabbit-out-of-a-hat” quality - because just like a magician pulling a rabbit out of an empty hat, there is a trick that makes it appear that that is happening, whereas the reality is far more prosaic.

In McGee’s subsequent ‘proof’, he defines a function where he simply assumes that the formal system can express the Gödel numbering function. So in effect his ‘proof’ amounts to:

*We prove that the formal system can represent itself by first assuming that the formal system can represent itself.*

Incidentally, McGee is incorrect in stating that Gödel wrote down that formula; in fact it appears that it was Carnap who first came up with an expression that can be considered to be a representation of the Diagonal Lemma formula. (Footnote:
Rudolf Carnap*. Logische Syntax der Sprache*, Springer Verlag, Vienna, 1934, English translation by A. Smeaton. *The logical syntax of language*. Routledge and Kegan Paul, 1937.)

Footnotes:

### Appendix: Text of the proof of Wikipedia article

This is the text of the proof of the Diagonal Lemma as given in Wikipedia as of 15 August 2012. The current page is Wikipedia - The Diagonal Lemma.

#### The Statement of the Lemma

Let T be a first-order theory in the language of arithmetic and capable of representing all computable functions. Let ψ be a formula in the theory T with one free variable. The diagonal lemma states that there is a sentence φ such that φ ⇔ ψ(#(φ)) is provable in T.

#### The Proof of the Lemma

Note: Line numbers have been added to the original Wiki section for easier reference.

(1)

Let *f*: **N**⇒**N** be the function defined by:

(2)

*f*(#(θ)) = #(θ(#(θ)))

for each *T*-formula θ in one free variable, and

(3)

*f*(*n*) = 0 otherwise.

(4)

The function *f* is computable, so there is a formula δ representing *f* in *T*. Thus for each formula θ, *T* proves

(5)

(∀*y*) [δ(#(θ), *y*) ⇔ *y* = *f*(#(θ))]

which is to say

(6)

(∀*y*) [δ(#(θ), *y*) ⇔ *y* = #(θ(#(θ)))]

(7)

Now define the formula β(*z*) as:

(8)

β(*z*) = (∀*y*) [δ(*z*, *y*) ⇒ ψ(*y*)]

then

(9)

β(#(θ)) ⇔ (∀*y*) [ *y* = #(θ(#(θ))) ⇒ ψ(*y*) ]

which is to say

(10)

β(#(θ)) ⇔ ψ(#(θ(#(θ))))

(11)

Let φ be the sentence β(#(β))

(12)

Then we can prove in *T* that:

(13)

φ ⇔ (∀*y*) [δ(#(β), *y*) ⇒ψ(*y*)] ⇔ (∀*y*) [*y* = #(β(#(β))) ⇒ ψ(*y*) ]

(14)

Working in T, analyze two cases:

(15)

Assuming φ holds, substitute #(β(#(β)) for *y* in the rightmost formula in (13), and obtain:

(16)

(#(β(#(β)) = #(β(#(β))) ⇒ ψ(#(β(#(β)))

(17)

Since φ = β(#(β)), it follows that ψ(#(φ)) holds.

(18)

Conversely, assume that ψ(#(β(#(β)))) holds. Then the final formula in (13) must be true, and φ is also true.

(19)

Thus φ ⇔ ψ(#(φ)) is provable in T, as desired.

### Appendix: Text of the proof of ProofWiki article

This is the text of the proof of the Diagonal Lemma as given in ProofWiki as of 15 August 2012. The current page is ProofWiki - The Diagonal Lemma.

Note: The notation for the Gödel numbering function has been changed, for example has been replaced by #(*A*).

#### The Statement of the Lemma:

Let *T* be the set of theorems of some theory in the language of arithmetic which contains minimal arithmetic.

For any formula *B*(*y*) in the language of arithmetic, there is a sentence G such that

*T*├ *G* ⇔ *B*(#(*G*))

where #(*G*) is the Gödel number of *G*.

#### The Proof of the Lemma:

There is a primitive recursive function *diag* which is defined by:

(1)

*diag*(*n*) = #(*A*(#(*A*)))

where *A*(*x*) is the formula such that #(*A*) = *n*

where, again, the #( ) denotes the Gödel number of the contained formula (and we are not being formal about distinguishing between integers and symbols in the language).

Informally, *diag* takes a Gödel number, decodes it to a formula, plugs in the Gödel number for that formula in place of a free variable, and encodes this new formula back to a new Gödel number.

Since *T* contains *Q*, by Recursive Sets are Definable in Arithmetic applied to the graph of *diag*, we have that there is some formula Diag(*x*, *y*) which defines the graph of *diag* in *T*.

That is:

(2)

*diag*(*n*) *= m* if and only if *T*├ Diag(*n*, *m*)

(3)

Let *A*(*x*) be the formula ∃*y*(Diag(*x*, *y*) ∧ *B*(*y*))

(4)

Let *G* be *A*(#(*A*))

(5)

We then have *T*├ Diag(#(*A*), #(*G*)), by checking the definitions.

(6)

Let *T ′ = T* ∪ {*G*}

(7)

Then *T ′*├ *A*(#(*A*))

(8)

Hence *T ′*├ ∃y(Diag(#(*A*), *y*) ∧ *B*(*y*))

(9)

But since #(*G*) is the only number such that *T*├ Diag(#(*A*), #(*G*)), this gives us

(10)

*T ′*├ *B*(#(*G*))

(11)

Thus, *T*├ *G* ⇒ *B*(#(*G*))

(12)

Let *T* = *T* ∪ {*B*(#(*G*))}

(13)

Again, we have *T*├ Diag(#(*A*), #(*G*)), so this gives us

(14)

*T ′*├ Diag(#(*A*), #(*G*)) ∧ *B*(#(*G*)), and hence

(15)

*T ′*├ ∃*y*(Diag(#(*A*), *y*) ∧ *B*(*y*))

(16)

But this is the same thing as

(17)

*T ′*├ *G*

(18)

Thus, *T*├ *B*(#(*G*)) ⇒ *G*

Thus *G* is as claimed.

**Interested in supporting this site?**

You can help by sharing the site with others. You can also donate at _{} where there are full details.

As site owner I reserve the right to keep my comments sections as I deem appropriate. I do not use that right to unfairly censor valid criticism. My reasons for deleting or editing comments do not include deleting a comment because it disagrees with what is on my website. Reasons for exclusion include:

Frivolous, irrelevant comments.

Comments devoid of logical basis.

Derogatory comments.

Long-winded comments.

Comments with excessive number of different points.

Questions about matters that do not relate to the page they post on. Such posts are not comments.

Comments with a substantial amount of mathematical terms not properly formatted will not be published unless a file (such as doc, tex, pdf) is simultaneously emailed to me, and where the mathematical terms are correctly formatted.

Reasons for deleting comments of certain users:

Bulk posting of comments in a short space of time, often on several different pages, and which are not simply part of an ongoing discussion. Multiple anonymous usernames for one person.

Users, who, when shown their point is wrong, immediately claim that they just wrote it wrong and rewrite it again - still erroneously, or else attack something else on my site - erroneously. After the first few instances, further posts are deleted.

Users who make persistent erroneous attacks in a scatter-gun attempt to try to find some error in what I write on this site. After the first few instances, further posts are deleted.

Difficulties in understanding the site content are usually best addressed by contacting me by e-mail.

Note: a password enables editing of comments, an email enables notification of replies