Set theory has a binary relation symbol \(\in\), which denotes set membership.
Specifically, \(a \in b\) denotes that \(a\) is a member of \(b\).
A bounded quantifier is a quantifier that ranges over an explicit domain.
The universal and existential bounded quantifiers are defined as follows, respectively:
\[ (\forall a \in b) \phi \equiv \forall a (a \in b \to \phi) \] \[ (\exists a \in b) \phi \equiv \exists a (a \in b \land \phi) \]A bounded formula is a formula in which all quantifiers are bounded.
Many concepts in set theory can be expressed as bounded formulas.
Some examples are the following. For example, \(\text{pair}(a, b, c)\) should be read as “\(a\) is a pair containing \(b\) and \(c\)”.
\begin{align} \text{empty}(a) &\equiv (\forall x \in a) \bot \\ \text{inhabited}(a) &\equiv (\exists x \in a) \top \\ a \subseteq b &\equiv (\forall x \in a) (x \in b) \\ \text{overlap}(a, b) &\equiv (\exists x \in a) (x \in b) \\ \text{disjoint}(a, b) &\equiv (\forall x \in a) (x \not\in b) \\ \text{singleton}(a, b) &\equiv b \in a \land (\forall x \in a) (x = b) \\ \text{pair}(a, b, c) &\equiv b \in a \land c \in a \land (\forall x \in a) (x = b \lor x = c) \\ \text{binaryunion}(a, b, c) &\equiv b \subseteq a \land c \subseteq a \land (\forall x \in a) (x \in b \lor x \in c) \\ \text{binaryintersection}(a, b, c) &\equiv (\forall x \in b) (x \in c \to x \in a) \land (\forall x \in a) (x \in b \land x \in c) \\ \text{union}(a, b) &\equiv (\forall x \in b) (x \subseteq a) \land (\forall y \in a) (\exists x \in b) (y \in x) \\ \text{adjunction}(a, b, c) &\equiv b \subseteq a \land c \in a \land (\forall x \in a) (x \in b \lor x = c) \\ \text{successor}(a, b) &\equiv \text{adjunction}(a, b, b) \\ \text{inductive}(a) &\equiv (\exists x \in a) \text{empty}(x) \land (\forall x \in a) (\exists y \in a) \text{successor}(y, x) \\ \text{transitive}(a) &\equiv (\forall x \in a) (x \subseteq a) \\ \text{transitiveclosure}(a, b) &\equiv b \in a \land \text{transitive}(a) \\ \text{intersection}(a, b) &\equiv (\forall x \in b) (\forall y \in x) ((\forall x' \in b) (y \in x') \to y \in a) \land (\forall y \in a) (\forall x \in b) (y \in x) \\ \text{partition}(a) &\equiv (\forall x \in a) \text{inhabited}(x) \land (\forall x, y \in a) (\text{overlap}(x, y) \to x = y) \\ \text{transversal}(a, b) &\equiv (\forall s \in b) (\exists_{=1} r \in a) (r \in s) \land (\forall r \in a) (\exists_{=1} s \in b) (r \in s) \end{align}Here, \(\exists_{=1}\) is the uniqueness quantifier, which is defined by
\[ \exists_{=1} \phi \equiv \exists x (\phi \land \forall y (\phi[x/y] \to x = y)) \]The standard set theory is Zermelo–Fraenkel set theory (ZFC). It is commonly used as a foundation of mathematics.
Several axioms of ZFC can be expressed in the form
\[ \exists a \phi \]where \(\phi\) is a bounded formula.
For example:
The axiom of empty set is
\[ \exists a \; \text{empty}(a) \]The axiom of pairing is
\[ \exists a \; \text{pair}(a, b, c) \]The axiom of union is
\[ \exists a \; \text{union}(a, b) \]The axiom of infinity is
\[ \exists a \; \text{inductive}(a) \]The axiom of choice states that every partition has a transversal:
\[ \text{partition}(b) \to \exists a \; \text{transversal}(a, b) \]The axiom schema of bounded separation states that, if \(\phi\) is a bounded formula in which \(b\) is not free, then
\[ \exists a ((\forall x \in b) (\phi \to x \in a) \land (\forall x \in a) (x \in b \land \phi)) \]One notable exception to this pattern is the axiom of powerset:
\[ \text{powerset}(a, b) \equiv \forall x (x \subseteq b \to x \in a) \land (\forall x \in a) (x \subseteq b) \] \[ \exists a \; \text{powerset}(a, b) \]This has higher quantifier complexity because the powerset predicate is not a bounded formula.
A formula is \(\Delta_0 = \Pi_0 = \Sigma_0\) iff it is bounded.
A formula is \(\Delta_i\) iff it is both \(\Sigma_i\) and \(\Pi_i\).
A formula is \(\Pi_{i+1}\) iff it is equivalent to \(\forall x_1, \ldots, x_n \phi\) where \(\phi\) is \(\Sigma_i\).
A formula is \(\Sigma_{i+1}\) iff it is equivalent to \(\exists x_1, \ldots, x_n \phi\) where \(\phi\) is \(\Pi_i\)
The resulting hierarchy of formulas is called the Lévy hierarchy.