Derivation of the Axiom of Choice from the axioms of Zermelo-Fraenkel set theory

Charles Michael Fox

This paper shows that the Axiom of Choice (AC) can be very simply derived from the axioms of Zermelo-Fraenkel set theory (ZF), despite the supposed proof by Paul Cohen that, if the set of axioms of ZF is consistent, AC is not entailed by, so cannot be proven (by correct rules of inference) from, those axioms.

Keywords: foundations of mathematics, logic, set theory, Axiom of Choice, Zermelo-Fraenkel, Paul Cohen AMS-MSC codes: 00A30, 03A05, 03B30, 03E25, 03E30, 03E35

Introduction

Derivation of AC in ZF

The derivation of AC from the axioms of ZF ([1], [2], [3], [4], [5], [6] 1.3, [7] p.1, [10] pp. 51-4), with the justifying axioms of ZF or other justifications listed to the right of the steps of the derivation, is as follows:

(1) Suppose that set S ≠ Φ & ∀(X ∈ S)(X ≠ Φ), | This is the hypothesis of AC.

i.e., (∃X ∈ S) & ∀(X ∈ S)(∃x ∈ X). | ("Φ"represents the empty set.)

(2) ∃[V ≡ (∪X| X ∈ S) & W ≡ S∪V]. | By (1), the Axiom of Union, & the Axiom of Pairs

(3) ∃P ≡ p(p(W)∪W)∪W. | By (2), the Power Set Axiom, the Axiom of Pairs, & the Axiom of Union

| ("p(Y)" represents the power set of Y, i.e., the set of all subsets of Y.)

(4) ∀(X ∈ S)(∃{X,X} = {X}). | By the Axiom of Pairs & the Axiom of Extensionality

(5) ∀(X,Y ∈ P)[∃({{X}, {X,Y}} ≡ (X,Y))]. | By (4), the Axiom of Pairs, & the definition, (X,Y) ≡ {{X}, {X,Y}}, of the ordered pair symbol "(X,Y)"

(6) ∃ a predicate Ψ with domain S×V: | S×V ≡ {(X,v)| X ∈ S, v ∈ V} ∈ P.

∀(X ∈ S)[(∃x ∈ X) & | By (1)

∀(v ∈ V)(Ψ(X,v) ⇔ (v = x))]. | Ψ exists by the rules of first-order logic.

(7) ∃f ≡ {(X,v)| (X,v) ∈ S×V ∧ Ψ(X,v)}. | By the Specification Axiom Schema

(8) f = {(X,x)| (X ∈ S) & (x ≡ f(X) ∈ X)}. ◻ | By (6) & (7)

f is a choice function for S which has been shown to exist using just the axioms of ZF and first-order logic, so it has been shown in ZF that a choice function exists for any non-empty set of non-empty sets, so AC has been proven in ZF.

The rest of the paper consists of five sections which counter various objections which have been or might be made to the above, give arguments positively supporting it, or indicate its importance.

Section 1

Satisfaction of the requirements for using the Specification Axiom Schema, an objection that the derivation

uses AC, and a few comments on the basics of formal proofs and further objections to my proof/derivation

The only sentences in the above proof which seem significantly likely to be criticized by any capable logician or mathematician are (6) and (7). There are three possible issues:

The first is whether there is satisfaction of the two requirements for using the Specification Axiom Schema to show the existence of f. To help make clear that those requirements have been satisfied, I now state that Ψ is the predicate which designates the elements of f, and S×V is a set which all the elements of f are members of, which satisfies the other requirement of Specification. Of course, the (X,x), Ψ, and f, for the general case considered by AC, are merely known to exist, they can’t be known explicitly (on the basis of--in terms of--what is known about S).

