# Axiom of Choice — Why is it an axiom and not a theorem?

My question is only indirectly about the axiom of choice, I just happened to come to the question via the axiom of choice and will use it to illustrate my problem.

So far I thought axioms were propositions that were a) asserted to be true and b) consistent with the remaining theory.

Now I read on the axiom of choice, and something feels strange about it. Isn't there a difference between an axioms such as

$$0 \textit{ is a number}$$

$$\textit{if n is a number then s(n) is a number}$$

on the one hand axioms such as

$$\textit{for any relation } R, \textit{ there exists a function } f \textit{ such that } f\subseteq R \land \operatorname{dom}(R) = \operatorname{dom}(f)$$

on the other? This sounds a lot more like a theorem than an axiom. I cannot quite put my finger on it, but something is different between this one and the first two examples.

So, how can this axiom specifically be an axiom and how generally speaking can axioms like this one, that feel more like theorems, be axioms? Why do such propositions not need to be proven and can be asserted axiomatically?

• Whether something is an axiom or a theorem has nothing to do with the complexity of the formulation. – Arthur Nov 11 '17 at 23:59
• It's not a theorem, as it is not a logical consequence of the remaining axioms of set theory. – Lord Shark the Unknown Nov 12 '17 at 0:01
• How do you feel about the (relatively complicated) parallel postulate being one of Euclid's axioms for Euclidean geometry? – Eric Towers Nov 12 '17 at 0:02
• @EricTowers That makes intuitive sense, but I feel the same way about it as the axiom of choice (which also makes intuitive sense, I guess). – user3578468 Nov 12 '17 at 0:04
• @user3578468 Yes - this was proved by Paul Cohen in 1963. – Noah Schweber Nov 12 '17 at 0:19

## 1 Answer

When asking whether or not an axiom can be proven, we need to ask "relative to what?" In other words, what axioms would we be allowed to use to prove it. Usually the answer here is something along the lines of "all of the other axioms".

Here, we typically take the 'other axioms' to be the ZF axioms of set theory. It is known that the axiom of choice is not a logical consequence of the ZF axioms. This was proven by Paul Cohen in the 1960s. What he showed, essentially, is that if there is a structure that satisfies the ZF axioms, then there is a structure that satisfies the ZF axioms but not AC. It had been shown earlier by Godel that if there is a structure that satisfies the ZF axioms, then there is one that satisfies ZF and the axiom of choice (ZFC). So the axiom of choice is truly independent of the other axioms.

It is useful to compare this to the situation with Euclid's parallel postulate, as I see people already doing in the comments. People thought for a long time that it must be provable from the other axioms. Let's call the other axioms neutral geometry NG. Of course a long time later, the mystery was solved why you could not prove the parallel postulate. There are structures that satisfy the NG axioms and also satisfy the parellel postulate (Euclidean geometry) and structures that satisfy the NG axioms but don't satisfy the parallel postulate (non-Euclidean geometries). It simply turned out that the other axioms were not sufficient to fully pin down Euclidean geometry, because there are multiple types of geometry that differ on whether the parallel postulate is true (and how it fails if it does).

Similarly, assuming ZF is consistent, there are many different universes of sets that are models of ZF, and they differ from one another on whether the axiom of choice is true.

Another useful comparision that's often made is to group theory. The axioms of group theory say that there are elements and a binary operation between them that obey certain properties. We find many structures that obey the axioms of group theory... we call them groups. There are many statements that are independent of the axioms of group theory. For instance $$\forall (x,y)\; x\cdot y = y\cdot x$$ is independent of the axioms of group theory since there are both abelian and non-abelian groups.

Similarly the axioms of ZF are that there are some elements (called sets) and a binary relation between them $$\in$$ such that $$x\in y$$ is interpreted as "$$x$$ is an element of $$y$$." We call a structure that obeys ZF a "model of ZF" (doesn't have a snappy name like "group"). Cohen and Godel showed that the axiom choice is independent of the ZF axioms just like the "commutativity axiom" is independent of the axioms of group theory.