# Why do we allow redundant axioms in ZFC?

I learned recently that even though ZFC is often said to have nine axioms, there are only 7 independent axioms (actually, 6 axioms and one axiom schema). These seven axioms are listed here. In summary, the following statements, often listed as axioms, are redundant:

"Axiom" of Empty Set: There exists a set with no elements.

"Axiom" of Pairing: If $$a$$ and $$b$$ are sets, there exists the set $$\{a,b\}.$$

"Axiom" of Specification: If $$A$$ is a set and $$P(x)$$ a proposition for each $$x\in A$$, then $$\{x\in A|P(x)\}$$ is a set.

Most sources I've seen include two of the above redundant axioms, giving a total of nine.

Why do we ever consider these sets of statements to all be axioms if some are redundant?

The answer here cites "convenience" as the reason, but this is nonsense. It would be just as convenient to call the redundant facts "theorems" and cite them as theorems when using them in other proofs. (Unless the "convenient" part is ignoring the proofs that they are redundant. But then it would be just as convenient to call the redundant facts "theorems" and not prove them, and at least that would be more transparent!)

There are some interesting discussions on math.SE, such as here, about the different meanings of "axiom." I can understand the word might have picked up different meanings/connotations in different areas (group axioms simply define a group, whereas set theory axioms declare "self-evident truths" about sets, according to some). But the concept of redundant axioms seems totally incoherent. Didn't several mathematicians spend their whole lives trying to show that Euclid's fifth postulate was redundant so that they could eliminate it from the list? If we accept all nine statements as axioms, why not accept all theorems of set theory as axioms?

• Because the version with "redundant" axioms is easy to learn and understand. – Mauro ALLEGRANZA Jan 14 at 9:26
• Have you taught set theory to students or wrote a textbook on the subject? – Asaf Karagila Jan 14 at 9:29
• One other reason I can think of, is that it makes it more natural to formulate weaker set theories by leaving out some axiom(s) from $\mathsf{ZFC}$. Another reason is probably history: all three of the axioms you state were part of Zermelo's original theory $\mathsf{Z}$. Replacement and foundation were only added later. – Vsotvep Jan 14 at 9:37
• Also, groups are often defined in a language that includes a constant symbol for the identity and an inverse relation. Both are redundant, as they are definable from the group operation. So if you wish to complain about redundancy, you can ask group theorists about that as well. – Asaf Karagila Jan 14 at 10:46
• @WillG People who need to learn it the first time have an easier time if the redundant axioms are included. People who read and understand advanced books on set theory are advanced enough to know it doesn't really matter whether you call them axioms or theorems, so why bother. – Vsotvep Jan 16 at 7:26

There is in fact considerable variation in how the axioms of ZFC are defined. Different authors give different exact statements of several of the axioms. Some authors omit some of the axioms which are redundant.

The point is that for most purposes, we don't care about the individual axioms. We only care about the theory that they generate: that is, which theorems we can prove from the axioms*. That's the main point of a foundation for math: it gives a precisely defined notion of "theorem" that everyone can agree on. So, no one will care if you use a funny version of ZFC which includes some statements as axioms which to you are theorems or omits some of your axioms, as long as it ends up proving the same theorems overall. Assuming you know that certain sets of axioms are equivalent to each other, the reason you would pick one over another is convenience: one may be easier for your audience to understand, for instance, or may just be traditional for historical reasons.

You seem concerned about choosing a foundation for math that involves as few assumptions as possible. That is reasonable, but if you can prove that certain assumptions are equivalent to other assumptions, that means it no longer really matters which of them you use; they have the exact same logical content, just expressed in different ways.

*We also care about there being an algorithm that identifies whether a proof from our axioms is valid. However, this will be true for any remotely reasonable choice of axioms.

• I agree with this statement, but I think this is addressing a different issue from my question. This explains why using different sets of equivalent axioms is standard practice. But my issue is with redundant axioms being used within one and the same theory. – WillG Jan 14 at 23:13
• It just seems to go against the definition of the word "axiom" to include a statement that is provable by other axioms of the same theory, in the same formulation of the theory. – WillG Jan 14 at 23:15
• A set of axioms with a redundant axiom is equivalent to the set of axioms with the redundant axiom removed. So, it doesn't matter which you use. – Eric Wofsey Jan 14 at 23:30
• That's a good point. It just seems so arbitrary as to be grossly inelegant. Why not also include all three of axiom of choice, well-ordering theorem, and Zorn's lemma as axioms? That would be logically equivalent as well. – WillG Jan 14 at 23:37
• In defense of the redundant lists of axioms, I will mention that I would not be surprised if there does not exist any irredundant set of axioms for ZFC. Remember that Separation and Replacement are each actually infinitely many axioms--and certainly any single instance of Replacement can be deduced from the others, for instance. – Eric Wofsey Jan 14 at 23:41