Category:Zermelo-Fraenkel Class Theory

From ProofWiki
Jump to navigation Jump to search

This category contains results about classes in ZF set theory.
Definitions specific to this category can be found in Definitions/Zermelo-Fraenkel Class Theory.

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.