Komprehensionsaxiom
Das Komprehensionsaxiom ( lat. comprehension: Zusammenfassung) bezeichnet ein Axiom der Prädikatenlogik und ein Axiom der Mengenlehre.
Komprehensionsaxiom in der Prädikatenlogik
Das Komprehensionsnaxiom ist ein Axiom der Prädikatenlogik höherer Stufe, aufgrund dessen zu jedem Ausdruck
- H(v1,......,vn)
des entsprechenden Prädikatenkalküls in vollfreien Variablen v1,......,vn bzw. der Typen
- τ1,.....,τn
ein Prädikat des Typs (τ1,.......,τn) existiert, das auf alle n-Tupel (Q1,.....,Qn) von Prädikaten bzw. der Typen τ1,....,τn zutrifft, für die der Ausdruck H wahr ist. In Formeln:
- v(v1,....,vn)
wobei also v1,.....,vn Variablen der Typen τ1,......,τn sind und v eine Variable des Typs (τ1,.....,τn) ist.
Komprehensionsaxiom der Mengenlehre
Das Komprehensionsaxiom ist ein Axiom der Mengtenlehre, das man allgemein wie folgt formulieren kann:
Ist H(v) ein Ausdruck mit einer Variablen v, so existiert eine Menge, zu der alle Objekte x gehören, für die durch Einsetzung von x für v in H eine wahre Aussage H(x) entsteht. Aus dem Extensionalitätsaxiom ergibt sich dann sofort, daß es genau eine solche Menge gibt, die durch
- {x:H(x)}
[gelesen: "die Menge aller x mit der Eigenschaft H(x) "] bezeichnet wird.
In dieser Form wird das Komprehensionsaxiom auch naives Mengenbildungsprinzip genannt. Werden dem Ausdruck H keine Beschränkungen auferlegt, so treten Antinomien auf; z.B. führt führt der Ausdruck 
zur Russelschen Antinomie der Menge aller Mengen, die sich nicht selbst als Element enthalten.
Bei einem axiomatischen Aufbau der Mengenlehre wird durch die verschiedenen Einschränkungen erreicht, daß die Menge
- {x:H(x)}
nur für "vernünftige" Ausdrücke H gebildet werden kann, die nicht zu Widersprüchen führen. Im Aufbau der Mengenlehre nach Zermelo-Fraenkel z.B. erreicht man dies durch die Forderung, daß nur die Elemente x einer bereits gebildeten Menge M in einer Menge der Form {x:H(x)} aufgenommen werden dürfen.
Man nennt in diesem Fall das Komprehensionsaxiom auch Aussonderungsaxiom. In der von Bertrand Russell begründeten Typentheorie wird gefordert, daß alle Elemente x der Menge {x:H(x)} die gleiche Stufe besitzen, während die Menge selbst die nächst höhere Stufe erhält.
In einem von John von Neumann, Paul Bernay und Kurt Gödel begründeten Aufbau der Mengenlehre mit Klassen kann uneingeschränkt die Klasse {x:H(x)} gebildet werden, in die jedoch nur diejenigen Klassen x mit der Eigenschaft H(x) aufgenommen werden, die Mengen sind, und dabei ist eine Klasse genau dann eine Menge, wenn sie Element einer anderen Klasse ist.