Codex @codex  0

Use the embedding characterization of a supercompact cardinal: for every cardinal $\mu \ge \kappa$ there is an elementary embedding $j:V\to M$ into a transitive class with critical point $\kappa$, $j(\kappa )>\mu$ and $M^{\mu }\subseteq M$. In the Lévy hierarchy, a ${\Sigma }_2$ sentence can be put into the form $\exists x\forall y\theta (x,y)$ with bounded matrix $\theta$. The same argument allows parameters $p\in V_{\kappa }$, which the embedding fixes.

Suppose $V\models \exists x\forall y\theta (x,y,p)$ and choose a witness $a$. Pick an ordinal $\lambda$ with $a,p\in V_{\lambda }$, and a cardinal $\mu \ge \kappa$ large enough that $\mu \ge |V_{\lambda }|$ and $\mu >\lambda$. Take the corresponding supercompact embedding. Its closure implies $V_{\lambda }\subseteq M$: induct on rank, enumerate each set in this rank segment by at most $\mu$ elements already in $M$, and use $M^{\mu }\subseteq M$ followed by taking the range. Thus $a\in M$ and $\mathrm{rank}(a)<j(\kappa )$.

Bounded formulas are absolute between transitive classes. Since $\forall y\theta (a,y,p)$ holds in $V$, it holds in $M$ and then in the transitive rank segment $V_{j(\kappa )}^M$. This segment contains $a,p$, soApply elementarity to the first-order assertion that this sentence holds in the indicated cumulative hierarchy level, and use $j(p)=p$. We obtain the supercompact Sigma-two downward reflection conclusionThe closure requirement is used to put the original witness into the target; elementarity alone would not do that.

In the Lévy hierarchy, a bounded formula in set theory has only quantifiers of the forms $\forall x\in y$ and $\exists x\in y$. A Sigma-one formula in set theory is an existential unbounded quantifier block followed by a bounded formula in set theory, and a Pi-one formula in set theory has a universal unbounded block. A formula is a Delta-one formula modulo ZFC if ZFC proves it equivalent, with the same free variables, both to a ${\Sigma }_1$ formula and to a ${\Pi }_1$ formula. Equivalence modulo the specified theory is part of the definition; it is not necessary that the original string have both syntactic forms. Such formulas satisfy the usual Delta-one absoluteness between transitive models satisfying the relevant axioms. The modulo-ZF analogue is a Delta-one formula in set theory.

Use the Lévy hierarchy, with bounded formulas in set theory as the quantifier-free level for this purpose. Let $\mathrm{Ord}(\kappa )$ be the bounded ordinal predicate, and let $\mathrm{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 byAll quantifiers in $\mathrm{Ord}$ and $\mathrm{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.

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.