# What axioms does ZF have, exactly?

While trying to find the list of axioms of ZF on the Web and in literature I noticed that the lists I had found varied quite a bit. Some included the axiom of empty set, while others didn't.

That is perfectly understandable - the statement of the axiom is provable from the axiom schema of specification. Some lists also contained the axiom of pairing, while others didn't - I've heard here on MSE that the statement of this axiom is also provable.

I was wondering: are there other axioms of ZF statements of which are also provable that I don't know of? What is the true commonly accepted list of ZF axioms which doesn't contain any redundant axioms included just for emphasis?

-
Does it matter what axioms you have? It matters what you can prove from them. And if you show that you can prove one list from the other and vice versa, then it doesn't matter anymore. For brevity, I prefer to think of ZF as the following: Extensionality, power set, union, regularity, replacement schema, infinity, choice. [Note that the replacement schema has two versions, one requires that we add the specification axiom as well; the other proves specification.] – Asaf Karagila Sep 1 '14 at 16:19
@AsafKaragila it's always nice to reduce the number of employed axioms, even though two different lists of axioms may be equivalent. And I also think it was you who told me that the axiom of pairing was not needed :-) – user132181 Sep 1 '14 at 16:22
Well, pairing is provable from replacement + power set + empty set; and empty set is provable from a myriad of axioms (infinity, for example). – Asaf Karagila Sep 1 '14 at 16:27
Of course in my first comment, choice is a explicit addition to $\sf ZF$. :-) – Asaf Karagila Sep 1 '14 at 16:37
@AsafKaragila I thought that asking the question in terms of ZFC instead of ZF would be... redundant (pun intended) :-D – user132181 Sep 1 '14 at 16:43

Here is my preferred list of axioms, they are written in the language of $\in$, and $=$ is a logical symbol.

1. Extensionality. $\forall x\forall y(x=y\leftrightarrow\forall z(z\in x\leftrightarrow z\in y))$. Two sets are equal if and only if they have the same elements.
2. Union. $\forall x\exists y\forall u(u\in y\leftrightarrow\exists v(v\in x\land u\in v))$. If $x$ is a set, then $\bigcup x$ is a set.
3. Regularity. $\forall x(\exists y(y\in x)\rightarrow\exists y(y\in x\land\forall z(z\in x\rightarrow z\notin y)))$. The $\in$ relation is well-founded.
4. Power set. $\forall x\exists y\forall z(z\in y\leftrightarrow\forall u(u\in z\rightarrow u\in x))$. If $x$ is a set, then $\mathcal P(x)$ is a set.
5. Replacement schema. If $\varphi(x,y,p_1,\ldots,p_n)$ is a formula in the language of set theory, then: $$\forall p_1\ldots\forall p_n\\ \forall u(\forall x(x\in u\rightarrow(\exists y\varphi(x,y,p_1,\ldots,p_n)\rightarrow\exists y(\varphi(x,y,p_1,\ldots,p_n)\land\forall z(\varphi(x,z,p_1,\ldots,p_n)\rightarrow z=y)))\rightarrow\exists v\forall y(y\in v\leftrightarrow\exists x(x\in u\land\varphi(x,y,p_1,\ldots,p_n))).$$ For every fixed parameters, $p_1,\ldots,p_n$, and for every set $u$, if for every $x\in u$ there is at most one $y$ such that $\varphi(x,y,p_1,\ldots,p_n)$, namely the formula, with the fixed parameters, define a partial function on $u$, then there is some $v$ which is exactly the range of this function.
6. Infinity. $\exists x(\exists y(y\in x\land\forall z(z\notin y))\land\forall u(u\in x\rightarrow\exists v(v\in x\land\forall w(w\in v\leftrightarrow w\in u\lor w=u))))$. There exist a set $x$ which has the empty set as an element, and whenever $y\in x$, then $y\cup\{y\}\in x$ as well.

I wrote those purely in the language of $\in$, as you can see, to avoid any claims that I need to use $\subseteq$ or $\mathcal P$ or $\bigcup$. I will now allow myself these addition to the language.

From these axioms we can easily:

1. Prove there is an empty set: it is the element of the set guaranteed to exist in the infinity axiom.
2. Prove the pairing axiom: By the power set axiom, $\mathcal P(\varnothing)$ exists, and its power set $\{\varnothing,\{\varnothing\}\}$ exists too. Now consider the formula $\varphi(x,y,a,b,c,d)$ whose content is $$(x=a\land y=c)\lor(x=b\land y=d).$$ Given two sets, $u,v$ consider the replacement axiom for $\varphi$ with the parameters: $\varphi(x,y,\varnothing,\mathcal P(\varnothing),u,v)$, and the domain $\mathcal{P(P(\varnothing))}$. Then there is a set who is the range of the function $\varphi$ defines here, which is exactly $\{u,v\}$.
3. Specification schema: Suppose that $\varphi(x,p_1,\ldots,p_n)$ is a formula in the language of set theory, and $A$ is a set which exists. Define $\psi(x,y,p_1,\ldots,p_n)$ to be $\varphi(x,p_1,\ldots,p_n)\land x=y$. Easily we can prove that given any element of $A$ there is at most one element satisfying $\psi(x,y,p_1,\ldots,p_n)$ (with the fixed parameters). And therefore the range of the function defined is $\{x\in A\mid\varphi(x,p_1,\ldots,p_n)\}$ as wanted.

And so on and so forth. The choice of axiomatization usually doesn't matter. But it does matter when one has to verify the axioms by hand for one reason or another, then it might be fortuitous to add explicit axioms or it might be better to keep it minimal. Depending on the situation.

It is also an important question what axioms you keep, or add, when you consider weakening of $\sf ZF$. You can remove replacement, but add specification, or perhaps specification for a particular class of formulas; or you can remove extensionality and then the choice whether to use Replacement or Collection schemas really prove a big different; and so on.

-
I'm extremely grateful for this very detailed answer, thank you very much. – user132181 Sep 1 '14 at 17:39
For rule two I think you meant x instead of z – DanielV Sep 1 '14 at 18:01
@Daniel: Thanks for noticing! – Asaf Karagila Sep 1 '14 at 20:44
In replacement, you presumably intended to say something about $y=z$ at the end of the second line. Also, there's an alternative proof of pairing using infinity and replacement. – Andreas Blass Sep 1 '14 at 23:30
@Andreas: D'oh, of course. – Asaf Karagila Sep 2 '14 at 4:12