Pi-one formula modulo ZF
= Pi-one formula modulo ZF
{title2=$\Pi_1^{\mathrm{ZF}}$}
= Pi-one formulas modulo ZF
{synonym}
A <first-order formula> is $\Pi_1^{\mathrm{ZF}}$ if <ZF> proves it equivalent, with the same free variables, to a universal unbounded quantifier block followed by a <bounded formula in set theory>. Bounded quantifiers do not increase its level in the <Lévy hierarchy>. Such properties are downward absolute between appropriate <transitive models> of <ZF>.