Past exam of the model theory and Gödel's incompleteness theorems course of the University of Oxford / 2007 / A / 2 / d

Let $d(n)$ be the Gödel number of the diagonal first-order sentence obtained by substituting $\bar{n}$ into the one-free-variable logical formula with code $n$, with an arbitrary default value on noncodes. By the assumptions and (c), this total function has a strong defining logical formula $D(x,y)$.

For the specified $F$, form the one-variable logical formulaLet $h$ be the Gödel number of $H$ and put $C=H(\bar{h})$. Then $d(h)=┌C┐$. Strong definability of a numerical function at this particular standard input givesSubstitution into the existential definition yieldsThe permitted equivalence between the source's two substitution notations identifies this with its requested fixed point. Bound variables are renamed when necessary before forming $H$, so the substitution is capture-free. This constructs one particular first-order sentence from the code of the logical formula which applies $F$ to its own diagonal output.