= Solution
Use the <Lévy hierarchy>, with <bounded formulas in set theory> as the quantifier-free level for this purpose. Let $\operatorname{Ord}(\kappa)$ be the bounded ordinal predicate, and let $\operatorname{Bij}(f,\alpha,\kappa)$ be the bounded predicate saying that $f$ is a graph of a <bijection> from $\alpha$ onto $\kappa$. Then cardinalhood is expressed by
$$
\boxed{\operatorname{Ord}(\kappa)\ \land\
\forall f\,\forall\alpha\in\kappa\ \neg\operatorname{Bij}(f,\alpha,\kappa).}
$$
All quantifiers in $\operatorname{Ord}$ and $\operatorname{Bij}$ are bounded by the displayed sets and the graph. Ordered-pair membership, graph functionality, injectivity and surjectivity have bounded expansions using the usual set coding of <ordered pairs>. The only unbounded quantifier shown is universal over $f$. The formula is therefore $\Pi_1$ and in particular a <Pi-one formula modulo ZF>.
In <ZF>, a <cardinal number> is an <ordinal> not in bijection with any smaller ordinal, so this formula has exactly the required meaning. Thus <cardinalhood is Pi-one definable>; the argument does not use the <axiom of choice>.
Back to article page
