Ackermann set theory

This article is about the mathematical theory of sets. For other uses, see Ackermann (disambiguation).

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

The language

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

The axioms

The axioms of AST are the following:

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

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

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

Relation to Zermelo–Fraenkel set theory

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

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

In 1970, William N. Reinhardt proved that if $\phi$ is a formula of $L_{\{\in \}}$ and ZF proves $\phi$, then AST proves $\phi ^{V}$.

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.

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".

See also

• Foundations of mathematics
• Zermelo set theory
• Alternative set theory