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 $\mathrm{\neg }$, $\wedge$, $\vee$, $\to$, $\leftrightarrow$ and the quantifiers $\mathrm{\forall }x$ and $\mathrm{\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: $\mathrm{\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\mathrm{\ne }y$ for $\mathrm{\neg }(x=y)$ and $x\mathrm{\notin }y$ for $\mathrm{\neg }(x\in y)$; we abbreviate $\mathrm{\forall }z(z\in x\to \phi )$ by $\mathrm{\forall }z\in x\phi$ and $\mathrm{\exists }z(z\in x\wedge \phi )$ by $\mathrm{\exists }z\in x\phi$; and we abbreviate $\mathrm{\exists }w(\psi (w)\wedge \mathrm{\forall }v(\psi (v)\to v=w))$ by $\mathrm{\exists }!w\psi (w)$, read "there is exactly one $w$ with $\psi (w)$".

A formula is written $\phi (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:\phi (z,\bar{p})\}$ is not a term of the language. It is notation for the formula $\phi$ itself, and a sentence written with it abbreviates a sentence that does not use it:

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

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:\phi (z)\}$ as a term would make "$\{z:\phi (z)\}$ exists" a triviality, and that is exactly the reading There is no $R$ with $x\in R\leftrightarrow x\mathrm{\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.