= Solution
A syntactically <bounded formula in set theory> is built from the atomic <first-order formulas> $u=v$ and $u\in v$ using <Boolean operations> and bounded quantifiers $\exists u\in v$ and $\forall u\in v$. These abbreviate $\exists u(u\in v\land\cdots)$ and $\forall u(u\in v\Rightarrow\cdots)$, with $u$ different from the bounding variable $v$.
The superscript in the question allows provable equivalence: a <ZF-equivalent bounded formula> is any <first-order formula> $\varphi(\vec v)$ for which some syntactically <bounded formula in set theory> $\psi(\vec v)$ satisfies
$$
\boxed{\mathsf{ZF}\vdash\forall\vec v\,(\varphi(\vec v)\leftrightarrow\psi(\vec v)).}
$$
Thus $\Delta_0^{\mathrm{ZF}}$ is the class of <first-order formulas> equivalent over <ZF> to a syntactic $\Delta_0$ <first-order formula>. If a convention uses $\Delta_0^{\mathrm{ZF}}$ just for syntactically bounded set-theoretic <first-order formulas>, it is the smaller syntactic class; the subsequent <set-theoretic absoluteness> proof works for both conventions.
Back to article page
