Diagonal Lemma
   HOME

TheInfoList



OR:

In
mathematical logic Mathematical logic is the study of Logic#Formal logic, formal logic within mathematics. Major subareas include model theory, proof theory, set theory, and recursion theory (also known as computability theory). Research in mathematical logic com ...
, the diagonal lemma (also known as diagonalization lemma, self-reference lemma or fixed point theorem) establishes the existence of
self-referential Self-reference is a concept that involves referring to oneself or one's own attributes, characteristics, or actions. It can occur in language, logic, mathematics, philosophy, and other fields. In natural language, natural or formal languages, ...
sentences in certain formal theories. A particular instance of the diagonal lemma was used by
Kurt Gödel Kurt Friedrich Gödel ( ; ; April 28, 1906 – January 14, 1978) was a logician, mathematician, and philosopher. Considered along with Aristotle and Gottlob Frege to be one of the most significant logicians in history, Gödel profoundly ...
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 Cantor's diagonal argument (among various similar namesthe diagonalisation argument, the diagonal slash argument, the anti-diagonal argument, the diagonal method, and Cantor's diagonalization proof) is a mathematical proof that there are infin ...
in set and number theory. The diagonal lemma applies to any sufficiently strong theories capable of representing the diagonal function. Such theories include first-order Peano arithmetic \mathsf, the weaker Robinson arithmetic \mathsf as well as any theory containing \mathsf (i.e. which interprets it). 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.


Background


Gödel Numbering

The diagonal lemma also requires a
Gödel numbering 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. Kurt Gödel developed the concept for the proof of his incom ...
\alpha. We write \alpha (\varphi) for the code assigned to \varphi by the numbering. For \overline, the standard numeral of n (i.e. \overline =_ \mathsf and \overline =_ \mathsf(\overline) ), let \ulcorner \varphi \urcorner be the standard numeral of the code of \varphi (i.e. \ulcorner \varphi \urcorner is \overline). We assume a standard Gödel numbering


Representation Theorem

Let \mathbb be the set of
natural numbers In mathematics, the natural numbers are the numbers 0, 1, 2, 3, and so on, possibly excluding 0. Some start counting with 0, defining the natural numbers as the non-negative integers , while others start with 1, defining them as the positiv ...
. A first-order
theory A theory is a systematic and rational form of abstract thinking about a phenomenon, or the conclusions derived from such thinking. It involves contemplative and logical reasoning, often supported by processes such as observation, experimentation, ...
T in the language of arithmetic containing \mathsf ''represents'' the k-ary recursive function f: \mathbb^k\rightarrow\mathbb if there is a
formula In science, a formula is a concise way of expressing information symbolically, as in a mathematical formula or a ''chemical formula''. The informal use of the term ''formula'' in science refers to the general construct of a relationship betwe ...
\varphi_f(x_1, \dots, x_k, y) in the language of T s.t. for all m_1, \dots, m_k \in \mathbb , if f(m_1, \dots, m_k) = n then T \vdash \forall y (\varphi_f (\overline, \dots, \overline, y) \leftrightarrow y = \overline ). The representation theorem is provable, i.e. every recursive function is representable in T.


The Diagonal Lemma and its proof

