Incubator escapee wiki

Diagonal lemma

Article Discussion

Template:Short description {{#invoke:other uses|otheruses}}In mathematical logic, the diagonal lemma (also known as diagonalization lemma, self-reference lemma or fixed point theorem) 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.<ref>See Smoryński 2022, Sec. 3.</ref> The diagonal lemma is named in reference to Cantor's diagonal argument 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 <math>\mathsf{PA}</math>, the weaker Robinson arithmetic <math>\mathsf{Q}</math> as well as any theory containing <math>\mathsf{Q}</math> (i.e. which interprets it).<ref>See Hájek and Pudlák 2016, Chap. III.</ref> 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.

BackgroundEdit

Gödel NumberingEdit

The diagonal lemma also requires a Gödel numbering <math>\alpha</math>. We write <math>\alpha (\varphi)</math> for the code assigned to <math>\varphi</math> by the numbering. For <math>\overline{n}</math>, the standard numeral of <math>n</math> (i.e. <math>\overline{0} =_{df} \mathsf{0}

</math> and <math>\overline{n+1} =_{df} \mathsf{S}(\overline{n}) </math>), let <math>\ulcorner \varphi \urcorner </math> be the standard numeral of the code of <math>\varphi</math> (i.e. <math>\ulcorner \varphi \urcorner </math> is <math>\overline{\alpha(\varphi)}</math>). We assume a standard Gödel numbering

Representation TheoremEdit

Let <math>\mathbb{N}</math> be the set of natural numbers. A first-order theory <math>T</math> in the language of arithmetic containing <math>\mathsf{Q}</math> represents the <math>k</math>-ary recursive function <math>f: \mathbb{N}^k\rightarrow\mathbb{N}</math> if there is a formula <math>\varphi_f(x_1, \dots, x_k, y)</math> in the language of <math>T</math> s.t. for all <math>m_1, \dots, m_k \in \mathbb{N} </math>, if <math>f(m_1, \dots, m_k) = n</math> then <math>T \vdash \forall y (\varphi_f (\overline{m_1}, \dots, \overline{m_k}, y) \leftrightarrow y = \overline{n} )</math>.

The representation theorem is provable, i.e. every recursive function is representable in <math>T</math>.<ref>See Hinman 2005, Chap 4.6 for additional details and a proof of this theorem.</ref>

The Diagonal Lemma and its proofEdit

Diagonal Lemma: Let <math>T</math> be a first-order theory containing <math>\mathsf{Q}</math> (Robinson arithmetic) and let <math>\psi (x)</math> be any formula in the language of <math>T</math> with only <math>x</math> as free variable. Then there is a sentence <math>\varphi</math> in the language of <math>T</math> s.t. <math>T \vdash \varphi \leftrightarrow \psi (\ulcorner \varphi \urcorner)</math>.

Intuitively, <math>\varphi</math> is a self-referential sentence which "says of itself that it has the property <math>\psi</math>."

Proof: Let <math>diag_T:\mathbb{N}\to\mathbb{N}</math> be the recursive function which associates the code of each formula <math>\varphi (x)</math> with only one free variable <math>x</math> in the language of <math>T</math> with the code of the closed formula <math>\varphi (\ulcorner \varphi \urcorner )</math> (i.e. the substitution of <math>\ulcorner \varphi \urcorner </math> into <math>\varphi</math> for <math>x</math>) and <math>0</math> for other arguments. (The fact that <math>diag_T</math> is recursive depends on the choice of the Gödel numbering, here the standard one.)

By the representation theorem, <math>T</math> represents every recursive function. Thus, there is a formula <math>\delta(x,y)</math> be the formula representing <math>diag_T</math>, in particular, for each <math>\varphi (x)</math>, <math>T \vdash \delta(\ulcorner \varphi \urcorner , y) \leftrightarrow y = \ulcorner \varphi (\ulcorner \varphi \urcorner) \urcorner </math>.

Let <math>\psi(x)</math> be an arbitrary formula with only <math>x</math> as free variable. We now define <math>\chi (x)</math> as <math>\exists y (\delta(x,y) \land \psi(y))</math>, and let <math>\varphi

</math> be <math>\chi (\ulcorner \chi \urcorner)</math>. Then the following equivalences are provable in <math>T</math>:

<math>\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) </math>.

Some GeneralizationsEdit

There are various generalizations of the Diagonal Lemma. We present only three of them; in particular, combinations of the below generalizations yield new generalizations.<ref>See Smoryński 2022, Sec. 3 or Hájek and Pudlák 2016, III.2.a</ref> Let <math>T</math> be a first-order theory containing <math>\mathsf{Q}</math> (Robinson arithmetic).

Diagonal Lemma with ParametersEdit

Let <math>\psi (x, y_1, \dots , y_n) </math> be any formula with free variables <math>x, y_1, \dots , y_n</math>.

Then there is a formula <math>\varphi (y_1, \dots y_n)</math> with free variables <math>y_1, \dots , y_n </math> s.t. <math>T \vdash \varphi (y_1 , \dots , y_n) \leftrightarrow \psi (\ulcorner \varphi (y_1 , \dots , y_n) \urcorner, y_1 , \dots , y_n)</math>.

Uniform Diagonal LemmaEdit

Let <math>\psi (x, y_1, \dots , y_n) </math> be any formula with free variables <math>x, y_1, \dots , y_n</math>.

Then there is a formula <math>\varphi (y_1, \dots y_n)</math> with free variables <math>y_1, \dots , y_n </math> s.t. for all <math>m_1 , \dots , m_n \in \mathbb{N} </math>, <math>T \vdash \varphi (\overline{m_1} , \dots , \overline{m_n}) \leftrightarrow \psi (\ulcorner \varphi (\overline{m_1} , \dots , \overline{m_n}) \urcorner, \overline{m_1} , \dots , \overline{m_n}) </math>.

Simultaneous Diagonal LemmaEdit

Let <math>\psi_1 (x_1 , x_2)</math> and <math>\psi_2 (x_1 , x_2) </math> be formulae with free variable <math>x_1</math> and <math>x_2</math>.

Then there are sentence <math>\varphi_1</math> and <math>\varphi_2 </math> s.t. <math>T \vdash \varphi_1 \leftrightarrow \psi_1(\ulcorner \varphi_1 \urcorner, \ulcorner \varphi_2 \urcorner)</math> and <math>T \vdash \varphi_2 \leftrightarrow \psi_2(\ulcorner \varphi_1 \urcorner, \ulcorner \varphi_2 \urcorner)</math>.

The case with <math>n</math> many formulae is similar.

HistoryEdit

The lemma is called "diagonal" because it bears some resemblance to Cantor's diagonal argument.<ref>See, for example, Gaifman (2006).</ref> 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 <math>\psi (x)</math> with <math>x</math> as free variable (in a sufficiently expressive language), then there exists a sentence <math>\varphi</math> such that <math>\varphi \leftrightarrow \psi(\ulcorner \varphi \urcorner)</math> is true (in some standard model).<ref>See Carnap, 1934, and Gödel, 1986, p. 363, fn 23.</ref> Carnap's work was phrased in terms of truth rather than provability (i.e. semantically rather than syntactically).<ref>See Smoryński 2022, Sec. 3.</ref> 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, and their respective proofs are similar.<ref>See Gaifman, 2006 or Smoryński 2022, Sec. 3.</ref> 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.<ref>See Smoryński 2022, Sec. 3.</ref>

See alsoEdit

NotesEdit

Template:Reflist

ReferencesEdit

Retrieved from "https://zalansite.site/mediawiki/index.php?title=Diagonal_lemma&oldid=221966"