Diagonal lemma
From Wikipedia, the free encyclopedia
In mathematical logic, Kurt Gödel's diagonal lemma is a precise way of constructing the self-referential sentences required to prove Gödel's incompleteness and Tarski's indefinability theorems.
Contents |
[edit] The lemma and its proof
Let T be a theory, in any extension of the language of arithmetic, capable of representing all computable functions. Let A(x) be a formula whose sole free variable is x. Let all formulas in the language of T have a code number, and let "Φ" denote the code number of formula Φ.
Diagonal Lemma: There exists a formula B such that .
Intuitively, B is a self-referential sentence, for it says of itself that it has the property A(x).
Proof. Let D(A) be the sentence A("A"), i.e. the result of substituting the quotation name of A for x in A. D(A) is the diagonalization of A, and D is the diagonal function. D can be shown to be computable ("primitive recursive" in older terminology). Since T is capable of representing all computable functions, let diag(x) denote the diagonal function that goes from code numbers to code numbers. Consider the sentence A(diag(x)), asserting that the diagonalization of x has property A. Now let B be the diagonalization of A(diag(x)), so that B is the sentence A(diag(''A(diag(x))'')). Hence B has the form A(t), where t is the term diag(''A(diag(x))''). Clearly,
But t denotes the diagonalization of A(diag(x)), namely B. Now B is provable in T, so that:
Substitute (2) into (1) to obtain
- QED.
[edit] History
The lemma is called "diagonal" because it bears some resemblance to Cantor's diagonal argument. The term "diagonal lemma" does not appear in Kurt Gödel's epochal 1931 article, or in Tarski (1936). The lemma as stated and proved in this entry appears to be primarily the creation of Raymond Smullyan, whose work on this broad topic culminated in Smullyan (1992). Smullyan in turn acknowledges earlier work by Willard Quine.
[edit] See also
- Gödel number
- Gödel incompleteness theorem
- Tarski's indefinability theorem
- Quine (computing)
- Self-reference
- Indirect self-reference
[edit] References
- Raymond Smullyan, 1991. Gödel's Incompleteness Theorems. Oxford Univ. Press.
- --------, 1994. Diagonalization and Self-Reference. Oxford Univ. Press.
- Alfred Tarski, 1936, "The Concept of Truth in Formal Systems" in Corcoran, J., ed., 1983. Logic, Semantics, Metamathematics: Papers from 1923 to 1938. Indianapolis IN: Hackett.