Solution (source code)

= Solution

A <bounded formula in set theory>, or $\Sigma_0$ formula in the <Lévy hierarchy>, uses only <bounded quantifiers> $\exists u\in v$ and $\forall u\in v$, with the usual Boolean connectives. A <Sigma-one formula in set theory> has the form
$$
\exists u_1\cdots\exists u_m\,\theta(\mathbf u,\mathbf x),
$$
where $\theta$ is a <bounded formula in set theory>; harmless logically equivalent rearrangements are allowed. A <Pi-one formula in set theory> is defined with a universal unbounded block instead.

A <Delta-one formula modulo ZF> is a <first-order formula> $\varphi(\mathbf x)$ for which there are such $\Sigma_1$ and $\Pi_1$ formulas $\sigma,\pi$ with
$$
\boxed{\mathrm{ZF}\vdash\forall\mathbf x\,(\varphi\leftrightarrow\sigma),\qquad\mathrm{ZF}\vdash\forall\mathbf x\,(\varphi\leftrightarrow\pi).}
$$
Equivalently, both $\varphi$ and $\neg\varphi$ have <Sigma-one formulas in set theory> provably equivalent to them in <ZF>. These are levels of the <Lévy hierarchy>, with bounds by sets.