What makes Tarski Grothendieck set theory non-empty?

Question

I'm fighting with Grothendieck set theory for some time now. This is the framework for the automated proof checking system of Mizar and hence there is a formalized version of the axioms here too, and here in the "Content" link provided as a pdf.

What I want to understand is how the theory contains sets at all, and then where which kinds of sets resides.

The first question would be answered if we establish why the theory contains the empty set. I read the theads

The existence of the empty set is an axiom of ZFC or not?

and

How do I get the existence of a set in ZFC following Jech?

However they are concerned with a pretty different set theory.

Now if the empty set would be established, then I guess the theory guarantees the existence of a Grothendieck universe with lots of nice stuff. Okay there is the claim on the Wikipedia page that the Tarski axiom implies the axiom of infinity and the existence of any set would mean we win. However I can not see how that Tarski axiom formulation

 reserve x,y,z,u,N,M,X,Y,Z for set;
 ...
 ex M st N in M &
 (for X,Y holds X in M & Y c= X implies Y in M) &
 (for X st X in M ex Z st Z in M & for Y st Y c= X holds Y in Z) &
 (for X holds X c= M implies X,M are_equipotent or X in M);

lets us generate even one axiom if the all-quantor goes over an empty domain.

Another path: If we search for the first occurence of the empty set in the Mizar Mathematical Library, then we find it here right after the axiom schema of separation is established. Clicking on "proof" then allows us to see how the schema is used to show the existence. It so happens that in the end of the following article

http://en.wikipedia.org/wiki/Axiom_of_empty_set

they exactly refer to a procedure to get a set from the separation axiom, however I read this and it still doesn't clear things up. And it goes without saying that there is no "it exists a set such..." axiom in the Mizar library.

Lastly, I can note that the defintion or specification of the empty set

 definition
 func {} -> set means
 :: XBOOLE_0:def 1
 not ex x being set st x in it;

is done by introducing something they denote "functor", but it's not a functor in the category theoretical sense, I think it's a term constructor as they also use this to define the pair in on the axiom page

  definition let y; func { y } means
  :: TARSKI:def 1
  x in it iff x = y;
  let z; func { y, z } means

I'm not even certain if this is an axiom guaranteeing the existence of the "functor" or if it's merely notation construction.

One more note: I read this SE thread and in the answer the poster says "One often needs to check that some definition doesn't depend on which universe it's carried out in". I wonder, if I'm interested in sets for doing topology and propability theory, will this named disadvantage be really one?

Answer 1

Axiomatic set theories are usually supposed to use classical first-order logic as their substratum, and classical first-order logic as it is usually formalized implicitly requires that the domain of discourse must be non-empty.

More technically, if $\varphi$ is any logical formula in the language we're considering, then first-order logic proves $\exists x(\varphi \lor \neg \varphi)$ using purely logical axioms and rules, needing no set-theoretical axioms at all for this. Therefore the existence of some set doesn't need to be made an axiom of the theory -- it can be assumed as a boundary condition because the theory is a creature of first-order logic.

It is possible to formulate a variant of first-order logic that doesn't prove things that are false in the empty domain of discourse -- but the cost of this is more complex rules for reasoning about quantifiers, and the only thing it buys us is to allow a rather uninteresting corner case as a model, which isn't usually considered worth the price.

Certainly it would be pointless to make logic itself more complex only to need to add an explicit axiom to our set theory whose effect is to negate what we just did.

---

This is often felt to be a rather subtle point, though, so to avoid confusion some introductions may choose to include "something exists" as an explicit axiom anyway -- after all this doesn't hurt unless we put a special value on having a minimal set of axioms, which is generally not achievable when there are axiom schemas around anyway.

Also, in set theories such as ZF where there is already, for other reasons, one or more axioms with a $\exists$ as the outermost quantifier, then it can be seen as worth a modest amount of ink to point out that this would allow us to prove that a set exists, even if we chose to work in a logic background that doesn't do this itself.