= Solution
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 formula>
$$
H(x)=\exists y\,(D(x,y)\wedge F(y)).
$$
Let $h$ be the <Gödel number> of $H$ and put $C=H(\bar h)$. Then $d(h)=\ulcorner C\urcorner$. <Strong definability of a numerical function> at this particular standard input gives
$$
S\vdash\forall y\,[D(\bar h,y)\leftrightarrow y=\overline{\ulcorner C\urcorner}].
$$
Substitution into the existential definition yields
$$
\boxed{S\vdash C\leftrightarrow F(\overline{\ulcorner C\urcorner}).}
$$
The 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.
Back to article page
