Diagonal lemma
In mathematical logic, the diagonal lemma 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 theory|first-order Peano arithmetic], the weaker Robinson arithmetic as well as any theory containing . A common statement of the lemma 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. We write for the code assigned to by the numbering. For, the standard numeral of, let be the standard numeral of the code of . We assume a standard Gödel numberingRepresentation theorem
Let be the set of natural numbers. A first-order theory in the language of arithmetic containing represents the -ary computable function if there is a formula in the language of such that for all, if then.The representation theorem is true, i.e. every computable function is representable in.
The diagonal lemma and its proof
Diagonal Lemma: Let be a first-order theory containing and let be any formula in the language of with only as free variable. Then there is a sentence in the language of such that.Intuitively, is a self-referential sentence that "says of itself that it has the property."
Proof: Let be the computable function that associates the code of each formula with only one free variable in the language of with the code of the closed formula and for other arguments.
By the representation theorem, represents every computable function. Thus, there is a formula representing, in particular, for each,.
Let be an arbitrary formula with only as free variable. We now define as, and let be. Then the following equivalences are provable in :
Some generalizations
There are various generalizations of the diagonal lemma. We present only three of them; in particular, combinations of the below generalizations yield new generalizations. Let be a first-order theory containing .Diagonal lemma with parameters
Let be any formula with free variables.Then there is a formula with free variables such that.
Uniform diagonal lemma
Let be any formula with free variables.Then there is a formula with free variables such that for all,.
Simultaneous diagonal lemma
Let and be formulae with free variables and.Then there are sentence and such that and.
The case with many formulae is similar.
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 with as free variable, then there exists a sentence such that is true. Carnap's work was phrased in terms of truth rather than provability. 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.