Diagonal lemma
Encyclopedia
In mathematical logic
, the diagonal lemma or fixed point theorem establishes the existence of self-referential sentence
s in certain formal theories of the natural number
s -- specifically those theories that are strong enough to represent all computable function
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 indefinability theorem
.
s. A theory
T represents the computable function f : N→N if there exists a formula δ(x,y) in the language of T such that for each n, T proves [f(n) = y ↔ δ(n,y)].
Here n is the numeral corresponding to the natural number n, which is defined to be the closed term 1+ ··· +1 (n ones), and f(n) is the numeral corresponding to f(n).
The diagonal lemma also requires that there be a systematic way of assigning to every formula θ a natural number #(θ) called its Gödel number
. Formulas can then be represented within the theory by the numerals corresponding to their Gödel numbers.
The diagonal lemma applies to theories capable of representing all primitive recursive functions. Such theories include Peano arithmetic and the weaker Robinson arithmetic
. A common statement of the lemma (as given below) makes the stronger assumption that the theory can represent all computable function
s.
theory in the language of arithmetic and capable of representing all computable function
s. Let ψ be a formula in the theory T with one free variable. The diagonal lemma states that there is a sentence φ such that φ ↔ ψ(#(φ)) is provable in T.
Intuitively, φ is a self-referential sentence saying that φ has the property ψ. The sentence φ can also be viewed as a fixed point
of the operation assigning to each formula θ the sentence ψ(#(θ)). The sentence φ constructed in the proof is not literally the same as ψ(#(φ)), but is provably equivalent to it in the theory T.
for any formula θ in the theory T having one free variable. If n is not the Gödel number of a formula, then f(n) = 0. The function f is computable, so there is a formula δ representing f in T. Thus for each formula θ, T proves [ δ(#(θ),y) ⇔ y = f(#(θ))],
which is to say [ δ(#(θ),y) ⇔ y = #(θ(#(θ)))].
Now define the formula β(z) as:
then
which is to say
Let φ be the sentence β(#(β)). Then we can prove in T that: φ ⇔ (∀y) [ δ(#(β),y) ⇒ ψ(y)] ⇔ (∀y) [ (y = #(β(#(β))) ⇒ ψ(y)].
Working in T, analyze two cases:
1. Assuming φ holds, substitute #(β(#(β)) for y in the rightmost formula in (*), and obtain:) = #(β(#(β))) → ψ(#(β(#(β))),
Since φ = β(#(β)), it follows that ψ(#(φ)) holds.
2. Conversely, assume that ψ(#(β(#(β)))) holds. Then the final formula in (*) must be true, and φ is also true.
Thus φ ↔ ψ(#(φ)) is provable in T, as desired.
in computability theory
, and their respective proofs are similar.
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 epochal 1931 article, or in Tarski (1936). Carnap (1934) was the first to prove that for any formula ψ in a theory T satisfying certain conditions, there exists a formula φ such that φ ↔ ψ(#(φ)) is provable in T. Carnap's work was phrased in alternate language, as the concept of computable function
s was not yet developed in 1934. Mendelson (1997, p. 204) believes that Carnap was the first to state that something like the diagonal lemma was implicit in Gödel's reasoning. Gödel was aware of Carnap's work by 1937.
Mathematical logic
Mathematical logic is a subfield of mathematics with close connections to foundations of mathematics, theoretical computer science and philosophical logic. The field includes both the mathematical study of logic and the applications of formal logic to other areas of mathematics...
, the diagonal lemma or fixed point theorem establishes the existence of self-referential sentence
Sentence (mathematical logic)
In mathematical logic, a sentence of a predicate logic is a boolean-valued well formed formula with no free variables. A sentence can be viewed as expressing a proposition, something that may be true or false...
s in certain formal theories of the natural number
Natural number
In mathematics, the natural numbers are the ordinary whole numbers used for counting and ordering . These purposes are related to the linguistic notions of cardinal and ordinal numbers, respectively...
s -- specifically those theories that are strong enough to represent all computable function
Computable function
Computable functions are the basic objects of study in computability theory. Computable functions are the formalized analogue of the intuitive notion of algorithm. They are used to discuss computability without referring to any concrete model of computation such as Turing machines or register...
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 indefinability theorem
Tarski's indefinability theorem
Tarski's undefinability theorem, stated and proved by Alfred Tarski in 1936, is an important limitative result in mathematical logic, the foundations of mathematics, and in formal semantics...
.
Background
Let N be the set of natural numberNatural number
In mathematics, the natural numbers are the ordinary whole numbers used for counting and ordering . These purposes are related to the linguistic notions of cardinal and ordinal numbers, respectively...
s. A theory
Theory (mathematical logic)
In mathematical logic, a theory is a set of sentences in a formal language. Usually a deductive system is understood from context. An element \phi\in T of a theory T is then called an axiom of the theory, and any sentence that follows from the axioms is called a theorem of the theory. Every axiom...
T represents the computable function f : N→N if there exists a formula δ(x,y) in the language of T such that for each n, T proves [f(n) = y ↔ δ(n,y)].
Here n is the numeral corresponding to the natural number n, which is defined to be the closed term 1+ ··· +1 (n ones), and f(n) is the numeral corresponding to f(n).
The diagonal lemma also requires that there be a systematic way of assigning to every formula θ a natural number #(θ) called its Gödel number
Gödel number
In mathematical logic, a Gödel numbering is a function that assigns to each symbol and well-formed formula of some formal language a unique natural number, called its Gödel number. The concept was famously used by Kurt Gödel for the proof of his incompleteness theorems...
. Formulas can then be represented within the theory by the numerals corresponding to their Gödel numbers.
The diagonal lemma applies to theories capable of representing all primitive recursive functions. Such theories include Peano arithmetic and the weaker Robinson arithmetic
Robinson arithmetic
In mathematics, Robinson arithmetic, or Q, is a finitely axiomatized fragment of Peano arithmetic , first set out in R. M. Robinson . Q is essentially PA without the axiom schema of induction. Since Q is weaker than PA, it is incomplete...
. A common statement of the lemma (as given below) makes the stronger assumption that the theory can represent all computable function
Computable function
Computable functions are the basic objects of study in computability theory. Computable functions are the formalized analogue of the intuitive notion of algorithm. They are used to discuss computability without referring to any concrete model of computation such as Turing machines or register...
s.
Statement of the lemma
Let T be a first-orderFirst-order logic
First-order logic is a formal logical system used in mathematics, philosophy, linguistics, and computer science. It goes by many names, including: first-order predicate calculus, the lower predicate calculus, quantification theory, and predicate logic...
theory in the language of arithmetic and capable of representing all computable function
Computable function
Computable functions are the basic objects of study in computability theory. Computable functions are the formalized analogue of the intuitive notion of algorithm. They are used to discuss computability without referring to any concrete model of computation such as Turing machines or register...
s. Let ψ be a formula in the theory T with one free variable. The diagonal lemma states that there is a sentence φ such that φ ↔ ψ(#(φ)) is provable in T.
Intuitively, φ is a self-referential sentence saying that φ has the property ψ. The sentence φ can also be viewed as a fixed point
Fixed point (mathematics)
In mathematics, a fixed point of a function is a point that is mapped to itself by the function. A set of fixed points is sometimes called a fixed set...
of the operation assigning to each formula θ the sentence ψ(#(θ)). The sentence φ constructed in the proof is not literally the same as ψ(#(φ)), but is provably equivalent to it in the theory T.
Proof
Let f: N→N be a function such that:- f(#(θ)) = #(θ(#(θ))
for any formula θ in the theory T having one free variable. If n is not the Gödel number of a formula, then f(n) = 0. The function f is computable, so there is a formula δ representing f in T. Thus for each formula θ, T proves [ δ(#(θ),y) ⇔ y = f(#(θ))],
which is to say [ δ(#(θ),y) ⇔ y = #(θ(#(θ)))].
Now define the formula β(z) as:
- β(z) = (∀y) [δ(z,y) ⇒ ψ(y)],
then
- β(#(θ)) ⇔ (∀y) [ y = #(θ(#(θ))) ⇒ ψ(y)],
which is to say
- β(#(θ)) ⇔ ψ(#(θ(#(θ))))
Let φ be the sentence β(#(β)). Then we can prove in T that: φ ⇔ (∀y) [ δ(#(β),y) ⇒ ψ(y)] ⇔ (∀y) [ (y = #(β(#(β))) ⇒ ψ(y)].
Working in T, analyze two cases:
1. Assuming φ holds, substitute #(β(#(β)) for y in the rightmost formula in (*), and obtain:) = #(β(#(β))) → ψ(#(β(#(β))),
Since φ = β(#(β)), it follows that ψ(#(φ)) holds.
2. Conversely, assume that ψ(#(β(#(β)))) holds. Then the final formula in (*) must be true, and φ is also true.
Thus φ ↔ ψ(#(φ)) is provable in T, as desired.
History
The diagonal lemma is closely related to Kleene's recursion theoremKleene's recursion theorem
In computability theory, Kleene's recursion theorems are a pair of fundamental results about the application of computable functions to their own descriptions...
in computability theory
Computability theory
Computability theory, also called recursion theory, is a branch of mathematical logic that originated in the 1930s with the study of computable functions and Turing degrees. The field has grown to include the study of generalized computability and definability...
, and their respective proofs are similar.
The lemma is called "diagonal" because it bears some resemblance to Cantor's diagonal argument
Cantor's diagonal argument
Cantor's diagonal argument, also called the diagonalisation argument, the diagonal slash argument or the diagonal method, was published in 1891 by Georg Cantor as a mathematical proof that there are infinite sets which cannot be put into one-to-one correspondence with the infinite set of natural...
. The terms "diagonal lemma" or "fixed point" do not appear in Kurt Gödel
Kurt Gödel
Kurt Friedrich Gödel was an Austrian logician, mathematician and philosopher. Later in his life he emigrated to the United States to escape the effects of World War II. One of the most significant logicians of all time, Gödel made an immense impact upon scientific and philosophical thinking in the...
's epochal 1931 article, or in Tarski (1936). Carnap (1934) was the first to prove that for any formula ψ in a theory T satisfying certain conditions, there exists a formula φ such that φ ↔ ψ(#(φ)) is provable in T. Carnap's work was phrased in alternate language, as the concept of computable function
Computable function
Computable functions are the basic objects of study in computability theory. Computable functions are the formalized analogue of the intuitive notion of algorithm. They are used to discuss computability without referring to any concrete model of computation such as Turing machines or register...
s was not yet developed in 1934. Mendelson (1997, p. 204) believes that Carnap was the first to state that something like the diagonal lemma was implicit in Gödel's reasoning. Gödel was aware of Carnap's work by 1937.