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.
I like this question very much.
I find the difference between the two readings of $\forall x\exists y\ P(x,y)$ to be similar to the issues often brought up by questions of uniformity in mathematical existence assertions. So this may be a good keyword leading to further discussion. For example, the discussion of uniformity in my answer to the question Can a problem be simultaneously NP and undecidable?.
To explain a little, in the context of computability theory, say, in the ordinary mathematical reading of $\forall x\exists y\ P(x,y)$, there is no reason to think that there should be a computable function mapping each $x$ to such a $y$. But if we assert that the existence claim is uniform, then this means something much closer to the semantics about which you inquire, namely, that there should be a computable function allowing us to pass from $x$ to a witness $y$.
In ZFC set theory, the axiom of choice can be interpreted as the assertion that all existence claims of the form $\forall x\in u\exists y\ P(x,y)$ are uniform, so that there is a function $f$ with domain $u$ so that $P(x,f(x))$ for each $y\in u$. In class theories such as KM, the global axiom of choice is the assertion that all assertions of the form $\forall x\exists y\ P(x,y)$ are uniform, so that there is a class function $F$ with $P(x,F(x))$ for all $x$.
Since the issue of the uniformity of existence assertions is often central in many mathematical domains, I propose that this is the answer to your question.
Best Answer
The following paper by Kurt Maes is focused on a version of the question at hand here, namely, finding an equivalent formulation of AC in the language of set theory using the fewest number of quantifiers, rather than merely the shortest length. In his main result, Maes finds a 5-quantifier assertion equivalent to the axiom of choice. The statement is built on the same statement as in François's answer, but modified to use fewer quantifiers (Maes has five, in comparison with ten for François; but of course François wasn't trying to minimize that quantity).
Maes's result refuted a conjecture of Harvey Friedman, which in the introduction the author mentions was stated on F.O.M., that it would not be possible to state a formulation of the axiom of choice using only five quantifiers.
Please see Maes's solution in his paper.
When I first heard about the Maes result (August 2004, apparently an earlier draft of his paper—I haven't checked the differences), I naturally set myself the task of proving the main result myself, without looking at Maes's argument. I would encourage the same of all of you---before reading further, try to express AC in the language of set theory using only five quantifiers! Here is what I had come up with (retrieved after digging around in my old computer files):
Theorem. AC is equivalent (in ZF) to the following assertion: $$\forall A\exists B\forall a\in A\, \exists x\forall z$$ $$(x \in a \cap B) \wedge (z \in a \cap B \implies z=x) \wedge (a \neq B)$$ $$\text{or }\quad(B \in x) \wedge (x \in A) \wedge (a \neq x)$$ $$\text{or }\quad(B \in A) \wedge (z \notin B).$$
Proof. The point is that in order to get down to only five quantifiers, you have to essentially reuse the quantifiers to cover the various cases. The idea is that clause 1 expresses that $B$ is a selection set for $A$, when $A$ is a family of disjoint nonempty sets (plus something extra useful when $A$ is not like that). Clause 2 expresses that $A$ has elements that are not disjoint (at least two contain $B$). Clause 3 expresses that $A$ contains the emptyset ($B=\emptyset$).
AC easily implies the assertion. If $A$ is a family of disjoint nonempty sets, then we can let $B$ be a selection set for $A$, and verify clause 1. (note: in order to get $(a \neq B)$ in the case that $A$ is a singleton, we can freely add irrelevant elements to $B$ outside of $\bigcup A$.) If $A$ contains non-disjoint sets, we let $B$ be any element which is in at least two elements of $A$, and then we can always be in clause 2, since for any element of $A$ we can find another element of $A$ containing $B$. Finally, if $A$ contains the empty set, we can set $B=\emptyset$, and verify always clause 3.
Conversely, suppose that the stated principle holds. To prove AC, it suffices to construct a selection set for a family $A$ of disjoint non-empty sets. By replacing $A$ if necessary with the isomorphic copy $\{\{w\}\times a\mid a \in A\}$, where $w$ has high rank (such as $w=A$ itself), we may assume that every element of $\bigcup A$ has the same rank. Thus, every element of $A$ has rank one higher than this, and every element of $\bigcup\bigcup A$ has rank lower than this. It follows that no element of $\bigcup A$ is in $A$, and no element of $\bigcup A$ has itself elements in $\bigcup A$.
For such an $A$, we get $B$ by the stated principle. Note now that Clause 2 implies $B \in\bigcup A$, and clause 3 implies $B \in A$. Meanwhile, clause 1 implies both that $B$ has an element in $\bigcup A$ and also that $B$ is not in $A$ (since it implies that $B\cap a$ is nonempty for some other $a\in A$, while sets in $A$ are disjoint). By our assumptions on $A$, these possibilities are mutually exclusive. It follows that $B$ must always be in clause 1, or always in clause 2, or always in clause 3, regardless of $a$, $x$, and $z$. If clause 3 always occurs, then $\emptyset\in A$, a contradiction. If clause 2 always occurs, then $B$ must be in more than one element of $A$, since otherwise we could let $a$ be that element, and this would contradict the disjointness of the elements of $A$. Thus, it must be that clause 1 always occurs. In this case, $B$ is a selection set, and so we have established AC. QED
Although I am not aware of any utility flowing from the fact that AC can be exprssed in this manner, it is nevertheless true that proof theory has sometimes made advances by investigating the resource-limited expressive powers of languages.