Description: Equivalent of Axiom of Choice. We do not insist that f be a function. However, Theorem ac5 , derived from this one, shows that this form of the axiom does imply that at least one such set f whose existence we assert is in fact a function. Axiom of Choice of TakeutiZaring p. 83.
Takeuti and Zaring call this "weak choice" in contrast to "strong choice" E. F A. z ( z =/= (/) -> ( Fz ) e. z ) , which asserts the existence of a universal choice function but requires second-order quantification on (proper) class variable F and thus cannot be expressed in our first-order formalization. However, it has been shown that ZF plus strong choice is a conservative extension of ZF plus weak choice. See Ulrich Felgner, "Comparison of the axioms of local and universal choice",Fundamenta Mathematica, 71, 43-62 (1971).
Weak choice can be strengthened in a different direction to choose from a collection of proper classes; see ac6s5 . (Contributed by NM, 21-Jul-1996)
Ref | Expression | ||
---|---|---|---|
Assertion | ac4 | |- E. f A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dfac3 | |- ( CHOICE <-> A. x E. f A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) ) |
|
2 | 1 | axaci | |- E. f A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) |