In Hilbert’s original formulation, for any property we can form a term such that
\exists x.P(x) \;\Rightarrow\; P\big(\varepsilon x.P(x)\big).
It should be noted that Hilbert and Bourbaki take the -operator, called in “Theory of Sets” to be a primitive symbol in a mathematical theory. This has the advantage of also allowing the existential and universal quantifiers to be constructed explicitly, since translates to . The intuitive meaning behind the operator is that it returns a distinguished object for which the proposition is true, or if no such object exists, it returns any object for which it is not true. Of course, the intuitive meaning can be misleading since the properties of the epsilon operator are governed by the axiom schema of existence and -extensionality, without which, the symbol has no meaning. The axiom scheme of existence is a statement of Hilbert’s axiom that avoids mention of the existential quantifier.
A wonderful usage of the global choice operator in Bourbaki is that we can easily show that paradoxical sets do not exist, since the definition of a set is given in terms of whether or not the relation defining the set is collectivizing. The example of Russel’s paradox is computed in (Theory of Sets, Chapter II, §1, no.4). A consequence of this formulation is that the epsilon calculus is quantifier-free, since subsumes their roles from the predicate calculus. If we adjoin to intuitionistic logic with the axiom scheme of existence, we obtain a non-conservative extension of intuitionistic logic in which the law of excluded middle still does not hold. However, the assumption of the axiom scheme of -extensionality implies the axiom of global choice and therefore the law of excluded middle.
One use of the choice operator is to eliminate undesirable details of implementation. For example, if is “ is a Dedekind-complete totally ordered field,” then we can define “the real numbers” to be . Any of the numerous constructions of the real numbers can then be used to show that there exists an such that , after which point we can discard whichever explicit construction and work only with . This way we can no longer assert that real numbers (elements of ) are Dedekind cuts, or equivalence classes of Cauchy sequences, or anything in particular, since the axioms provide no rules about how must be chosen other than that it must satisfy . So might consist of Cauchy sequences, or Dedekind cuts, or any other way to construct the reals, but we have no way of knowing, and thus we cannot make use of any such definition in a proof about ; we are forced to use only its formal properties.
In many cases, the assumption of a global choice operator implies the axiom of choice, since for any family of inhabited sets, a choice function is given by . In fact, in the form given above it often implies the stronger global axiom of choice, which applies to proper classes as well as sets.
“Here, moreover, we come upon a very remarkable circumstance, namely, that all of these transfinite axioms are derivable from a single axiom, one that also contains the core of one of the most attacked axioms in the literature of mathematics, namely, the axiom of choice: , where is the transfinite logical choice function.”
—Hilbert (1925), “On the Infinite”, excerpted in Jean van Heijenoort, From Frege to Gödel, p. 382.
However, in some foundations it seems to be possible to avoid this conclusion (if it is unwanted) by not requiring the choice operator to be extensional, i.e. it may not be the case that implies .
Mike Shulman: Is there a formal statement in some formal system along the lines of “a non-extensional choice operator does not imply AC”?
Toby: I don't know about a formal statement, but I can give you an example.
Recall: In Per Martin-Löf's Intuitionistic Type Theory (and many other systems along similar lines), the basic notion axiomatised is not really that of a set (even though it might be called ‘set’) but instead a preset (or ‘type’). Often one hears that the axiom of choice does hold in these systems, which doesn't imply classical logic due to a lack of quotient (pre)sets. However, if we define a set to be a preset equipped with an equivalence predicate, then the axiom of choice fails (although we have COSHEP if presets come with an identity predicate).
A lot of these systems (including Martin-Löf's) use ‘propositions as types’, in which is represented as , which comes equipped with an operation . That is not going to get us our choice operator, but since a choice operator is constructively questionable anyway, then let's throw in excluded middle. This is known to not imply choice, but we do have, for every preset , an element of , that is of . It's not literally true that is of type , of course, but that would be unreasonable in a structural theory; what we do have is a fixed such that, if is inhabited, then for some (necessarily unique) of type (where is the natural inclusion ), which I think should be considered good enough. This is for presets (types), but every set has a type of elements, so that gets us our operator.
How is this nonextensional? We do have if (which is a meaningful statement to Martin-Löf, albeit not a proposition exactly), but if and are given as subsets of some , then we may well have as subsets of without in the sense of identity of their underlying (pre)sets. In particular, if is a surjection and and are the preimages of elements and of , then will not imply that , and the proof of the axiom of choice does not go through. It will go through if and are identical, that is if in the underlying preset of , so again we do get choice for presets (again), but not for sets.
I'm not certain that a nonextensional global choice operator won't imply excluded middle in some other way, but I don't see how it would. You'd want to do something with the idea that always exists but belongs to if and only if is inhabited, but I don't see how to parse it (just by assuming that it exists) to decide the question.
Mike Shulman: That’s a very nice explanation/example, and it did help me to understand better what’s going on; thanks! (Did you mean to say “excluded middle” and not “AC” in your final paragraph?) What I would really like, though, is a statement like “the addition of a nonextensional global choice operator to ____ set theory is conservative” (i.e. doesn’t enable the proving of any new theorems that doen’t refer explicitly to the choice operator). Of course I am coming from this comment, wondering whether what you suggested really is a way to get a choice operator without implying the axiom of choice.
Toby: Yeah, I really did mean to say ‘excluded middle’; remembering that comment, I assume that the real question is whether the thing is OK for a constructivist. I just argued , and I know the result , so I conclude ; but I don't know for certain. I certainly don't have conservative over , nor with any other theory (other than those that already model , obviously).
Mike Shulman: Where should I look for a proof that doesn’t imply AC?
Toby: I'm not sure, it's part of my folk knowledge now. Probably Michael J. Beeson's Foundations of Constructive Mathematics is the best bet. I'll try to get a look in there myself next week; I can see that it's not exactly obvious, and perhaps my memory is wrong now that I think about it.
Toby: No, I can't get anything at all out of Beeson (or other references) about full AC (for types equipped with equivalence relations) in .
Harry Gindi: I have references for this discussion that should settle the issue at hand:
Bell, J. L., 1993a. ‘Hilbert’s epsilon-operator and classical logic’, Journal of Philosophical Logic, 22:1-18
Bell, J. L., 1993b. ‘Hilbert’s epsilon operator in intuitionistic type theories’, Mathematical Logic Quarterly 39:323-337
Meyer Viol, W., 1995a. ‘A proof-theoretic treatment of assignments’, Bulletin of the IGPL, 3:223-243
Toby: Thanks, Harry! Now I just have to find these journals at the library.
Like the axiom of choice, the existence of a global choice operator is consistent with the other axioms of most foundations. For example, in ZF, the constructible universe (which models , the axiom of constructibility?) admits a natural classical well-ordering of the entire universe, giving rise to a naturally defined global choice operator (namely, = the smallest such that in the global well-ordering).
On the other hand, a global choice operator is inconsistent with the univalence axiom of homotopy type theory. For univalence requires that all operations on the type of types must be natural with respect to equivalences, which no global choice operator can be.
Hilbert’s -Operator, PlanetMath.
See also Hilbert (1927), “The Foundations of Mathematics”, pp. 464–479 in JvH.