The syntactic diagonal lemma

By F1 define d(e) to be the code obtained by substituting the numeral of e in the designated free variable of formula e, with a fixed default for invalid inputs. It is primitive recursive. F2 supplies a formula D(x,y) numeralwise representing d uniquely in Q. Choose auxiliary y fresh from psi and from the designated variable x.

Let $\eta (x)=\mathrm{\exists }y(D(x,y)\wedge \psi (y))$, $e=\mathrm{\#}\eta$ and $\theta =\eta (\bar{e})$. By definition of d, $d(e)=\mathrm{\#}\eta (\bar{e})=\mathrm{\#}\theta$. Thus Q proves $\mathrm{\forall }y(D(\bar{e},y)\leftrightarrow y=<mi\; mathvariant="normal">⌜</mi>\theta <mi\; mathvariant="normal">⌝</mi>)$ by F2. The code e is a natural number; its numeral is the term used in theta.

From theta a witness y satisfies D and psi; the uniqueness equation in step 2.1 gives $y=<mi\; mathvariant="normal">⌜</mi>\theta <mi\; mathvariant="normal">⌝</mi>$, hence $\psi (<mi\; mathvariant="normal">⌜</mi>\theta <mi\; mathvariant="normal">⌝</mi>)$. Conversely D holds at that numeral by the same equation; conjoin it with psi at that numeral and introduce the existential to obtain theta. All replacements use fresh variables and licensed equality substitution. These finite syntactic operations prove the biconditional in Q effectively.