The second possible issue is the question of the definition of the “(X,x))” in order to define “Ψ” in terms of them (“define” in the sense of “specify the values of”, not “give the meaning of”). It has been objected that if I say “I will simply define '(X,x)', for all X∈S, as one of those pairs that exists”, then I’ve just used AC. The short but correct answer to this is that in my derivation I don’t try to or claim to define the “(X,x)”, in order to define “Ψ”, in order to define "f”, rather I just show, using the hypothesis of AC, that the (X,x) exist, in order to show that Ψ exists by defining it in terms of them and S×V, in order to show that f exists, which last is all that AC states. AC itself can’t be used to define the “(X,x)”, or to show that such a definition (in terms of S) exists.

Finally, several people, including some logic journal editors, have objected that some early step in this or previous versions of my derivation/proof is essentially equivalent to AC, the conclusion of the proof, so the proof is invalid. Indeed, the hypothesis, step (1) of my proof, which by the rules of formal proof is allowed to be asserted without justification at any stage of the proof, suffers from this fault, unless it is guilty of a presumably even greater sin, of being even stronger than the conclusion, i.e., logically implying it but not being logically implied by it. That the hypothesis logically implies the conclusion, however, is necessary for the proof to be correct and the theorem to be valid, i.e., for the conclusion to be true in all models of the hypothesis. The trick is to show this logical implication by steps which follow from previous ones, or are part of the hypothesis, by use of the axioms and rules of inference of the theory (which, for ZF, are generally believed to be obviously analytically true, on the basis of the meanings of the terms involved in them, in the usual interpretation of the symbols of those axioms and rules). If the steps satisfy this requirement, the proof is a correct, clearly valid proof; if they don't, it isn't.

