Diagonal lemma

In mathematical logic, the diagonal lemma (also known as diagonalization lemma, self-reference lemma or fixed point theorem) establishes the existence of self-referential sentences in certain formal theories.

A particular instance of the diagonal lemma was used by Kurt Gödel in 1931 to construct his proof of the incompleteness theorems as well as in 1933 by Tarski to prove his undefinability theorem. In 1934, Carnap was the first to publish the diagonal lemma at some level of generality. The diagonal lemma is named in reference to Cantor's diagonal argument in set theory and number theory.

The diagonal lemma applies to any sufficiently strong theories capable of representing the diagonal function. Such theories include first-order Peano arithmetic <math>\mathsf{PA}</math>, the weaker Robinson arithmetic <math>\mathsf{Q}</math> as well as any theory containing <math>\mathsf{Q}</math> (i.e. that interprets it). A common statement of the lemma (as given below) makes the stronger assumption that the theory can represent all (total) computable functions, but all the theories mentioned have that capacity, as well.

Background

Gödel numbering

The diagonal lemma also requires a Gödel numbering <math>\alpha</math>. We write <math>\alpha (\varphi)</math> for the code assigned to <math>\varphi</math> by the numbering. For <math>\overline{n}</math>, the standard numeral of <math>n</math> (i.e. <math>\overline{0} =_{df} \mathsf{0}

</math> and <math>\overline{n+1} =_{df} \mathsf{S}(\overline{n}) </math>), let <math>\ulcorner \varphi \urcorner </math> be the standard numeral of the code of <math>\varphi</math> (i.e. <math>\ulcorner \varphi \urcorner </math> is <math>\overline{\alpha(\varphi)}</math>). We assume a standard Gödel numbering

Representation theorem

Let <math>\mathbb{N}</math> be the set of natural numbers. A first-order theory <math>T</math> in the language of arithmetic containing <math>\mathsf{Q}</math> represents the <math>k</math>-ary (total) computable function <math>f: \mathbb{N}^k\rightarrow\mathbb{N}</math> if there is a formula <math>\varphi_f(x_1, \dots, x_k, y)</math> in the language of <math>T</math> such that for all <math>m_1, \dots, m_k \in \mathbb{N} </math>, if <math>f(m_1, \dots, m_k) = n</math> then <math>T \vdash \forall y (\varphi_f (\overline{m_1}, \dots, \overline{m_k}, y) \leftrightarrow y = \overline{n} )</math>.

The representation theorem is true, i.e. every computable function is representable in <math>T</math>.

The diagonal lemma and its proof

Diagonal Lemma: Let <math>T</math> be a first-order theory containing <math>\mathsf{Q}</math> (Robinson arithmetic) and let <math>\psi (x)</math> be any formula in the language of <math>T</math> with only <math>x</math> as free variable. Then there is a sentence <math>\varphi</math> in the language of <math>T</math> such that <math>T \vdash \varphi \leftrightarrow \psi (\ulcorner \varphi \urcorner)</math>.

Intuitively, <math>\varphi</math> is a self-referential sentence that "says of itself that it has the property <math>\psi</math>."

Proof: Let <math>diag_T:\mathbb{N}\to\mathbb{N}</math> be the computable function that associates the code of each formula <math>\varphi (x)</math> with only one free variable <math>x</math> in the language of <math>T</math> with the code of the closed formula <math>\varphi (\ulcorner \varphi \urcorner )</math> (i.e. the substitution of <math>\ulcorner \varphi \urcorner

</math> into <math>\varphi</math> for <math>x</math>) and <math>0</math> for other arguments. (The fact that <math>diag_T</math> is computable depends on the choice of the Gödel numbering, here the standard one.)

By the representation theorem, <math>T</math> represents every computable function. Thus, there is a formula <math>\delta(x,y)</math> representing <math>diag_T</math>, in particular, for each <math>\varphi (x)</math>, <math>T \vdash \delta(\ulcorner \varphi \urcorner , y) \leftrightarrow y = \ulcorner \varphi (\ulcorner \varphi \urcorner) \urcorner </math>.

Let <math>\psi(x)</math> be an arbitrary formula with only <math>x</math> as free variable. We now define <math>\chi (x)</math> as <math>\exists y (\delta(x,y) \land \psi(y))</math>, and let <math>\varphi

</math> be <math>\chi (\ulcorner \chi \urcorner)</math>. Then the following equivalences are provable in <math>T</math>:

<math>\varphi \leftrightarrow \chi(\ulcorner \chi \urcorner) \leftrightarrow \exists y (\delta(\ulcorner \chi \urcorner,y) \land \psi(y)) \leftrightarrow \exists y (y = \ulcorner \chi (\ulcorner \chi \urcorner) \urcorner \land \psi(y)) \leftrightarrow \exists y (y = \ulcorner \varphi \urcorner \land \psi(y)) \leftrightarrow \psi (\ulcorner \varphi \urcorner) </math>.

Some generalizations

There are various generalizations of the diagonal lemma. We present only some of them; in particular, combinations of the first three generalizations below yield new generalizations. Let <math>T</math> be a first-order theory containing <math>\mathsf{Q}</math> (Robinson arithmetic).

Diagonal lemma with parameters

Let <math>\psi (x, y_1, \dots , y_n)

</math> be any formula with free variables <math>x, y_1, \dots , y_n</math>.

Then there is a formula <math>\varphi (y_1, \dots y_n)</math> with free variables <math>y_1, \dots , y_n

