Definition:Class (Class Theory)/Zermelo-Fraenkel
 | This article needs to be linked to other articles. In particular: NGB You can help $\mathsf{Pr} \infty \mathsf{fWiki}$ by adding these links. To discuss this page in more detail, feel free to use the talk page. When this work has been completed, you may remove this instance of {{MissingLinks}} from the code. |
Definition
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} }\) |
where:
- $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.
 | This page needs proofreading. Please check it for mathematical errors. If you believe there are none, please remove {{Proofread}} from the code.To discuss this page in more detail, feel free to use the talk page. When this work has been completed, you may remove this instance of {{Proofread}} from the code. |
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.
Caution
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.