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

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.

An infinite cardinal number $\kappa$ is a regular cardinal if every function from an ordinal $\delta <\kappa$ into $\kappa$ has bounded range. Write this as $\forall f\forall \delta \in \kappa (\mathrm{Map}(f,\delta ,\kappa )\Rightarrow \exists \beta \in \kappa \forall \xi \in \delta f(\xi )<\beta )$. The graph predicates are bounded formulas in set theory, and cardinalhood is Pi-one definable, so adding infinite cardinalhood yields a Pi-one formula modulo ZF.

An ordinal $\kappa$ is a cardinal number precisely when no smaller ordinal has a bijection onto it. Ordinalhood and the graph predicate for a bijection are bounded formulas in set theory, so $\mathrm{Ord}(\kappa )\wedge \forall f\forall \alpha \in \kappa \neg \mathrm{Bij}(f,\alpha ,\kappa )$ is a Pi-one formula modulo ZF. This does not assert that every set can be assigned an ordinal cardinal without the axiom of choice.