In mathematics and logic, Ackermann set theory (AST) is an axiomatic set theory proposed by Wilhelm Ackermann in 1956.
AST is formulated in first-order logic. The language of AST contains one binary relation denoting set membership and one constant denoting the class of all sets (Ackermann used a predicate instead).
The axioms of AST are the following:
- comprehension on : for any formula where is not free,
- Ackermann's schema: for any formula with free variables and no occurrences of ,
An alternative axiomatization uses the following axioms:
- reflection: for any formula with free variables ,
denotes the relativization of to , which replaces all quantifiers in of the form and by and , respectively.
Relation to Zermelo–Fraenkel set theory
Let be the language of formulas that do not mention .
In 1959, Azriel Levy proved that if is a formula of and AST proves , then ZF proves .
In 1970, William N. Reinhardt proved that if is a formula of and ZF proves , then AST proves .
Therefore, AST and ZF are mutually interpretable in conservative extensions of each other. Thus they are equiconsistent.
A remarkable feature of AST is that, unlike NBG and its variants, a proper class can be an element of another proper class.
An extension of AST called ARC was developed by F.A. Muller, who stated that ARC "founds Cantorian set-theory as well as category-theory and therefore can pass as a founding theory of the whole of mathematics".