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 of the
natural numbers—specifically those theories that are strong enough to represent all
computable function
Computable functions are the basic objects of study in computability theory. Computable functions are the formalized analogue of the intuitive notion of algorithms, in the sense that a function is computable if there exists an algorithm that can do ...
s. The sentences whose existence is secured by the diagonal lemma can then, in turn, be used to prove fundamental limitative results such as
Gödel's incompleteness theorems and
Tarski's undefinability theorem.
Background
Let
be the set of
natural numbers. A
first-order
In mathematics and other formal sciences, first-order or first order most often means either:
* "linear" (a polynomial of degree at most one), as in first-order approximation and other calculus uses, where it is contrasted with "polynomials of hig ...
theory in the language of arithmetic ''represents'' the computable function
if there exists a "graph" predicate
in the language of
such that for each
: