User:IssaRice/Computability and logic/Diagonalization lemma

The diagonalization lemma, also called the Godel-Carnap fixed point theorem, is a fixed point theorem in logic.

Rogers's fixed point theorem

Let $f$ be a total computable function. Then there exists an index $e$ such that $\varphi _{e}\simeq \varphi _{f(e)}$.

(simplified)

Define $d(x)=\varphi _{x}(x)$ (this is actually slightly wrong, but it brings out the analogy better).

Consider the function $f\circ d$. This is partial recursive, so $f\circ d\simeq \varphi _{i}$ for some index $i$.

Now $\varphi _{f(d(i))}\simeq \varphi _{\varphi _{i}(i)}$ since $f\circ d\simeq \varphi _{i}$. This is equivalent to $\varphi _{d(i)}$ by definition of $d$. Thus, we may take $e=d(i)$ to complete the proof.

Diagonalization lemma

(semantic version)

Let $A$ be a formula with one free variable. Then there exists a sentence $G$ such that $G$ iff $A(\ulcorner G\urcorner )$.

Define $\mathrm {diag} (x)$ to be $\ulcorner C(\ulcorner C\urcorner )\urcorner$ where $x=\ulcorner C\urcorner$. In other words, given a number $x$, the function $\mathrm {diag}$ finds the formula with that Godel number, then diagonalizes it (i.e. substitutes the Godel number of the formula into the formula itself), then returns the Godel number of the resulting sentence.

Let $B$ be $A(\mathrm {diag} (x))$, and let $G$ be $B(\ulcorner B\urcorner )$.

Then $G$ is $A(\mathrm {diag} (\ulcorner B\urcorner ))$, by substituting $x=\ulcorner B\urcorner$ in the definition of $B$.

We also have $\mathrm {diag} (\ulcorner B\urcorner )=\ulcorner B(\ulcorner B\urcorner )\urcorner$ by definition of $\mathrm {diag}$. By definition of $G$, this is $\ulcorner G\urcorner$, so we have $\mathrm {diag} (\ulcorner B\urcorner )=\ulcorner G\urcorner$.

To complete the proof, apply $A$ to both sides of the final equality to obtain $A(\mathrm {diag} (\ulcorner B\urcorner ))$ iff $A(\ulcorner G\urcorner )$; this simplifies to $G$ iff $A(\ulcorner G\urcorner )$.

Comparison table

Some things to notice:

• The two theorems are essentially identical, with identical proofs, as seen by the matching rows. The analogy breaks down slightly at the very end, where we apply $\varphi _{f(\cdot )}$ vs $A(\cdot )$ (the latter corresponds to $f$ until the very end).
• In the partial recursive functions world, it's easy to go from the index (e.g. $e$) to the partial function ($\varphi _{e}$). In the formulas world it's the reverse, where it's easy to go from a formula (e.g. $A$) to its Godel number $\ulcorner A\urcorner$).

Step	Rogers's fixed point theorem	Diagonalization lemma
Theorem statement (note: quantifiers are part of the metalanguage)	$(\forall f\exists e)\ \varphi _{e}\simeq \varphi _{f(e)}$	$(\forall A\exists G)\ G\leftrightarrow A(\ulcorner G\urcorner )$
Given mapping	$f$	$A$
Definition of diagonal function	$d(x)=\varphi _{x}(x)$	$\mathrm {diag} (\ulcorner C\urcorner )=\ulcorner C(\ulcorner C\urcorner )\urcorner$
Composition of given mapping with diagonal function ($\mathrm {given} \circ \mathrm {diagonal}$)	$f(d(x))$	$A(\mathrm {diag} (x))$
Naming the $\mathrm {given} \circ \mathrm {diagonal}$ composition	$f\circ d$ (name not given because compositions are easy to express outside a formal language)	$B$
Index of $\mathrm {given} \circ \mathrm {diagonal}$ composition	$i$	$\ulcorner B\urcorner$
Expanding using definition of diagonal	$d(i)=\varphi _{i}(i)$	$\mathrm {diag} (\ulcorner B\urcorner )=\ulcorner B(\ulcorner B\urcorner )\urcorner$
The $\mathrm {given} \circ \mathrm {diagonal}$ composition applied to own index (i.e. diagonalization of the composition)	$f\circ d(i)$	$B(\ulcorner B\urcorner )$
G defined	$\varphi _{i}(i)$ (no equivalent definition)	$G$ is $B(\ulcorner B\urcorner )$
	$f(d(i))=\varphi _{i}(i)$	$A(\mathrm {diag} (\ulcorner B\urcorner ))\leftrightarrow B(\ulcorner B\urcorner )$
Renaming index	$e=d(i)$	$\ulcorner G\urcorner =\mathrm {diag} (\ulcorner B\urcorner )$
Leibniz law to previous row	Apply $\varphi _{f(\cdot )}$ to obtain $\varphi _{f(e)}=\varphi _{f(d(i))}$	Apply $A(\cdot )$ to obtain $A(\ulcorner G\urcorner )\leftrightarrow A(\mathrm {diag} (\ulcorner B\urcorner ))$
Use definition of G	$\varphi _{f(e)}=\varphi _{\varphi _{i}(i)}=\varphi _{e}$	$A(\ulcorner G\urcorner )\leftrightarrow B(\ulcorner B\urcorner )\leftrightarrow G$
(Definition of G)?	$\varphi _{i}(i)$ is $f(d(i))$	$G$ is $A(\mathrm {diag} (\ulcorner B\urcorner ))$