In mathematics and logic, **Ackermann set theory** (AST) is an axiomatic set theory proposed by Wilhelm Ackermann in 1956.^{[1]}

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:^{[2]}^{[3]}^{[4]}

- extensionality
- heredity:
- 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:^{[5]}

- extensionality
- heredity
- comprehension
- reflection: for any formula with free variables ,
- regularity

denotes the *relativization* of to , which replaces all quantifiers in of the form and by and , respectively.

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 .^{[6]}

In 1970, William N. Reinhardt proved that if is a formula of and ZF proves , then AST proves .^{[7]}

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.^{[4]}

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".^{[8]}