What is a Choice Principle, really?

Question

This question is quite soft, and I apologize in advance if it borderline off-topic.

When working in theories between ZF and ZFC the term "choice principle" is heard quite often. For example:

$\quad$ The Axiom of Countable Choice: Every countable family of non-empty sets has a choice function.

We can say, if so, that a choice principle is an assertion about choosing. On the other hand, the above axiom is equivalent [1] to the following assertion:

$\quad$ Every $\sigma$-compact space is Lindelöf.

However this statement does not talk about choosing anything. The first alternative is to define a choice principle as something equivalent to a choice-referring statement, but what about the ordering principle?

$\quad$ Ordering Principle: Every set can be linearly ordered.

Commonly thought of as a choice principle, the order principle is not really equivalent to any choice principle directly. It does however prove that every family of non-empty and finite sets has a choice function.

Maybe we can define a choice principle as something which proves some sort of a choice statement. Alas this too can be troublesome, consider the Small Violations of Choice principle:

$\quad$ SVC: There exists $S$ such that for every $x$ there is an ordinal $\alpha$ such that $x\leq\mathcal P(\alpha)\times S$.

It is consistent with the existence of an amorphous set AND a countable set of pairs without a choice function that SVC holds, so it doesn't even imply the axiom of choice for pairs.

So we may wish to define a choice principle as follows:

Let $\varphi$ be a sentence in the language of set theory, $\varphi$ is a choice principle if ZF does not prove $\varphi$, but ZFC does.

This definition catches the wanted properties of a choice principle, it is simply an assertion in between the two theories. However in a recent comment on math.SE Carl Mummert suggested that this definition is also problematic, since the assertion: $$\lnot\rm AC\rightarrow\text{Con}(ZF)$$ Is not provable from ZF, but vacuously true in ZFC.

This leads to the question:

Question: What would be a good definition for Choice Principle (in ZF), which encapsulates the notion of a statement "between" ZF and ZFC, but still avoids vacuous statements as above?

---

Bibliography:

1. Brunner, N. σ-kompakte Räume. (German. English summary) [σ-compact spaces] Manuscripta Math. 38 (1982), no. 3, 375–379.

Answer 1

Here is a way to think about Carl's example, which seems to undercut your interpretation of it as vacuous, and allows us still to think of it as choice principle. Namely, the statement $\neg\text{AC}\to\text{Con}(\text{ZFC})$ is equivalently expressed as: $$\neg\text{Con}(\text{ZFC})\to\text{AC},$$ which says that if a certain number-theoretic principle holds, then we have full choice. I regard this as a choice principle---perhaps one would call it a conditional choice principle---because it asserts the full power of AC, provided a certain requirement is met. This would seem to be a choice principle even in the intensional sense mentioned by Andrej. It asserts that we may make our choices, provided that we first verify that the combinatorial assertion $\neg\text{Con}(\text{ZFC})$ holds. This particular example is a weak choice principle, because ZF plus this axiom, if consistent, is strictly between ZF and ZFC.

There is of course nothing special about $\text{Con}(\text{ZFC})$ here. If $\Phi$ is any statement provable in ZFC, then over ZF it is equivalent to $\neg\text{AC}\to\Phi$, and hence also to $\neg\Phi\to\text{AC}$. Such a form of the principle can be viewed as a conditional assertion of the axiom of choice, even in the intensional sense, since it asserts the full power of AC, providing a certain requirement is met. In this sense, any statement $\Phi$ provable in ZFC and not in ZF, including any of the usual weak choice principles, may be viewed in this way also as a conditional choice principle.

This seems to allow us to retain your proposal that a statement $\varphi$ is a choice principle if it is provable in ZFC, but not in ZF.

Answer 2

When we speak of a "choice principle" we are discussing the meaning of a statement, not its truth value, i.e., the usual statement AC got its name because of what it means and not because of its truth status. However, logical equivalence preserves only truth values but not meanings. Thus the statements "all unicorns have two horns" and "1 + 1 = 2" are both true, hence equivalent, but they have different meanings. Likewise, the axiom of choice and the well-ordering principle have different meanings, even though they are equivalent. If you wonder about AC being equivalent to a well-ordering principle, you should also wonder about many other equivalences in mathematics that relate statements with different meanings.

As for your question "what is a choice principle, really?" I would say that choice principles are a certain kind of reversal of quantifiers. The axiom of choice can be stated as $$(\forall x \in A . \exists y \in B . \phi(x,y)) \implies \exists f \in B^A . \forall x \in A . \phi(x, f(x))$$ where $\phi$ is a relation between the sets $A$ and $B$. This form of the axiom of choice does not require any set theory, just a bit of simple type theory and first-order logic (if you read schematically in $\phi$).

Exercise: convince yourself that the above statement is equivalent to AC. Hint: given a family of sets $C_i$ indexed by $i \in I$ let $A = I$, $B = \bigcup_{i \in I} C_i$ and $\phi(i, x) \iff x \in C_i$. Conversely, given $A$, $B$ and $\phi$, let $I = A$ and $C_i = \lbrace y \in B \mid \phi(i,y)\rbrace$.

A category theorist might say that choice is about splitting epis. Indeed, given a family $C_i$ indexed by $i \in I$, consider the map $e : \coprod_{i \in I} C_i \to I$ defined by $e (i,x) = i$. Then $(C_i)_{i \in I}$ is a family of non-empty sets if, and only if, $e$ is surjective (epi), and it has a choice map if, and only if, $e$ has a right inverse (is split). Conversely, to split an epi $e : A \to B$ is the same as to give a choice function for the family of sets $C_i = \lbrace x \in A \mid e(x) = i\rbrace$ indexed by $i \in B$.

Supplement: in answer to Trevor, here is how one might phrase dependent choice categorically. I do not know whether there is a slicker formulation. Given $1 \to A$ and $e, p: B \to A$ with $e$ epi, there is $f: \mathbb{N} \to A$ such that there is a factorization $h: \mathbb{N} \to B$ of the span $f, f \circ \mathrm{succ} : \mathbb{N} \to A$ through the span $e, p: B \to A$. This looks nicer as a commutative diagram, how do I draw one of those? Anyhow, I do not see a particular advantage over the usual formulation. Perhaps someone can improve this.