Strong diagonal lemma

Statement

Let $\psi (x)$ be any formula in the language of $T$ with only $x$ as free variable. Then there is a term $t$ in the language of $T$ such that $T \vdash t = \ulcorner \psi (t) \urcorner$.

Trivially, the diagonal lemma follows from the strong diagonal lemma (take $\varphi (x)$ to be $\psi (t)$). Note however that the strong diagonal lemma depends on the language of $T$, particularly on whether there is such a term $t$. Typically, the strong diagonal lemma fails for theories in the basic language of arithmetic (such as $\mathsf{Q}$ or $\mathsf{PA}$), but holds for primitive recursive arithmetic $\mathsf{PRA}$ which has a function symbol for each primitive recursive functions.