Editing Diagonal lemma (section)

== The Diagonal Lemma and its proof ==

<blockquote>'''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>.
</blockquote>

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 [[Gödel's encoding|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>.