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

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 ∀ab (a = b ⇔ ∀c (cacb)) and ∀aU (aU), 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?

• Unlike NBG, TG does not have a notion of class, so you can't use the term 'class'. Commented Jul 5, 2017 at 4:15
• Formally, there's no point to it, no. In ZF we understand everything in the domain of quantification to be a set, and don't need any special axiom to tell us so. Commented Jul 5, 2017 at 5:05
• I am not at all familiar with TG. But is there a def'n of a Grothendieck universe? I get the impression that sets are the things that are members of Grothendieck universes but that G.-universes are not members of anything. Is that correct? Commented Jul 5, 2017 at 21:34
• @DanielWainfleet Grothendieck universes are sets that contain all members of their members, all powersets of their members, and all subsets of themselves that are of a cardinality corresponding to an ordinal that they contain. They are designed as sets that share some properties with the proper classes of NBG/MK, but they are still sets and may be members of sets. Commented Jul 6, 2017 at 6:08

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.

The article you referred to is the second of the two axiomatic articles of the Mizar Mathematical Library. As described on that site:

All other texts undergo verification by Mizar to be correct consequences of those axioms. The Mizar system assists the author of a new text in preparing available terminology and results, verifies the claims of the text and extracts facts and definitions for inclusion into the library.

So the article you referred to (TARSKI) (note that the version you read was human written abstract + latexed version of the human written article for the Mizar system, the latter being able to be understood by the machine) was explicitly written as foundation for a strict computational verification system. As such, you can't simply be

Using the definition of a set as a "class that is a member of a class"

because that is not what it is built on. The axiomatics, as well as Mizar in general, are covered in "Mizar in a Nutshell" by Adam Grabowski et al.

The other one of the two axiomatic articles is literally HIDDEN. The important logical concepts (e.g. $\land$ &, $\lor$ or, $\neg$ not (for predicates) or non (for attributes), $\Rightarrow$ implies, $\Leftrightarrow$ iff, $\forall$ for, $\exists$ ex) are wired directly into the software and grammar of the Mizar language, but explicit modes (what kind of something else something can be, like an object or a set) or explicit predicates (saying that one or several something(s) are in some relation to another or not, like $x=y$ x = y, $x\neq y$ x <> y and $x\in X$ x in X) which basically the foundation to be even able to talk about axioms haven't been declared implicitly in the software, but explicitly in HIDDEN. They just are. And based on that, the axioms in TARSKI could be defined from the programming point of view. Or as it is put in "Mizar in a Nutshell":

[HIDDEN] documents a part of the Mizar axiomatics – it shows how the primitives of set theory are introduced in the Mizar Mathematical Library.

"Mizar in a Nutshell" goes through each of the short axiomatic articles. It states

[TARSKI] defines axiomatic foundations of the Tarski- Grothendieck set theory: extensionality axiom [TARSKI:2] [...]

and goes on with the rest of the article, thereby implicitly stating that TARSKI:1 ("everything is a set") is not directly part of the TG axioms, but simply a part of the Mizar axiomatics. In fact, one could have left objects out of the whole axiomatization and sometimes I wonder if that wouldn't have been better, or just introduce "object" as a different notation of set, but in the end, it basically amounts to the same thing, but improves readability alot, depending on an author wanting to emphasize if a certain "thing" is an object or rather a set (which e.g. can be empty or stand on the right side of an in).

If you are interested in it, the empty set is derived from these axioms here.

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).

• I believe that the paper in the question is the original definition of the TG set theory. It says that it is from 1989. Commented Jul 7, 2017 at 7:13