5 added 562 characters in body

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.

4 better opening

There is

When we speak of a difference between "choice principle" we are discussing the meaning of a statementand , 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. Logical 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$.

3 movd splitting of epis to the right place

There is a difference between the meaning of a statement and its truth value. Logical equivalence preserves 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 for 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)}$. 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 = {x \in A \mid e(x) = i}$ indexed by $i \in B$. 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\$.

2 added 173 characters in body
1