|
There are many classically equivalent formulations of the axiom of choice, the one I gave is just the one I like best. :) But you are right, the devil is in the details, so let me spell it out precisely: The axiom states that for every set X, there is a function \epsilon : P(X)/{\empty} -> X
If you want to restrict yourself to first-order logic, then you have to encode the function \epsilon (e.g. as a functional relation, where relations are in turn encoded as sets of ordered pairs, which are in turn encoded with Kuratowsky's construction). Set theorists like first-order logic and this encoding overhead is the reason why it's not the standard definition, even though it's arguably what the axiom is trying to express(1,2). Apart from that the statements are (classically) equivalent:To go from the higher-order version to the cartesian product, note that the cartesian product of an I-indexed family of sets is a set of functions f from I to the union of all X_i's, such that f(i) \in X_i for all i. Let (X_i)_{i\in I} be an I-indexed family of sets, all of which are non-empty, then (i -> \epsilon(X_i)) is in the cartesian product of the X_i's, where we use \epsilon for the union of all X_i's. The reason we couldn't build that element without AC is precisely that we have no way of selecting exacly one element from each X_i, even though we know that they are non-empty. In the other direction we can use Zermelo's well-ordering theorem to construct a well-order on X. We define \epsilon to pick out the minimum with respect to this order. (1) This really is what the axiom of choice was meant to express. If you can read German, you can refer to Zermelo's own work: https://eudml.org/doc/158167
Under point 2 in this paper, Zermelo assumes that there is such a choice function on a given set and from this he derives the well-ordering of that set.(2) Another example of the drawbacks of working with a first-order axiomatization is the axiom of regularity. The idea we want to express is that there are no infinitely descending element chains ("every set is well-founded"), but expressing this in first-order logic leads to a convoluted statement which obscures the simple idea... and is also not a correct encoding of this idea in intuitionistic logic! |