Skip to content

Proof of the Diagonal Lemma in Logic

May 25, 2020

Why is the proof so short yet so difficult?

Saeed Salehi is a logician at the University of Tabriz in Iran. Three years ago he gave a presentation at a Moscow workshop on proofs of the diagonal lemma.

Today I thought I would discuss the famous diagonal lemma.

The lemma is related to Georg Cantor’s famous diagonal argument yet is different. The logical version imposes requirements on when the argument applies, and requires that it be expressible within a formal system.

The lemma underpins Kurt Gödel’s famous 1931 proof that arithmetic is incomplete. However, Gödel did not state it as a lemma or proposition or theorem or anything else. Instead, he focused his attention on what we now call Gödel numbering. We consider this today as “obvious” but his paper’s title ended with “Part I”. And he had readied a “Part II” with over 100 pages of calculations should people question that his numbering scheme was expressible within the logic.

Only after his proof was understood did people realize that one part, perhaps the trickiest part, could be abstracted into a powerful lemma. The tricky part is not the Gödel numbering. People granted that it can be brought within the logic once they saw enough of Gödel’s evidence, and so we may write {\ulcorner \phi \urcorner} for the function giving the Gödel number of any formula {\phi} and use that in other formulas. The hard part is what one does with such expressions.

This is what we will try to motivate.

Tracing the Lemma

Rudolf Carnap is often credited with the first formal statement, in 1934, for instance by Eliott Mendelson in his famous textbook on logic. Carnap was a member of the Vienna Circle, which Gödel frequented, and Carnap is considered a giant among twentieth-century philosophers. He worked on sweeping grand problems of philosophy, including logical positivism and analysis of human language via syntax before semantics. Yet it strikes us with irony that his work on the lemma may be the best remembered.

Who did the lemma first? Let’s leave that for others and move on to the mystery of how to prove the lemma once it is stated. I must say the lemma is easy to state, easy to remember, and has a short proof. But I believe that the proof is not easy to remember or even follow.

Salehi’s presentation quotes others’ opinions about the proof:

{\bullet } Sam Buss: “Its proof [is] quite simple but rather tricky and difficult to conceptualize.”

{\bullet} György Serény (we jump to Serény’s paper): “The proof of the lemma as it is presented in textbooks on logic is not self-evident to say the least.”

