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 $\varphi _{e}\simeq \varphi _{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(\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).