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 , the weaker
Robinson arithmetic as well as any theory containing
(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 ...
. We write
for the code assigned to
by the numbering. For
, the standard numeral of
(i.e.
and
), let
be the standard numeral of the code of
(i.e.
is
). We assume a
standard Gödel numbering
Representation Theorem
Let
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, ...
in the language of arithmetic containing
''represents'' the
-ary recursive function
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 ...
in the language of
s.t. for all
, if
then
.
The representation theorem is provable, i.e. every recursive function is representable in
.
The Diagonal Lemma and its proof
Diagonal Lemma: Let be a first-order theory containing ( Robinson arithmetic) and let be any formula in the language of with only as free variable. Then there is a sentence in the language of s.t. .
Intuitively,
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
."
Proof: Let
be the recursive function which associates the code of each formula
with only one free variable
in the language of
with the code of the closed formula
(i.e. the substitution of
into
for
) and
for other arguments. (The fact that
is recursive depends on the choice of the Gödel numbering, here the
standard one.)
By the representation theorem,
represents every recursive function. Thus, there is a formula
be the 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
(
Robinson arithmetic).
Diagonal Lemma with Parameters
Let
be any formula with free variables
.
Then there is a formula
with free variables
s.t.
.
Uniform Diagonal Lemma
Let
be any formula with free variables
.
Then there is a formula
with free variables
s.t. for all
,
.
Simultaneous Diagonal Lemma
Let
and
be formulae with free variable
and
.
Then there are sentence
and
s.t.
and
.
The case with
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
with
as free variable (in a sufficiently expressive language), then there exists a sentence
such that
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