User:IssaRice/Computability and logic/Diagonalization lemma

Rogers's fixed point theorem

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

Diagonalization lemma

(semantic version)

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

Define $\mathrm{d}\mathrm{i}\mathrm{a}\mathrm{g}(x)$ to be $⌜C(⌜C⌝)⌝$ where $x=⌜C⌝$. In other words, given a number $x$, the function $\mathrm{d}\mathrm{i}\mathrm{a}\mathrm{g}$ finds the formula with that Godel number, then diagonalizes it (i.e. substitutes the Godel number of the formula into the formula itself).