{\bullet } Wayne Wasserman: “It is `Pulling a Rabbit Out of the Hat’—Typical Diagonal Lemma Proofs Beg the Question.”

So I am not alone, and I thought it might be useful to try and unravel its proof. This exercise helped me and maybe it will help you.

Here goes.

Stating the Lemma

Let {S(w)} be a formula in Peano Arithmetic ({PA}). We claim that there is some sentence {\phi} so that

\displaystyle  PA \vdash \phi \iff S(\ulcorner \phi \urcorner).


Lemma 1 Suppose that {S(x)} is some formula in {PA}. Then there is a sentence {\phi} so that

\displaystyle  PA \vdash \phi \iff S(\ulcorner \phi \urcorner).

The beauty of this lemma is that it was used by Gödel and others to prove various powerful theorems. For example, the lemma quickly proves this result of Alfred Tarski:

Theorem 2 Suppose that {PA} is consistent. Then truth cannot be defined in {PA}. That is there is no formula {Tr(x)} so that for all sentences {\phi} {PA} proves

\displaystyle  \phi \iff Tr(\ulcorner \phi \urcorner).

The proof is this. Assume there is such a formula {Tr(x)}. Then use the diagonal lemma and get

\displaystyle  \phi \iff \neg Tr(\ulcorner \phi \urcorner).

This shows that

\displaystyle  \phi \iff \neg Tr(\ulcorner \phi \urcorner) \iff Tr(\ulcorner \phi \urcorner).

This is a contradiction. A short proof.

The Proof

The key is to define the function {F(n)} as follows: Suppose that {n} is the Gödel number of a formula of the form {A(x)} for some variable {x} then

\displaystyle  F(n) = \ulcorner A(\ulcorner A(x) \urcorner) \urcorner.

If {n} is not of this form then define {F(n)=0}. This is a strange function, a clever function, but a perfectly fine function, It certainly maps numbers to numbers. It is certainly recursive, actually it is clearly computable in polynomial time for any reasonable Gödel numbering. Note: the function {F} does depend on the choice of the variable {x}. Thus,

\displaystyle  F(\ulcorner y=0 \urcorner) = \ulcorner (\ulcorner y=0 \urcorner)=0 \urcorner,


\displaystyle  F(\ulcorner x=0 \urcorner) = \ulcorner (\ulcorner x=0 \urcorner)=0 \urcorner.

Now we make two definitions:

\displaystyle  \begin{array}{rcl}        g(w) &\equiv& S(F(w)) \\        \phi &\equiv& g(\ulcorner g(x) \urcorner). \end{array}

Now we compute just using the definitions of {F, g, \phi}:

\displaystyle  \begin{array}{rcl}        \phi &=& g(\ulcorner g(x) \urcorner) \\                 &=& S(F(\ulcorner g(x) \urcorner)) \\           &=& S(\ulcorner g(\ulcorner g(x) \urcorner) \urcorner) \\               &=& S(\ulcorner \phi \urcorner). \end{array}

We are done.

But …

Where did this proof come from? Suppose that you forgot the proof but remember the statement of the lemma. I claim that we can then reconstruct the proof.

First let’s ask: Where did the definition of the function {F} come from? Let’s see. Imagine we defined

\displaystyle  \begin{array}{rcl}        g(w) &\equiv& S(F(w)) \\        \phi &\equiv& g(\ulcorner g(x) \urcorner). \end{array}

But left {F} undefined for now. Then

\displaystyle  \begin{array}{rcl}        \phi &=& g(\ulcorner g(x) \urcorner) \\                 &=& S(F(\ulcorner g(x) \urcorner)). \end{array}

But we want {\phi = S(\ulcorner \phi \urcorner)} that happens provided:

\displaystyle  \ulcorner g(\ulcorner g(x) \urcorner) \urcorner) = F(\ulcorner g(x) \urcorner).

This essentially gives the definition of the function {F}. Pretty neat.

But but …

Okay where did the definition of {g} and {\phi} come from? It is reasonable to define

\displaystyle  g(w) \equiv S(F(w)),

for some {F}. We cannot change {S} but we can control the input to the formula {S}, so let’s put a function there. Hence the definition for {g} is not unreasonable.

Okay how about the definition of {\phi}? Well we could argue that this is the magic step. If we are given this definition then {F} follows, by the above. I would argue that {\phi} is not completely surprising. The name of the lemma is after all the “diagonal” lemma. So defining {\phi} as the application of {g} to itself is plausible.

Taking an Exam

Another way to think about the diagonal lemma is imagine you are taking an exam in logic. The first question is:

Prove in {PA} that for any {S(x)} there is a sentence {\phi} so that

\displaystyle  \phi \iff S(\ulcorner \phi \urcorner).

You read the question again and think: “I wish I had studied harder, I should have not have checked Facebook last night. And then went out and {\dots}” But you think let’s not panic, let’s think.

Here is what you do. You say let me define

\displaystyle  g(x) = S(F(x)),

for some {F}. You recall there was a function that depends on {S}, and changing the input from {x} to {F(x)} seems to be safe. Okay you say, now what? I need the definition of {F}. Hmmm let me wait on that. I recall vaguely that {F} had a strange definition. I cannot recall it, so let me leave it for now.

But you think: I need a sentence {\phi}. A sentence cannot have an unbound variable. So {\phi} cannot be {g(x)}. It could be {g(m)} for some {m}. But what could {m} be? How about {\ulcorner \phi \urcorner}. This makes

\displaystyle  \phi = g(\ulcorner g \urcorner).

It is after all the diagonal lemma. Hmmm does this work. Let’s see if this works. Wait as above I get that {F} is now forced to satisfy

\displaystyle  F(\ulcorner g(x) \urcorner) = \ulcorner g(\ulcorner g(x) \urcorner) \urcorner.

Great this works. I think this is the proof. Wonderful. Got the first question.

Let’s look at the next exam question. Oh no {\dots}

Open Problems

Does this help? Does this unravel the mystery of the proof? Or is it still magic?

[Fixed equation formatting]

20 Comments leave one →
  1. May 25, 2020 11:40 am

    Cool! I once reviewed a paper of Salehi.

  2. May 25, 2020 11:48 am

    I’ve always felt that von Neumann’s theory of self-reproducing machines sheds the most
    light on the diagonal lemma. (See pp.64-66 of these notes, from this webpage.)

  3. May 25, 2020 11:51 am

    I’ve always felt that von Neumann’s theory of self-reproducing automatat sheds the most light on the diagonal lemma. (See pp.64-66 of the notes “Basics of First-Order Logic” on this webpage.)

    • May 25, 2020 12:52 pm

      First comment is moderated, then comments are automatic for an X time period—where we don’t know X. We also don’t know if deleting someone’s comments gets scored against X, so let us know if another comment doesn’t come thru right away.

  4. Dave Lewis permalink
    May 25, 2020 12:03 pm

    Latex is not rendering from “Now we make two definitions:” to “that happens provided”

    • May 25, 2020 12:50 pm

      Thanks—fixed. We sometimes forget which LaTeX features are rendered.

  5. May 25, 2020 1:39 pm

    What is the parenthetization of the Lemma? Is it

    (PA ⊢ φ) ⇔ S(⌜φ⌝)

    or is it

    PA ⊢ (φ ⇔ S(⌜φ⌝) )

    • rjlipton permalink*
      May 26, 2020 7:51 am

      Dear Bruno:

      We mean the latter. That is PA ⊢ (φ ⇔ S(⌜φ⌝) ). Sorry for the confusion.

      Best and be safe


  6. Pascal Koiran permalink
    May 26, 2020 1:41 am

    The diagonal lemma looks very similar to fixed point theorems in recursion theory.
    Is there a formal or historical connection between the two ?

  7. May 26, 2020 5:55 am

    Yup, I second Pascal Koiran.
    Isn’t this about the same than Kleene second recursion theorem?

    • May 26, 2020 4:58 pm

      Indeed (kevembuangga and Pascal), I had a thought to add my own 2cents by tying it to some old notes on motivating the fixed-point Recursion Theorem:
      But Dick’s post was already long enough and I’ve never taken time to polish or finish these notes; the chess world has been keeping me insanely busy all month.

  8. Flavio Botelho permalink
    May 26, 2020 1:10 pm

    My issue with the Diagonal Argument is that it is a halting algorithm (discovered before the Theory of Computation), personally I think every algorithm capable of solving the Halting Problem is physically unrealizable (“Unreal”? It’s funny that that this turns the chosen terminology “Real Numbers” an oxymoron)… Just as traveling to the past would lead to logical paradoxes, algorithms that solve the halting problem seem to be in the same ballpark…

    I am still waiting for some Logician out there to mix Ultrafinitism and Theory of Computation into a Foundation (UltraComputationism?) that simply discards the physically unrealizable. If you have only a countable sets then the Axiom of Choice becomes a trivial theorem… Modern Constructivism research might already have all the necessary pieces, but doesn’t seem much interested in Foundations?

  9. Peter Gerdes permalink
    May 27, 2020 5:24 am

    This is much more intuitive to prove via the recursion theorem which itself can be motivated by the idea that an appropriate notion of computation allows a machine to read it’s own source code.

  10. Marcus Schaefer permalink
    May 27, 2020 10:18 am

    James Owings’ “Diagonalization and the recursion theorem” ( views the recursion theorem (and the diagonal lemma, and various other related results) as a failed diagonalization. (In Soare’s “Turing Computability” some of that material can be found in Section 2.2.4 “A Diagonal Argument which Fails”.) That way of thinking about the diagonal lemma removes some of the magic. The connection to Cantor’s argument is so direct that one may be tempted to conjecture that this is how Goedel arrived at his insight.


  11. Stella Seremetaki Mathematician permalink
    June 6, 2020 12:24 pm

    Reblogged this on Magazino.

  12. proofless permalink
    September 13, 2020 2:23 pm

    I have a question… How do you compute the Gödel number \ulcorner g(x) \urcorner? Given any formula $S(x)$ I understand how to create a Gödel number: You simply have each symbol of the formula represent a different number, and use those numbers as powers of primes. For instance x = 0 might have a coding of 2^{13}3^{1}5^{2} where 13, 1, 2 represent x, =, 0 respectively and 2, 3, 5 code the first, second, and third symbols of the formula.

    The problem with g(x) is that it contains a function F(x) for the input for the free variable in the formual S(x). How is F(x) represented in the Gödel coding? If S(x ):= x = 0 what is S(F(x)) and \ulcorner S(F(x))\urcorner?

  13. November 16, 2020 12:22 am

    A very elementary beginner question: Say S(x) is the formula x = zero. There is only one numeral that can be substituted in for x to make S(x) provable, namely S(zero). However, no reasonable Godel numbering would have zero be the Godel number of a syntactically valid formula, much less a provable one. So, how do you find phi for this example? Is the claim of the lemma that phi and S(godelNumber(phi)) are both either provable or their syntactic negations are both provable? I.e., if the arrow symbol in the lemma was syntactic as opposed to meta-mathematical, then I suppose you could use a contraposition tautology as an axiom and deduce the formula not phi not S(godelNum(phi)). In that case, basically every formula that is provably false would suffice, because none of them would satisfy the particular S() in this example, and all would be provably false. The lemma would presumably pick one such example. I’m wondering if there is a “least” value the lemma generates, similar to least fixed points in denotational semantics, if there are multiple candidates for phi. BTW – thanks for this great posting!

    • rjlipton permalink*
      November 17, 2020 2:30 pm

      Dear Greg Johnson:

      Thanks for your kind interest. Let me think about this. You are right about 0 not the number of 0.



      • November 27, 2020 2:53 pm

        One thought/speculation: The theorem does not assert the existence of a phi such that phi and S(phi) are both provable. It only asserts the existence of a phi such that the provability status of the formulas phi and S(phi) is the same. So, any provably false formula phi would do; S(phi) would also not be provable. An even crazier example would be S(x) == x < 0. There is no WFF phi at all whose Godel number would make S(n) provable, so any WFF that is provably false would suffice to satisfy the theorem in this case.

  14. November 27, 2020 3:23 pm

    Regarding your open question: While I could follow and replicate your logic, the “aha” still eluded me, and left me feeling that there is more magic to be brought out into the open! Struggling with your elegant and thought-provoking article, something finally clicked, and I finally understood, came into direct contact with, and stood in awe of the genius of Kurt Godel.

    My path to intuition was via lambda calculus. I translated your derivation in a somewhat rough and ready manner into the Y combinator:

    Your F(x) can be thought to correspond to (x x), a well-formed lambda expression with one free variable.

    g(w) then maps to S(F(w)), which by the above corresponds to S(w w).

    We now wish to view g(w) as a function and apply it, so let us abstract:

    g = lambda w.S(w w)

    g(g) then becomes:

    (lambda w.S(w w)) (lambda w.S(w w))

    This is our candidate expression for phi. (And is, of course, the Y combinator applied to S.)

    Now, let’s do one function application to the above expression for phi. (“beta reduction” in lambda calculus terms.)

    Taking the body of the left-hand term and replacing instances of “w” with the right-hand term, we get:

    S(lambda w.S(w w)) (lambda w.S(w w))

    And this is precisely S(phi).

    So, one might say that Kurt Godel effectively invented the Y combinator. In his proof, it seems that he started with something like S(F(x)): “for all p, not isProof(p, x, x)”. He then took the Godel number of this expression, and substituted it in for x. So, his “phi” was actually something like S(lambda w.S(w w)) (lambda w.S(w w)), which he then transformed via the equivalent in logic of beta reduction to S(S(lambda w.S(w w)) (lambda w.S(w w))). The new outer S is then interpreted to assert that its argument has no proof, but the WFF that therefore has no proof is exactly “phi”.

Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out /  Change )

Google photo

You are commenting using your Google account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s