Is there a strict limit on choice principles in $\sf ZFC$?

Question

Is there a principle $\sf P$ that $\sf ZFC$ [or some suitable extension of it] proves to be a strict limit on choice principles?

By a choice principle I mean a sentence (or scheme) that is equivalent [over $\sf ZF$] to a selection principle. The latter is a sentence of the form:

$\forall x_1,..,\forall x_n \exists F \forall y: \Omega \to F(x_1,..,x_n)(y) \in y$

Where $\Omega$ is a formula, that may use "$x_1,..,x_n,F,y$" among its free variables.

that is not provable in $\sf ZF$ alone.

By $\sf P$ being a strict limit on choice principles, it means that for every choice principle $\sf c$ we have $\sf ZFP \vdash c$, and $\sf ZFc \not \vdash P$; and such that there does not exist any principle $\sf H$ such that: $\sf ZFP \vdash H$, and $\sf ZFH \not \vdash P$, and for every choice principle $\sf c $ we have $\sf ZFH \vdash c$, and $\sf ZFc \not \vdash H$.

Answer 1

The answer is no. Every theorem of ZFC is equivalent to a choice principle. I will prove this is true, but nevertheless also I will be first to agree that the manner in which this is true is trivial and ultimately unsatisfying. I take the real lesson here to be that the property of being a choice principle in this sense is not a useful notion.

Theorem. Every statement provable in ZFC is equivalent over ZF to a choice principle for a definable set family $\Omega$.

Proof. Suppose that $\psi$ is a sentence provable in ZFC. Define the family $\Omega$ so that it is the empty family, in the event that $\psi$ holds, and otherwise it is the family $V_\alpha-\{\emptyset\}$, where $\alpha$ is the least ordinal such that this family has no choice function. (Note that if $\psi$ fails, then AC must fail and so there will indeed be such an ordinal $\alpha$.)

I defined the family $\Omega$ so that ZF proves both that $\psi$ implies $\Omega=\emptyset$, and also that $\neg\psi$ implies that $\Omega=V_\alpha-\{\emptyset\}$, where $\alpha$ is least such that this has no choice function.

Now we argue in ZF. If $\psi$ holds, then the family given by $\Omega$ is empty, and so it vacuously has a choice function. And if $\psi$ does not hold, then AC fails and so indeed there is a first ordinal where the family of nonempty sets of rank below $\alpha$ has no choice function, and $\Omega$ is this family. So in this case, $\Omega$ does not have a choice function.

So the sentence $\psi$ is equivalent over ZF to the existence of a choice function for $\Omega$, as desired. $\Box$

The theorem is meant as a scheme over all $\psi$ that are provable in ZFC. So for each instance of the theorem, $\psi$ is a fixed sentence, and this sentence appears in the definition of the family $\Omega$.