Diagonal Lemma: Let T be a first-order theory containing \mathsf ( Robinson arithmetic) and let \psi (x) be any formula in the language of T with only x as free variable. Then there is a sentence \varphi in the language of T s.t. T \vdash \varphi \leftrightarrow \psi (\ulcorner \varphi \urcorner).
Intuitively, \varphi is a
self-referential Self-reference is a concept that involves referring to oneself or one's own attributes, characteristics, or actions. It can occur in language, logic, mathematics, philosophy, and other fields. In natural language, natural or formal languages, ...
sentence which "says of itself that it has the property \psi." Proof: Let diag_T:\mathbb\to\mathbb be the recursive function which associates the code of each formula \varphi (x) with only one free variable x in the language of T with the code of the closed formula \varphi (\ulcorner \varphi \urcorner ) (i.e. the substitution of \ulcorner \varphi \urcorner into \varphi for x) and 0 for other arguments. (The fact that diag_T is recursive depends on the choice of the Gödel numbering, here the standard one.) By the representation theorem, T represents every recursive function. Thus, there is a formula \delta(x,y) be the formula representing diag_T, in particular, for each \varphi (x), T \vdash \delta(\ulcorner \varphi \urcorner , y) \leftrightarrow y = \ulcorner \varphi (\ulcorner \varphi \urcorner) \urcorner . Let \psi(x) be an arbitrary formula with only x as free variable. We now define \chi (x) as \exists y (\delta(x,y) \land \psi(y)), and let \varphi be \chi (\ulcorner \chi \urcorner). Then the following equivalences are provable in T: \varphi \leftrightarrow \chi(\ulcorner \chi \urcorner) \leftrightarrow \exists y (\delta(\ulcorner \chi \urcorner,y) \land \psi(y)) \leftrightarrow \exists y (y = \ulcorner \chi (\ulcorner \chi \urcorner) \urcorner \land \psi(y)) \leftrightarrow \exists y (y = \ulcorner \varphi \urcorner \land \psi(y)) \leftrightarrow \psi (\ulcorner \varphi \urcorner) .


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 T be a first-order theory containing \mathsf ( Robinson arithmetic).


Diagonal Lemma with Parameters

Let \psi (x, y_1, \dots , y_n) be any formula with free variables x, y_1, \dots , y_n. Then there is a formula \varphi (y_1, \dots y_n) with free variables y_1, \dots , y_n s.t. T \vdash \varphi (y_1 , \dots , y_n) \leftrightarrow \psi (\ulcorner \varphi (y_1 , \dots , y_n) \urcorner, y_1 , \dots , y_n).


Uniform Diagonal Lemma

Let \psi (x, y_1, \dots , y_n) be any formula with free variables x, y_1, \dots , y_n. Then there is a formula \varphi (y_1, \dots y_n) with free variables y_1, \dots , y_n s.t. for all m_1 , \dots , m_n \in \mathbb , T \vdash \varphi (\overline , \dots , \overline) \leftrightarrow \psi (\ulcorner \varphi (\overline , \dots , \overline) \urcorner, \overline , \dots , \overline) .


Simultaneous Diagonal Lemma

Let \psi_1 (x_1 , x_2) and \psi_2 (x_1 , x_2) be formulae with free variable x_1 and x_2. Then there are sentence \varphi_1 and \varphi_2 s.t. T \vdash \varphi_1 \leftrightarrow \psi_1(\ulcorner \varphi_1 \urcorner, \ulcorner \varphi_2 \urcorner) and T \vdash \varphi_2 \leftrightarrow \psi_2(\ulcorner \varphi_1 \urcorner, \ulcorner \varphi_2 \urcorner). The case with n many formulae is similar.


History