</math> such that <math>T \vdash \varphi (y_1 , \dots , y_n) \leftrightarrow \psi (\ulcorner \varphi (y_1 , \dots , y_n) \urcorner, y_1 , \dots , y_n)</math>.

Uniform diagonal lemma

Let <math>\psi (x, y_1, \dots , y_n)

</math> be any formula with free variables <math>x, y_1, \dots , y_n</math>.

Then there is a formula <math>\varphi (y_1, \dots y_n)</math> with free variables <math>y_1, \dots , y_n

</math> such that for all <math>m_1 , \dots , m_n \in \mathbb{N}

</math>, <math>T \vdash \varphi (\overline{m_1} , \dots , \overline{m_n}) \leftrightarrow \psi (\ulcorner \varphi (\overline{m_1} , \dots , \overline{m_n}) \urcorner, \overline{m_1} , \dots , \overline{m_n})

</math>.

Simultaneous diagonal lemma

Let <math>\psi_1 (x_1 , x_2)</math> and <math>\psi_2 (x_1 , x_2)

</math> be formulae with free variables <math>x_1</math> and <math>x_2</math>.

Then there are sentence <math>\varphi_1</math> and <math>\varphi_2

</math> such that <math>T \vdash \varphi_1 \leftrightarrow \psi_1(\ulcorner \varphi_1 \urcorner, \ulcorner \varphi_2 \urcorner)</math> and <math>T \vdash \varphi_2 \leftrightarrow \psi_2(\ulcorner \varphi_1 \urcorner, \ulcorner \varphi_2 \urcorner)</math>.

The case with <math>n</math> many formulae is similar.

Strong diagonal lemma

Let <math>\psi (x)</math> be any formula in the language of <math>T</math> with only <math>x</math> as free variable. Then there is a term <math>t</math> in the language of <math>T</math> such that <math>T \vdash t = \ulcorner \psi (t) \urcorner </math>.

Trivially, the diagonal lemma follows from the strong diagonal lemma (take <math>\varphi (x)</math> to be <math>\psi (t)</math>). Note however that the strong diagonal lemma depends on the language of <math>T</math>, particularly on whether there is such a term <math>t</math>. Typically, the strong diagonal lemma fails for theories in the basic language of arithmetic (such as <math>\mathsf{Q}</math> or <math>\mathsf{PA}</math>), but holds for primitive recursive arithmetic <math>\mathsf{PRA}</math> which has a function symbol for each primitive recursive functions.

History

The lemma is called "diagonal" because it bears some resemblance to Cantor's diagonal argument. The terms "diagonal lemma" or "fixed point" do not appear in Kurt Gödel's 1931 article or in Alfred Tarski's 1936 article.

In 1934, Rudolf Carnap was the first to publish the diagonal lemma in some level of generality, which says that for any formula <math>\psi (x)</math> with <math>x</math> as free variable (in a sufficiently expressive language), then there exists a sentence <math>\varphi</math> such that <math>\varphi \leftrightarrow \psi(\ulcorner \varphi \urcorner)</math> is true (in some standard model). Carnap's work was phrased in terms of truth rather than provability (i.e. semantically rather than syntactically). Moreover, the concept of computable functions was not yet developed in 1934.

The diagonal lemma is closely related to Kleene's recursion theorem in computability theory, and their respective proofs are similar. In 1952, Léon Henkin asked whether sentences that state their own provability are provable. His question led to more general analyses of the diagonal lemma, especially with Löb's theorem and provability logic.

Notes

References

George Boolos and Richard Jeffrey, 1989. Computability and Logic, 3rd ed. Cambridge University Press.
Rudolf Carnap, 1934. Logische Syntax der Sprache. (English translation: 2003. The Logical Syntax of Language. Open Court Publishing.)
Haim Gaifman, 2006. 'Naming and Diagonalization: From Cantor to Gödel to Kleene'. Logic Journal of the IGPL, 14: 709–728.

Robert G. Jeroslow, 1973. 'Redundancies in the Hilbert-Bernays Derivability Conditions for Gödel's Second Incompleteness Theorem'. The Journal of Symbolic Logic, 38.3: 359–367.

Petr Hájek & Pavel Pudlák, 2016 (first edition 1998). Metamathematics of First-Order Arithmetic. Springer Verlag.

Peter Hinman, 2005. Fundamentals of Mathematical Logic. A K Peters.
Mendelson, Elliott, 1997. Introduction to Mathematical Logic, 4th ed. Chapman & Hall.
Panu Raatikainen, 2015a. The Diagonalization Lemma. In Stanford Encyclopedia of Philosophy, ed. Zalta.
Panu Raatikainen, 2015b. Gödel's Incompleteness Theorems. In Stanford Encyclopedia of Philosophy, ed. Zalta.
Raymond Smullyan, 1991. Gödel's Incompleteness Theorems. Oxford Univ. Press.
Raymond Smullyan, 1994. Diagonalization and Self-Reference. Oxford Univ. Press.
Craig Smoryński, 2023. 'The early history of formal diagonalization'. Logic Journal of the IGPL, 31.6: 1203–1224.
Alfred Tarski, tr. J. H. Woodger, 1983. 'The Concept of Truth in Formalized Languages'. English translation of Tarski's 1936 article. In A. Tarski, ed. J. Corcoran, 1983, Logic, Semantics, Metamathematics, Hackett.