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.