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.
The diagonal lemma applies to any sufficiently strong theories capable of representing the diagonal function. Such theories include first-order Peano arithmetic P A {\displaystyle {\mathsf {PA}}} , the weaker Robinson arithmetic Q {\displaystyle {\mathsf {Q}}} as well as any theory containing Q {\displaystyle {\mathsf {Q}}} (i.e. which interprets it).[2] A common statement of the lemma (as given below) makes the stronger assumption that the theory can represent all recursive functions, but all the theories mentioned have that capacity, as well.
The diagonal lemma also requires a Gödel numbering α {\displaystyle \alpha } . We write α ( φ ) {\displaystyle \alpha (\varphi )} for the code assigned to φ {\displaystyle \varphi } by the numbering. For n ¯ {\displaystyle {\overline {n}}} , the standard numeral of n {\displaystyle n} (i.e. 0 ¯ = d f 0 {\displaystyle {\overline {0}}=_{df}{\mathsf {0}}} and n + 1 ¯ = d f S ( n ¯ ) {\displaystyle {\overline {n+1}}=_{df}{\mathsf {S}}({\overline {n}})} ), let ⌜ φ ⌝ {\displaystyle \ulcorner \varphi \urcorner } be the standard numeral of the code of φ {\displaystyle \varphi } (i.e. ⌜ φ ⌝ {\displaystyle \ulcorner \varphi \urcorner } is α ( φ ) ¯ {\displaystyle {\overline {\alpha (\varphi )}}} ). We assume a standard Gödel numbering
Let N {\displaystyle \mathbb {N} } be the set of natural numbers. A first-ordertheory T {\displaystyle T} in the language of arithmetic containing Q {\displaystyle {\mathsf {Q}}} represents the k {\displaystyle k} -ary recursive function f : N k → N {\displaystyle f:\mathbb {N} ^{k}\rightarrow \mathbb {N} } if there is a formula φ f ( x 1 , … , x k , y ) {\displaystyle \varphi _{f}(x_{1},\dots ,x_{k},y)} in the language of T {\displaystyle T} s.t. for all m 1 , … , m k ∈ N {\displaystyle m_{1},\dots ,m_{k}\in \mathbb {N} } , if f ( m 1 , … , m k ) = n {\displaystyle f(m_{1},\dots ,m_{k})=n} then T ⊢ ∀ y ( φ f ( m 1 ¯ , … , m k ¯ , y ) ↔ y = n ¯ ) {\displaystyle T\vdash \forall y(\varphi _{f}({\overline {m_{1}}},\dots ,{\overline {m_{k}}},y)\leftrightarrow y={\overline {n}})} .
The representation theorem is provable, i.e. every recursive function is representable in T {\displaystyle T} .[3]
Diagonal Lemma: Let T {\displaystyle T} be a first-order theory containing Q {\displaystyle {\mathsf {Q}}} (Robinson arithmetic) and let ψ ( x ) {\displaystyle \psi (x)} be any formula in the language of T {\displaystyle T} with only x {\displaystyle x} as free variable. Then there is a sentence φ {\displaystyle \varphi } in the language of T {\displaystyle T} s.t. T ⊢ φ ↔ ψ ( ⌜ φ ⌝ ) {\displaystyle T\vdash \varphi \leftrightarrow \psi (\ulcorner \varphi \urcorner )} .
Intuitively, φ {\displaystyle \varphi } is a self-referential sentence which "says of itself that it has the property ψ {\displaystyle \psi } ."
Proof: Let d i a g T : N → N {\displaystyle diag_{T}:\mathbb {N} \to \mathbb {N} } be the recursive function which associates the code of each formula φ ( x ) {\displaystyle \varphi (x)} with only one free variable x {\displaystyle x} in the language of T {\displaystyle T} with the code of the closed formula φ ( ⌜ φ ⌝ ) {\displaystyle \varphi (\ulcorner \varphi \urcorner )} (i.e. the substitution of ⌜ φ ⌝ {\displaystyle \ulcorner \varphi \urcorner } into φ {\displaystyle \varphi } for x {\displaystyle x} ) and 0 {\displaystyle 0} for other arguments. (The fact that d i a g T {\displaystyle diag_{T}} is recursive depends on the choice of the Gödel numbering, here the standard one.)
By the representation theorem, T {\displaystyle T} represents every recursive function. Thus, there is a formula δ ( x , y ) {\displaystyle \delta (x,y)} be the formula representing d i a g T {\displaystyle diag_{T}} , in particular, for each φ ( x ) {\displaystyle \varphi (x)} , T ⊢ δ ( ⌜ φ ⌝ , y ) ↔ y = ⌜ φ ( ⌜ φ ⌝ ) ⌝ {\displaystyle T\vdash \delta (\ulcorner \varphi \urcorner ,y)\leftrightarrow y=\ulcorner \varphi (\ulcorner \varphi \urcorner )\urcorner } .
Let ψ ( x ) {\displaystyle \psi (x)} be an arbitrary formula with only x {\displaystyle x} as free variable. We now define χ ( x ) {\displaystyle \chi (x)} as ∃ y ( δ ( x , y ) ∧ ψ ( y ) ) {\displaystyle \exists y(\delta (x,y)\land \psi (y))} , and let φ {\displaystyle \varphi } be χ ( ⌜ χ ⌝ ) {\displaystyle \chi (\ulcorner \chi \urcorner )} . Then the following equivalences are provable in T {\displaystyle T} :
There are various generalizations of the diagonal lemma. We present only three of them; in particular, combinations of the below generalizations yield new generalizations.[4] Let T {\displaystyle T} be a first-order theory containing Q {\displaystyle {\mathsf {Q}}} (Robinson arithmetic).
Let ψ ( x , y 1 , … , y n ) {\displaystyle \psi (x,y_{1},\dots ,y_{n})} be any formula with free variables x , y 1 , … , y n {\displaystyle x,y_{1},\dots ,y_{n}} .
Then there is a formula φ ( y 1 , … y n ) {\displaystyle \varphi (y_{1},\dots y_{n})} with free variables y 1 , … , y n {\displaystyle y_{1},\dots ,y_{n}} s.t. T ⊢ φ ( y 1 , … , y n ) ↔ ψ ( ⌜ φ ( y 1 , … , y n ) ⌝ , y 1 , … , y n ) {\displaystyle T\vdash \varphi (y_{1},\dots ,y_{n})\leftrightarrow \psi (\ulcorner \varphi (y_{1},\dots ,y_{n})\urcorner ,y_{1},\dots ,y_{n})} .
Let ψ ( x , y 1 , … , y n ) {\displaystyle \psi (x,y_{1},\dots ,y_{n})} be any formula with free variables x , y 1 , … , y n {\displaystyle x,y_{1},\dots ,y_{n}} .
Then there is a formula φ ( y 1 , … y n ) {\displaystyle \varphi (y_{1},\dots y_{n})} with free variables y 1 , … , y n {\displaystyle y_{1},\dots ,y_{n}} s.t. for all m 1 , … , m n ∈ N {\displaystyle m_{1},\dots ,m_{n}\in \mathbb {N} } , T ⊢ φ ( m 1 ¯ , … , m n ¯ ) ↔ ψ ( ⌜ φ ( m 1 ¯ , … , m n ¯ ) ⌝ , m 1 ¯ , … , m n ¯ ) {\displaystyle 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}}})} .
Let ψ 1 ( x 1 , x 2 ) {\displaystyle \psi _{1}(x_{1},x_{2})} and ψ 2 ( x 1 , x 2 ) {\displaystyle \psi _{2}(x_{1},x_{2})} be formulae with free variable x 1 {\displaystyle x_{1}} and x 2 {\displaystyle x_{2}} .
In 1934, Rudolf Carnap was the first to publish the diagonal lemma in some level of generality, which says that for any formula ψ ( x ) {\displaystyle \psi (x)} with x {\displaystyle x} as free variable (in a sufficiently expressive language), then there exists a sentence φ {\displaystyle \varphi } such that φ ↔ ψ ( ⌜ φ ⌝ ) {\displaystyle \varphi \leftrightarrow \psi (\ulcorner \varphi \urcorner )} is true (in some standard model).[6] Carnap's work was phrased in terms of truth rather than provability (i.e. semantically rather than syntactically).[7] Remark also that the concept of recursive functions was not yet developed in 1934.
be any formula in the language of T {\displaystyle T}
as free variable. Then there is a sentence φ {\displaystyle \varphi }
.
