Use the Lévy hierarchy, with bounded formulas in set theory as the quantifier-free level for this purpose. Let be the bounded ordinal predicate, and let be the bounded predicate saying that is a graph of a bijection from onto . Then cardinalhood is expressed by
All quantifiers in and 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 . The formula is therefore 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.

Articles by others on the same topic (0)

There are currently no matching articles.