V has a definable truth predicate

Given: Work in ZF unless the statement explicitly weakens or supplements it; fix the objects and hypotheses of the statement.

Set satisfaction and relativization must be distinguished. Set satisfaction is uniform in the code of a formula and the data of a set structure. Relativization to a definable proper class supplies an ambient formula separately for each fixed input formula. Writing $V\models \varphi (\vec{a})$ in this latter sense merely abbreviates $\varphi (\vec{a})$. For the truth-with-parameters interface, a proposed pure membership formula $T(w,x,y,z)$ and a set parameter $t$ would have to satisfy, for every pure membership formula $\psi$ with free variables among $x,y$ and all sets $r,s$, the biconditional $\psi (r,s)\leftrightarrow T(<mi\; mathvariant="normal">⌜</mi>\psi <mi\; mathvariant="normal">⌝</mi>,r,s,t)$. Here $<mi\; mathvariant="normal">⌜</mi>\psi <mi\; mathvariant="normal">⌝</mi>$ is its finite set code. This is a scheme of requirements, not a single first-order assertion quantifying over ambient truths. The companion refutation tests this exact scheme by one formula built from the proposed $T$. No sentence-only arithmetized diagonal lemma or representability theorem is asserted here. Conventions and prerequisites: thm-relativization-and-set-satisfaction. (Set truth and the Tarski interface)

There is a canonical total capture-avoiding substitution $\varphi ⟨t\mathrm{/}x⟩$ on formulas, obtained by renaming obstructing binders using least unused variable indices. It replaces the original free occurrences of $x$ and satisfies $\mathcal{M},s\models \varphi ⟨t\mathrm{/}x⟩⟺\mathcal{M},s[x:=\mathrm{⟦}t{\mathrm{⟧}}_s]\models \varphi \mathrm{.}$ Canonicity refers to the specified coding and traversal, not to literal invariance under other fresh-variable conventions. (Canonical capture-avoiding substitution)