Is the Axiom of Empty Set a canonical ZFC axiom? As in title.
The Axiom of Empty set is sometimes offered as a fundamental axiom in the ZFC framework (example), but sometimes it is not (example). Would you consider it a tenth canonical ZFC axiom? Am I misunderstanding things?
In case the question is more nebulous at very advanced levels of mathematics: I am asking in the context of an introductory course on axiomatic set theory.
Thank you for your time!
 A: The existence of an emptyset follows from the other axioms. The axiom of Infinity implies, in particular, that there is at least one set $a$. Next, the axiom of Separation comes into play: supposing $a$ is some set, consider the set  $\{x\in a \mid x\not=x \}$. This is (it is easy to prove) an empty set! With the axiom of Extensionality, any two sets with the same elements are the same set; so we may reasonably call this the emptyset.
So there is no need to consider a separate axiom asserting the existence of the emptyset.
A: As Noah explains, the existence of the empty set can be derived from the axioms of infinity and separation, so it is not strictly necessary to have an axiom that states explicitly that an empty set exists. However, by the same token it doesn't harm to have such an axiom (in the sense that the theorems we can prove with and without that axiom are the same), which is why textbook authors can get away with either including it or not and call the resulting system ZFC in both cases!
One reason for including this axiom could be that one is interested in studying what happens if the axiom of infinity is removed from ZFC. In that case we would need to have some other way to guarantee that sets exist, and the relation between the full ZFC and the one without infinity will be clearer if one is an actual subset of the other.
But actually it is even subtler than that.
ZFC is intended to be used within the framework of first-order logic, and usual first-order logic implicitly assumes that at least one thing exists. In other words, first-order logic can prove $\exists x(x=x)$ without any set-theoretic axioms at all.  So one doesn't even need the axiom of infinity to carry out Noah's argument in formal logic -- separation alone will allow you to prove $\exists z \forall x(x\notin z)$ which says that an empty set exists.
Textbooks typically don't take the consequence of this and formulate ZFC without an empty-set axiom. One reason for this is that it puts an extra burden on the author to convince students that "something exists" is a logical truth rather than something the theory needs to supply. And it is really only considered a logical truth for somewhat boring technical reasons. It is not as if it is so by necessity; it is just easier to construct a ruleset for what a valid proofs is if we allow ourselves to make that assumption.
Another reason is that it is something of an accident that the logical truth "there exists something" means "there exists a set", because in ZFC everything that exists is a set. But there are other closely related theories where the something that exists is not necessarily a set -- in particular,  in NGB set theory it might be a "proper class" instead. In those theories one needs an axiom to claim that there exists a set, so it is convenient to make that axiom a part of ZFC too, such that one can compare the systems without being sidetracked by irrelevant differences.
A: When the axioms of ZF or ZFC are listed, they often include three "redundant" results: the axiom of the empty set, the axiom of the unordered pair and the axiom schema of comprehension. Each of these is provable only by using the axiom schema of replacement, and they are explicitly required axioms in the weaker Zermelo set theory.
