What axioms does ZF have, exactly?

Question

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?

Answer 1

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))))\text{.}$$ 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.