Delta-one formula modulo ZF (source code)

= Delta-one formula modulo ZF
{title2=$\Delta_1^{\mathrm{ZF}}$}

= Delta-one formulas modulo ZF
{synonym}

A <first-order formula> is Delta-one modulo <ZF> if that theory proves it equivalent both to a <Sigma-one formula in set theory> and to a <Pi-one formula in set theory>, with the same free variables. Equivalently its assertion and negation each have existential-bounded definitions over <ZF>. A witness gives upward absoluteness for the first definition; the universal form gives downward absoluteness. Thus the formula has <Delta-one absoluteness> between nested <transitive models> of <ZF>.