In TG, what is the purpose of the "set axiom"

Question

Recently I have been reading about Tarski-Grothendieck set theory, and have been impressed by its short axiomatisation, inclusion of inaccessible cardinals, and capability of supporting category theory without proper classes. http://mizar.org/JFM/pdf/tarski.pdf.

However, I am somewhat confused by its first axiom, which states that everything is a set. It then formulates extensionality by saying that two sets are equal if they have the same members, and Tarski's axiom by saying that every set is a member of a Grothendieck universe. This seems unnecessarily complex to me. Using the definition of a set as a "class that is a member of a class", wouldn't the statements ∀a∀b (a = b ⇔ ∀c (c ∈ a ⇔ c ∈ b)) and ∀a∃U (a ∈ U), where U is a Grothendieck universe, prove that if an object has no members, it would be the empty set, and that anything else would of course be a set, as it would both have members and be a member of a Grothendieck universe.

Am I misunderstanding something, or is there some other reason for using the set axiom?

Answer 1

You're reading it "wrong". They only clarify the context, that all the variables indicate sets, and not some atomic objects like you might want to think about the real numbers as being "numbers" rather than sets.

Note that this is a short paper related to the Mizar system, which is a proof assistant. Since proof assistants are meant to be used by mathematicians who might not subscribe to the notion "everything is a set", it is a good idea to remind them of this fact when it is relevant.

From a set theoretic foundational perspective, yeah, nothing is new by this update. For other people? Well, that might not be the case.

Answer 2

First you should look at https://en.wikipedia.org/wiki/Tarski%E2%80%93Grothendieck_set_theory for the axioms in TG. They are written in standard/logic language You can see that there is no set axiom. Second the reference you quoted starts with axiom 2 and a footnote says that axiom 1 (the set axiom which bothers you) has been deleted. You must have read it in another/older paper. This is a translation in machine readable language of the axioms found in Wikipedia. Obviously, if every thing that you can quantify is called "set" , then there is no point in writing/checking this any longer (the predicate set(x) is always true).