The first-order language of set theory: $\in$, $=$, formulas with parameters, and class abbreviations

The language of set theory is first-order logic with equality whose only non-logical symbol is a binary relation symbol $\in$. Its terms are the variables $x, y, z, \dots$; its atomic formulas are $x \in y$ and $x = y$; and its formulas are built from atomic formulas by the connectives $\neg$, $\wedge$, $\vee$, $\to$, $\leftrightarrow$ and the quantifiers $\forall x$ and $\exists x$. Each axiom stated on this page is a sentence of this language, and no other vocabulary occurs in any of them.

Two conventions of ordinary first-order logic are in force throughout.

• The domain of discourse is nonempty: $\exists x\,(x = x)$ is logically valid, so some object exists before any axiom is assumed.
• Every object of the domain is a set. There are no urelements, so "$z$" and "the set $z$" say the same thing.

We write $x \neq y$ for $\neg(x = y)$ and $x \notin y$ for $\neg(x \in y)$; we abbreviate $\forall z\,(z \in x \to \varphi)$ by $\forall z \in x\,\varphi$ and $\exists z\,(z \in x \wedge \varphi)$ by $\exists z \in x\,\varphi$; and we abbreviate $\exists w\,\bigl(\psi(w) \wedge \forall v\,(\psi(v) \to v = w)\bigr)$ by $\exists! w\,\psi(w)$, read "there is exactly one $w$ with $\psi(w)$".

A formula is written $\varphi(z, \bar p)$ when its free variables are among $z$ and the variables of the list $\bar p = p_1, \dots, p_n$; the $p_i$ are its parameters. Parameters matter because an axiom schema ranges over formulas, and a formula may mention sets already in hand.

A class abbreviation $\{\, z : \varphi(z, \bar p) \,\}$ is not a term of the language. It is notation for the formula $\varphi$ itself, and a sentence written with it abbreviates a sentence that does not use it:

• $w \in \{\, z : \varphi(z, \bar p) \,\}$ abbreviates $\varphi(w, \bar p)$;
• "$\{\, z : \varphi(z, \bar p) \,\}$ is a set" abbreviates $\exists y\,\forall z\,\bigl(z \in y \leftrightarrow \varphi(z, \bar p)\bigr)$.

Every formula has a class abbreviation, and whether that abbreviation is a set is a separate question; answering it affirmatively always requires an axiom.

• ZFC. ZFC is the theory whose axioms are the ZF axioms stated on this page together with the Axiom of Choice, which this library states at The Axiom of Choice ↗. Choice is stated there and not restated here, and no construction and no result on this page uses it. The axiom ledger for this page: which of the ZFC axioms each construction and each result actually consumes records, axiom by axiom, what the material on this page does use.

• Why the class notation needs its own convention. Reading $\{\, z : \varphi(z) \,\}$ as a term would make "$\{\, z : \varphi(z) \,\}$ exists" a triviality, and that is exactly the reading There is no $R$ with $x \in R \leftrightarrow x \notin x$ for every $x$ refutes. Keeping it an abbreviation is what forces every set-forming step below to name the axiom that licenses it.