Step (6), which states the existence of the predicate Ψ and defines it in terms of previously-shown-to-exist things, and which is used to show the existence of the set f , the choice function, in the next step, is the critical step in my proof, and the one which has received the least obviously incorrect criticisms. Specification, which is used in (7) to show the existence of f, is an axiom of ZF used to show the existence of some set A, in my case f, using a predicate which specifies what the elements of A are, together with the fact that all those elements are members of some other (already known to exist) set B (to block Russell's paradox and other similar logical/set-theoretic paradoxes). Specification does not require that the definition of the predicate use only terms which have been previously shown to exist in the set A- to do so would be to give a method of showing the existence of A which required one previously to have shown the existence of A. The criticisms of (6) which I have received so far have all been objections that the definition of Ψ assumes AC, without, however, specifying how the definition does that. As my argument above demonstrates, even though such a demonstration isn't actually necessary, since the proof is correct as it stands, (6) follows from previous steps by the rules of formal proof, and that statement, of course, isn't shown to be false by the fact that (6) leads to (7) and (8), the statements of AC.

Section 2

A defective but basically correct argument in Hrbacek & Jech showing AC for finite |S|

Theorem 1.2, Ch. 8, p. 139, of [6], which is AC restricted to finite sets S of sets, except for not requiring S or its elements to be non-empty, supposedly is proved by induction on the cardinality |S| of S. The supposed induction on |S|, which is said to be possible only because |S| is finite, is both totally inessential and almost totally useless for the proof, and is incorrectly carried out to boot. The proof proceeds about as mine above (without, however, explicit appeal or adherence to the axioms of ZF), except for being restricted to finite S and needlessly using, or claiming to use, induction on |S|.

[6]’s proof assumes that every system with n elements has a choice function, and lets |S|= n+1. It next says to fix X∈S; the set S - {X} has n elements and, consequently, a choice function gx. If X ≠ Φ, then gx = gx U {(X,x)} is a choice function for S (for any x ∈ X). (It also considers the case X = Φ, and claims in that case gx U {(X,Φ)} is a choice function for S, which of course it isn’t, since in that case Φ ∉ X ; Φ is a subset, but not an element, of X. In addition, it fails to establish the existence of a choice function for |S| = 0, 1, or any other |S| without assuming its existence for an S of smaller cardinality, which is one of the two requirements for an induction from n to n+1 to prove the assertion for all finite n.)

The proof says to choose (fix) X, without specifying it other than by X ∈ S, then, in the non-empty X case, to choose x∈X, without otherwise specifying x. Neither choice depends on the existence of a gx for S - {X}. The only place where the induction hypothesis, that AC has been established for |S| = n, and so a gx exists for S - {X}, is supposedly used is in showing, from the existence of gx and {(X,x)}, the existence of the choice function gx for S. However, just as the choice of x ∈ X in no way depends on the existence of a choice function gx for S- {X) (the induction hypothesis), if an x ∈ X can be chosen as the proof says it can, so can an x ∈ X for each of the X ∈ S - {X} be similarly shown to exist without invoking that induction hypothesis, and in fact was so shown, since the induction hypothesis wasn’t used to show the existence of any of the x’s, so an x ∈ X could have been shown to exist for each of the X ∈ S without that hypothesis, so a gx = {(X,x)| X ∈ S}, a choice function for S, could have been shown to exist without any induction. This [6]’s proof, which without the induction is essentially the same as mine above except for the assembling of the (X,x)'s into a function f in my steps (6) and (7), thus doesn’t depend on, or can be simply altered so as not to depend on, any induction, and further, to work for any S, regardless of what |S| is, as my somewhat more careful proof does with the addition of those 2 steps.

I have seen several claims, in addition to those in [6], that AC for finite index sets has been proven in ZF, but cannot be proven in general there. I cannot be certain that these claims all were referring, for the proof of AC for finite index sets, to the proof in [6], although one did refer explicitly to that proof, but none have referred explicitly to any proof other than that in [6]. As far as I know, [6] is a reputable text in set theory, and its authors reputable mathematicians, despite their basically correct but slipshod proof of Thm. 1.2, and their statement that there is no proof in ZF of AC for cases with infinite S.

Section 3

Two questions/arguments for critics

Suppose that S contained one and only one element, namely non-empty X. Would there be any doubt that the existence (not specification, i.e., definition, on the basis of S) of a choice function f ≡ {(X,x)} for S, with only x ∈ X known about x, could be shown in ZF? What, then, prevents the passage to: The existence of a choice function f for arbitrary sets S can be shown in ZF?

If it is necessary to specify or define the choice function f to show its existence (its existence is all that AC claims), why then is it not necessary to specify or define each X (i.e., somehow give its elements), and each x ∈ X, in the hypothesis of AC, to be able to state that they exist? If that were indeed necessary, and each X and x ∈ X were specified or defined in the hypothesis, then that specification or definition could be used to actually specify or define (in ZF) a choice function f, thus satisfying the demands of the critics of such proofs as mine that a choice function f must be defined in order to be shown to exist.

Current mathematics contains a large number of proofs that show the existence of mathematical objects without defining those objects. A famous example is Brouwer's proof of his own Fixed-Point Theorem. His proof shows the existence of a fixed point without specifying that point or giving any method for finding it. Intuitionism, which Brouwer founded, insists that no such non-constructive existence proof is valid. Brouwer spent a considerable part of the rest of his life vainly trying to find a constructive proof for his theorem, but most mathematicians find his non-constructive existence proof entirely acceptable.

Section 4

Paul Cohen’s contrary proof

I haven’t studied all of the supposed proof by Paul Cohen ([8], [9], [10]) that AC is not provable in, or even entailed by, ZF, much less pinpointed this supposed proof’s error(s), which must exist unless there is a formal error in my derivation above, or a basic inconsistency (shudder!) in the logical foundations upon which one of our derivations is based. His supposed proof was said by Cohen to have been done by constructing, or showing that there exists, assuming ZF is consistent, a model of ZF in which AC is not true. ([8], [9], and [10] are devoted mainly to what Cohen calls a proof that the Continuum Hypothesis is not entailed by the axioms of ZF + AC, but along the way he gives what he claims to be a proof that AC is not entailed by the axioms of ZF.) Cohen’s “proof” involves a technique termed “forcing”, which he introduced, said by him to be a delicate technique. Use of such a technique might have led to an error that resulted in an invalid argument, even when used by a good logician, and overlooked by the rest of the logical community in a complex argument such as Cohen’s. My argument, by contrast, is extremely simple and transparent. I have been told that many people have erroneously claimed to have proved AC in ZF. How their claimed proofs differed from mine I don’t know. Maybe some didn’t differ, and so were valid, but were not seriously examined by professional logicians because of the prestige of Cohen and his supposed proof.

Section 5

The importance of this paper's proof

It has been said that AC is obviously true, and (almost) everyone believes it, so it doesn't really matter whether it can be proven in ZF. This claim is untrue for at least three reasons:

1. Many people actually think AC is not true, or at least tend to doubt it, because of the counter-intuitive statements that it is equivalent to or implies, in conjunction with ZF, even though they accept ZF itself. Assuming ZF, AC is equivalent to the Well-ordering Theorem, which on its face is as obviously false as AC is obviously true. Even worse, ZF + AC implies the Banach-Tarski Paradox, which violates most peoples' intuitions about measure, and even basic Euclidean Geometry. If my proof is correct, rejecting either the Well-ordering Theorem or the Banach-Tarski Paradox requires also rejecting at least part of ZF.

2. Much research has been done on an alternative to AC, the Axiom of Determinacy (AD), which is usually paired with ZF. Assuming ZF, AD is inconsistent with AC. Therefore, if my proof is correct, AD is inconsistent with ZF.

3. If my proof is correct, Paul Cohen's claimed proof that AC can't be derived from ZF is incorrect, and the culprit in his supposed proof is likely to be either his forcing technique itself, or some error in his application of it. I understand that his forcing technique, since he introduced it, has been used by many mathematicians in some of their own foundational set-theoretic supposed proofs. If the basic scheme of the forcing technique contains a logical error, these other supposed proofs would also be incorrect, and some perhaps irreparably so.

REFERENCES

1. The Stanford Encyclopedia of Philosophy, “Zermelo-Fraenkel Set Theory”. https://plato.stanford.edu/entries/set-theory/ZF.html Last accessed 2018/6/7

2. WikipediA, “Zermelo-Fraenkel set theory”. https://simple.wikipedia.org/wiki/Zermelo%E2%80%93Fraenkel_set_theory Last accessed 2018/6/7

3. WikipediA, “Zermelo-Fraenkel set theory”. https://en.wikipedia.org/wiki/Zermelo%E2%80%93Fraenkel_set_theory Last accessed 2018/6/7

4. Wolfram MathWorld, “Zermelo-Fraenkel Axioms”. http://mathworld.wolfram.com/Zermelo-FraenkelAxioms.html Last accessed 2018/6/7

5. Encyclopedia of Mathematics, “ZFC”. https://wwww.encyclopediaofmath.org/index.php/ZFC Last accessed 2018/6/7

6. Hrbacek, Karel & Thomas Jech. Introduction to Set Theory, Third Edition. Boca Raton, FL: CRC Press, 1999.

7. Jech, Thomas. Set Theory. New York: Academic Press, 1978.

8. Cohen, Paul J. “THE INDEPENDENCE OF THE CONTINUUM HYPOTHESIS.” Proceedings of the National Academy of Sciences of the United States of America 50.6 (1963): 1143-1148. Print. Also https://www.ncbi.nlm.nih.gov/pmc/articles/PMC221287 Last accessed 2018/10/9

9. Cohen, Paul J. “THE INDEPENDENCE OF THE CONTINUUM HYPOTHESIS, II.” Proceedings of the National Academy of Sciences of the United States of America 51.1 (1964): 105-110. Print. Also https://www.ncbi.nlm.nih.gov/pmc/articles/PMC300611 Last accessed 2018/10/9

10. Cohen, Paul J. Set Theory and the Continuum Hypothesis. Mineola, New York: Dover Publications, 1966, 2008.