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

The language

AST is formulated in first-order logic. The language ${\displaystyle L_{\{\in ,V\))}$ of AST contains one binary relation ${\displaystyle \in }$ denoting set membership and one constant ${\displaystyle V}$ denoting the class of all sets (Ackermann used a predicate ${\displaystyle M}$ instead).

The axioms

The axioms of AST are the following:^[2][3][4]

1. extensionality
2. heredity: ${\displaystyle (x\in y\lor x\subseteq y)\land y\in V\to x\in V}$
3. comprehension on ${\displaystyle V}$: for any formula ${\displaystyle \phi }$ where ${\displaystyle x}$ is not free, ${\displaystyle \exists x\forall y(y\in x\leftrightarrow y\in V\land \phi )}$
4. Ackermann's schema: for any formula ${\displaystyle \phi }$ with free variables ${\displaystyle a_{1},\ldots ,a_{n},x}$ and no occurrences of ${\displaystyle V}$, ${\displaystyle a_{1},\ldots ,a_{n}\in V\land \forall x(\phi \to x\in V)\to \exists y{\in }V\forall x(x\in y\leftrightarrow \phi )}$

An alternative axiomatization uses the following axioms:^[5]

1. extensionality
2. heredity
3. comprehension
4. reflection: for any formula ${\displaystyle \phi }$ with free variables ${\displaystyle a_{1},\ldots ,a_{n))$, ${\displaystyle a_{1},\ldots ,a_{n}{\in }V\to (\phi \leftrightarrow \phi ^{V})}$
5. regularity

${\displaystyle \phi ^{V))$ denotes the relativization of ${\displaystyle \phi }$ to ${\displaystyle V}$, which replaces all quantifiers in ${\displaystyle \phi }$ of the form ${\displaystyle \forall x}$ and ${\displaystyle \exists x}$ by ${\displaystyle \forall x{\in }V}$ and ${\displaystyle \exists x{\in }V}$, respectively.

Relation to Zermelo–Fraenkel set theory

Let ${\displaystyle L_{\{\in \))}$ be the language of formulas that do not mention ${\displaystyle V}$.

In 1959, Azriel Levy proved that if ${\displaystyle \phi }$ is a formula of ${\displaystyle L_{\{\in \))}$ and AST proves ${\displaystyle \phi ^{V))$, then ZF proves ${\displaystyle \phi }$.^[6]

In 1970, William N. Reinhardt proved that if ${\displaystyle \phi }$ is a formula of ${\displaystyle L_{\{\in \))}$ and ZF proves ${\displaystyle \phi }$, then AST proves ${\displaystyle \phi ^{V))$.^[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]

AST and category theory

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]