Logic and Language

Logic and Language

Copyright © James R Meyer 2012 - 2017 www.jamesrmeyer.com

This page is keyboard accessible:

• Use**Tab**, **Shift + Tab **keys to traverse the main menu. To enter a sub-menu use the **Right Arrow** key. To leave a sub-menu use the **Left Arrow** or the **Escape** key.

• The**Enter** or the **Space** key opens the active menu item.

• To skip the menu and move to the main content, press**Tab** after the page loads to reveal a skip button.

• To get back to the top of the page anytime, press the**Home** key.

• For more information, click here: Accessibility Close this tip.

• Use

• The

• To skip the menu and move to the main content, press

• To get back to the top of the page anytime, press the

• For more information, click here: Accessibility Close this tip.

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

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.) The error in Smith’s proof is the same error that is dealt with in detail in the paper A Fundamental Flaw in an Incompleteness Proof by Peter Smith PDF. 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.

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* ¬ψ(

(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 (PDF).

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.

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*).

so that here, rather than using the general case of:

├_{ 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.

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

ISBN‑10: 0412808307 ISBN‑13: 978‑0412808302 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. Also, Mendelson uses overscores to indicate the numeric notation of the formal system (such as *q*¯ 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 ψ(

├_{ 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 wf β(*x*_{1}), namely (δ), and *q* is the Gödel number of β(*m*). Since δ represents D in,

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

The pertinent information here is that the relation δ represents 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 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 also a function that is defined in terms of a meta-language to the system K.

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.

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.

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

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

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 (PDF). By simply assuming that

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.*

Besides, in fact it wasn’t Gödel who wrote down that formula, 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:

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.

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.

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.

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*).

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*.

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 *∪* *{*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.

Diverse opinions and criticisms are welcome, but messages that are frivolous, irrelevant or devoid of logical basis will be blocked (comments will be checked before appearing on this site). Difficulties in understanding the site content are usually best addressed by contacting me by e-mail.Note: you will be asked to provide an e-mail address - this will only be used to notify you of replies to your comments - it will never be used for any other purpose, will never be displayed and does not require verification. Comments are common to the entire website, so please indicate what section of the site you are commenting on.

If you cannot see any comments below, it may be that a plug-in on your browser is blocking Disqus comments from loading. Avast anti-virus in particular is known to do this, especially with Internet Explorer and Safari. See Disqus Browser plug-in/extension conflicts or Why isn’t the comment box loading?.

Please wait for comments to load …

It has come to my notice that, when asked about the demonstration of the flaw in his proof (see A Fundamental Flaw in an Incompleteness Proof by Peter Smith PDF), Smith refuses to engage in any logical discussion, and instead attempts to deflect attention away from any such discussion. If any other reader has tried to engage with Smith regarding my demonstration of the flaw, I would be interested to know what the outcome was.

There is a new addition to the page Yet another flawed incompleteness proof, where Berto’s proof of incompleteness in his book *There’s something about Gödel* comes under scrutiny.

I found that making, adding or deleting footnotes in the traditional manner proved to be a major pain. So I developed a different system for footnotes which makes inserting or changing footnotes a doddle. You can check it out at Easy Footnotes for Web Pages (Accessibility friendly).

I have now added a new section to my paper on Russell O’Connor’s claim of a computer verified incompleteness proof. This shows that the flaw in the proof arises from a reliance on definitions that include unacceptable assumptions - assumptions that are not actually checked by the computer code. See also the new page Representability.

There is now a new page on Chaitin’s Constant (Chaitin’s Omega), which demonstrates that Chaitin has failed to prove that it is actually algorithmically irreducible.

16th Mar 2015 Bishops Dancing with Pixies?

23rd Feb 2015 Artificial Intelligence

31 Mar 2015 Cranks and Crackpots

For convenience, there are now two pages on this site with links to various material relating to Gödel and the Incompleteness Theorem

– a page with general links:

– and a page relating specifically to the Gödel mind-machine debate:

All pages on this website are printer friendly, and will print the main content in a convenient format. Note that the margins are set by your browser print settings.

Note: for some browsers JavaScript must be enabled for this to operate correctly.

Comments on this site are welcome, please see the comment section.

Please note that this web site, like any other is a collection of various statements. Not all of this web site is intended to be factual. Some of it is personal opinion or interpretation.

If you prefer to ask me directly about the material on this site, please send me an e-mail with your query, and I will attempt to reply promptly.

Feedback about site design would also be appreciated so that I can improve the site.

Copyright © James R Meyer 2012 - 2017

www.jamesrmeyer.com