Klassen in der Zermelo-Fraenkel-Mengenlehre

Die Regel For4ZF erlaubt es uns für jede denkbare Eigenschaft $\phi$ eine ZF-Formel der Form $\{x | \phi(x,\dots)\}$ zu bilden. Diese Objekte nennen wir Klassen oder auch Klassenterme, da sie im Allgemeinen keine Mengen sein müssen. Nur wenn die Axiome die Bildung einer entsprechen Menge zulassen, können wir sie wie Mengen behandeln. Handelt es sich bei einer Klasse um keine Menge sprechen wir von einer echten Klasse.

Zur Vereinfachung der Schreibweise wollen wir konkrete Klassen der Form $\{x | \phi(x,\dots)\}$ mit Großbuchstaben wie $A, B, C\dots$ bezeichnen. Dabei gilt es einige Klippen zu umschiffen. Die allgemeine Quantisierung über Klassen ist in ZF nicht erlaubt.

Wenn wir Aussagen über Klassen $A$ mit gewissen Eigenschaften treffen, müssen wir immer daran denken, dass wir stets von konkreten Klassentermen der Form $\{x | \phi(x,\dots)\}$ sprechen und niemals über abstrakte Klassenvariablen $A$ etc., denn diese sind nicht Bestandteil unserer Sprache. Daher sind Terme wie $\forall A \dots$ oder $\exists A \dots$ in ZF nicht erlaubt, während sie bei Mengenvariablen sehr wohl Bestandteil der ZF-Sprache sind.

Analog zu den Mengen, benutzen wir bei Klassen die abkürzenden Schreibweisen $\forall x\in A \, \phi$ für $\forall x (x\in A\implies\phi)$ $\exists x\in A \, \phi$ für $\exists x (x\in A\and \phi)$

Wir können ZF komplett basierend auf die Regeln For1ZF - For3ZF aufbauen und auf die Klassenbildungsregel For4ZF verzichten. Da diese aber eine einfache und bequeme Methode zur Bildung von Klassen gestattet, wollen wir For4ZF jedoch mit hinzunehmen. Dann benötigen wir eine Methode mit der wir die Klassenausdrücke in Ausdrücke ohne Klassenbildung zu überführen.

Dieses Axiom ermöglicht es uns Klassenterme zu eliminieren oder für beliebige Eigenschaften welche zu bilden.

KeZF und For4ZF werden lediglich aus Gründen der Bequemlichkeit benötigt. Man kann zeigen, dass die von For1ZF - For3ZF erzeugte Sprache genauso mächtig ist wie die vollen ZF-Sprache ergänzt um KeZF.

Alternativ hätten wir auch unsere Sprache um Klassenausdrücke erweitern können und KeZF zu ihrer Definition verwenden können.