Zermelo–Fraenkel set theory

Formally, ZFC is a one-sorted theory in first-order logic. Equality is treated as a primitive logical symbol and the signature has a single primitive non-logical symbol, usually denoted ${\displaystyle \in }$, which is a predicate symbol of arity 2 (a relation symbol). This symbol symbolizes a set membership relation. For example, the formula ${\displaystyle a\in b}$ means that a is an element of the set b (also read as a is a member of b).


The language's alphabet consists of:


With this alphabet, the iterative rules for forming well-formed formulae (wff) are as follows:


${\displaystyle x}$ and ${\displaystyle y}$ above are metavariables standing for any variables. The first rule describes the two ways to build an atomic formula. As a general rule, the brackets for ${\displaystyle \land }$ and ${\displaystyle \lor }$ may be dropped following this order precedence: not, and, or. ${\displaystyle (x)}$ and ${\displaystyle (\exists x)}$, which are read as "given any x" and "there exists an x such that" respectively, may also be written as ${\displaystyle \forall x}$ and ${\displaystyle \exists x}$ respectively. We define ${\displaystyle (\phi \Rightarrow \psi )}$ as ${\displaystyle (\lnot \phi \lor \psi )}$, and ${\displaystyle (\phi \Leftrightarrow \psi )}$ as ${\displaystyle (\phi \Rightarrow \psi )\land (\psi \Rightarrow \phi )}$. The type of brackets used need not be fixed and a blending of different types may be seen in the literature to aid readability.


A statement in set-builder notation abbreviates a wff. An expression representing a mathematical object abbreviates a noun phrase in the metalanguage denoting a specific set that satisfies a specific (usually long) wff. The following tables illustrate some correspondences:


The symbols for a formal language are not set in stone, rather, the emphasis is on the form of the proposition. A wff can be visualised as a syntax tree: the atomic formulae are nodes at the end of the branches while ${\displaystyle \lnot }$ , ${\displaystyle \land }$ , ${\displaystyle \lor }$ , ${\displaystyle \langle x\rangle }$ and ${\displaystyle \langle \exists x\rangle }$ are the other nodes in the tree. A property of ${\displaystyle \land }$ and ${\displaystyle \lor }$ is that they may be swapped with each other by inserting ${\displaystyle \lnot }$ onto adjacent edges to obtain an equivalent wff (De Morgan's laws). This is also the case with ${\displaystyle \langle x\rangle }$ and ${\displaystyle \langle \exists x\rangle }$. If two ${\displaystyle \lnot }$ in the tree have an edge between them, they may both be removed from the tree (double negation). There are countably infinitely many wff, however, each wff has a finite number of nodes.