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:
- Brunner, N. σ-kompakte Räume. (German. English summary) [σ-compact spaces]
Manuscripta Math. 38 (1982), no. 3, 375–379.
Best Answer
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.