The lemma is called "diagonal" because it bears some resemblance to
Cantor's diagonal argument Cantor's diagonal argument (among various similar namesthe diagonalisation argument, the diagonal slash argument, the anti-diagonal argument, the diagonal method, and Cantor's diagonalization proof) is a mathematical proof that there are infin ...
. The terms "diagonal lemma" or "fixed point" do not appear in
Kurt Gödel Kurt Friedrich Gödel ( ; ; April 28, 1906 – January 14, 1978) was a logician, mathematician, and philosopher. Considered along with Aristotle and Gottlob Frege to be one of the most significant logicians in history, Gödel profoundly ...
's 1931 article or in
Alfred Tarski Alfred Tarski (; ; born Alfred Teitelbaum;School of Mathematics and Statistics, University of St Andrews ''School of Mathematics and Statistics, University of St Andrews''. January 14, 1901 – October 26, 1983) was a Polish-American logician ...
's 1936 article. In 1934,
Rudolf Carnap Rudolf Carnap (; ; 18 May 1891 – 14 September 1970) was a German-language philosopher who was active in Europe before 1935 and in the United States thereafter. He was a major member of the Vienna Circle and an advocate of logical positivism. ...
was the first to publish the diagonal lemma in some level of generality, which says that for any formula \psi (x) with x as free variable (in a sufficiently expressive language), then there exists a sentence \varphi such that \varphi \leftrightarrow \psi(\ulcorner \varphi \urcorner) is true (in some standard model). Carnap's work was phrased in terms of
truth Truth or verity is the Property (philosophy), property of being in accord with fact or reality.Merriam-Webster's Online Dictionarytruth, 2005 In everyday language, it is typically ascribed to things that aim to represent reality or otherwise cor ...
rather than provability (i.e. semantically rather than syntactically). Remark also that the concept of recursive functions was not yet developed in 1934. The diagonal lemma is closely related to Kleene's recursion theorem in
computability theory Computability theory, also known as recursion theory, is a branch of mathematical logic, computer science, and the theory of computation that originated in the 1930s with the study of computable functions and Turing degrees. The field has since ex ...
, 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 Provability logic is a modal logic, in which the box (or "necessity") operator is interpreted as 'it is provable that'. The point is to capture the notion of a proof predicate of a reasonably rich formal theory, such as Peano arithmetic. Examples ...
.See Smoryński 2022, Sec. 3.


See also

* Indirect self-reference * List of fixed point theorems *
Self-reference Self-reference is a concept that involves referring to oneself or one's own attributes, characteristics, or actions. It can occur in language, logic, mathematics, philosophy, and other fields. In natural or formal languages, self-reference ...
* Self-referential paradoxes


Notes


References

* George Boolos and
Richard Jeffrey Richard Carl Jeffrey (August 5, 1926 – November 9, 2002) was an American philosopher, logician, and probability theorist. He is best known for developing and championing the philosophy of radical probabilism and the associated heuristic of ...
, 1989. ''Computability and Logic'', 3rd ed. Cambridge University Press. *
Rudolf Carnap Rudolf Carnap (; ; 18 May 1891 – 14 September 1970) was a German-language philosopher who was active in Europe before 1935 and in the United States thereafter. He was a major member of the Vienna Circle and an advocate of logical positivism. ...
, 1934. ''Logische Syntax der Sprache''. (English translation: 2003. ''The Logical Syntax of Language''. Open Court Publishing.) * Haim Gaifman, 2006.
Naming and Diagonalization: From Cantor to Gödel to Kleene
. ''Logic Journal of the IGPL'', 14: 709–728. * Petr Hájek & Pavel Pudlák, 2016 (first edition 1998). ''Metamathematics of First-Order Arithmetic.'' Springer Verlag. * Peter Hinman, 2005. ''Fundamentals of Mathematical Logic''. A K Peters. * Mendelson, Elliott, 1997. ''Introduction to Mathematical Logic,'' 4th ed. Chapman & Hall. * Panu Raatikainen, 2015a
The Diagonalization Lemma
In
Stanford Encyclopedia of Philosophy The ''Stanford Encyclopedia of Philosophy'' (''SEP'') is a freely available online philosophy resource published and maintained by Stanford University, encompassing both an online encyclopedia of philosophy and peer-reviewed original publication ...
, ed. Zalta. * Panu Raatikainen, 2015b
Gödel's Incompleteness Theorems
In
Stanford Encyclopedia of Philosophy The ''Stanford Encyclopedia of Philosophy'' (''SEP'') is a freely available online philosophy resource published and maintained by Stanford University, encompassing both an online encyclopedia of philosophy and peer-reviewed original publication ...
, ed. Zalta. * Raymond Smullyan, 1991. ''Gödel's Incompleteness Theorems''. Oxford Univ. Press. * Raymond Smullyan, 1994.
Diagonalization and Self-Reference
'. Oxford Univ. Press. * Craig Smoryński, 2023. 'The early history of formal diagonalization'. ''Logic Journal of the IGPL'', 31.6: 1203–1224. * *
Alfred Tarski Alfred Tarski (; ; born Alfred Teitelbaum;School of Mathematics and Statistics, University of St Andrews ''School of Mathematics and Statistics, University of St Andrews''. January 14, 1901 – October 26, 1983) was a Polish-American logician ...
, tr. J. H. Woodger, 1983. 'The Concept of Truth in Formalized Languages'
English translation of Tarski's 1936 article
In A. Tarski, ed. J. Corcoran, 1983, ''Logic, Semantics, Metamathematics'', Hackett. {{DEFAULTSORT:Diagonal Lemma Mathematical logic Lemmas Articles containing proofs