Delta-one formula modulo ZF (${\Delta }_1^{\mathrm{ZF}}$)

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.