ZF-equivalent bounded formula (source code)

= ZF-equivalent bounded formula
{c}
{title2=$\Delta_0^{\mathrm{ZF}}$}

= Delta-zero formula modulo ZF
{synonym}

A <first-order formula> is ZF-equivalent bounded if <ZF> proves it equivalent, with the same free variables, to a syntactically <bounded formula in set theory>. It need not itself have only bounded quantifiers. Between <transitive models> of <ZF>, use the bounded equivalent and the axioms in each model to prove <set-theoretic absoluteness>. The syntactic bounded-formula result requires only transitivity; the provable-equivalence extension additionally requires the theory used for the equivalence.