Definition:Class (Class Theory)/Zermelo-Fraenkel

From ProofWiki
Jump to navigation Jump to search


Denote with $\textrm{ZF}$ the language of set theory endowed with the Zermelo-Fraenkel axioms.

A class in $\textrm{ZF}$ is a formal vehicle capturing the intuitive notion of a class, namely a collection of all sets such that a particular condition $P$ holds.

In $\textrm{ZF}$, classes are written using class-builder notation:

$\set {x : \map P x}$

where $\map P x$ is a well-formed formula containing $x$ as a free variable.

More formally, a class $\set {x: \map P x}$ serves to define the following definitional abbreviations involving the membership symbol:

\(\ds y \in \set {x: \map P x}\) \(\text{for}\) \(\ds \map P y\)
\(\ds \set {x: \map P x} \in y\) \(\text{for}\) \(\ds \exists z \in y: \forall x: \paren {x \in z \iff \map P x}\)
\(\ds \set {x: \map P x} \in \set {y: \map Q y}\) \(\text{for}\) \(\ds \exists z: \paren {\map Q z \land \forall x: \paren {x \in z \iff \map P x} }\)


$x, y ,z$ are variables of $\textrm{ZF}$
$P, Q$ are well-formed formulas.

Through these "rules", every statement involving $\set {x: \map P x}$ can be reduced to a simpler statement involving only the basic language of set theory.

This definition "overloads" the membership symbol $\in$ since its operands could now be either sets or classes.

That such does not lead to ambiguity is proved on Class Membership Extension of Set Membership.

Class Variables

In deriving general results about $\textrm{ZF}$ which mention classes, it is often convenient to have class variables, which denote an arbitrary class.

By convention, these variables are taken on $\mathsf{Pr} \infty \mathsf{fWiki}$ to be the (start of) the capital Latin alphabet, i.e. $A, B, C$, and so on.


Unlike in von Neumann-Bernays-Gödel set theory, it is prohibited to quantify over classes.

That is, expressions like:

$\forall A: \map P A$

are ill-defined; admitting them without further consideration would lead us to Russell's Paradox.