Arithmetic truth is not arithmetically definable

The syntactic diagonal lemma: For every formula $\psi (v)$ with no other free variables in an effective signature extending arithmetic, there is a sentence $\theta$ such that Q in that signature proves $\theta \leftrightarrow \psi (<mi\; mathvariant="normal">⌜</mi>\theta <mi\; mathvariant="normal">⌝</mi>)$. The construction is effective and requires neither consistency nor soundness.

Robinson arithmetic, PA, and numeral conventions: Use the arithmetic signature $0,S,+,\cdot ,=$. Robinson arithmetic $Q$ consists of the universal closures of these seven formulas:

$Sx\mathrm{\ne }0;Sx=Sy\to x=y;x\mathrm{\ne }0\to \mathrm{\exists }yx=Sy;$ $x+0=x;x+Sy=S(x+y);x\cdot 0=0;x\cdot Sy=x\cdot y+x\mathrm{.}$

PA adds, for every formula $\varphi (x,\bar{z})$, the universal closure of $[\varphi (0,\bar{z})\wedge \mathrm{\forall }x(\varphi (x,\bar{z})\to \varphi (Sx,\bar{z}))]\to \mathrm{\forall }x\varphi (x,\bar{z})$. Parameters $\bar{z}$ are allowed. No induction schema is included in $Q$.

For an external natural number $n$, its numeral is the term $\bar{n}=S^{n}0$. Define $x\le y$ by $\mathrm{\exists }z(z+x=y)$ and $x<y$ by $x\le y\wedge x\mathrm{\ne }y$, with $z$ fresh. The left-addend witness is intentional: commutativity is not an axiom of Q.

Use def-set-coded-formal-derivation for the six logical schemes and three rules. Negation, conjunction and existential quantification are primitive: $A\to B$ expands to $\mathrm{\neg }(A\wedge \mathrm{\neg }B)$, $A\vee B$ to $\mathrm{\neg }(\mathrm{\neg }A\wedge \mathrm{\neg }B)$, and $\mathrm{\forall }xA$ to $\mathrm{\neg }\mathrm{\exists }x\mathrm{\neg }A$. Inequality means negated equality. Substitute capture-free, always taking the least available fresh variable index and universally closing the remaining parameters in increasing index order. Thus each displayed axiom and each induction instance is a definite finite sentence.

Soundness for arbitrary set signatures: In ZF, for any set signature and sentence theory $T$, if $T⊢\varphi$, every nonempty set structure satisfying $T$ satisfies $\varphi$ under every assignment. Consequently a theory with a model is consistent.