Solution (source code)

= Solution

The <Diagonal lemma> states that for every formula $\theta(x)$ with one free variable there is a sentence $\gamma$ such that
$$
PA^-\vdash\gamma\leftrightarrow\theta(\ulcorner\gamma\urcorner).
$$
The same conclusion holds in every theory extending the arithmetic needed to formalize substitution.