Ackermann set theory

Ackermann set theory is a version of axiomatic set theory proposed by Wilhelm Ackermann in 1956.

The language

Ackermann set theory is formulated in first-order logic. The language $L_{A}$ consists of one binary relation $\in$ and one constant $V$ (Ackermann used a predicate $M$ instead). We will write $x\in y$ for $\in (x,y)$ . The intended interpretation of $x\in y$ is that the object $x$ is in the class $y$ . The intended interpretation of $V$ is the class of all sets.

The axioms

The axioms of Ackermann set theory, collectively referred to as A, consists of the universal closure of the following formulas in the language $L_{A}$

1) Axiom of extensionality:

\forall x\forall y(\forall z(z\in x\leftrightarrow z\in y)\rightarrow x=y).

2) Class construction axiom schema: Let $F(y,z_{1},\dots ,z_{n})$ be any formula which does not contain the variable $x$ free.

\forall y(F(y,z_{1},\dots ,z_{n})\rightarrow y\in V)\rightarrow \exists x\forall y(y\in x\leftrightarrow F(y,z_{1},\dots ,z_{n}))

3) Reflection axiom schema: Let $F(y,z_{1},\dots ,z_{n})$ be any formula which does not contain the constant symbol $V$ or the variable $x$ free. If $z_{1},\dots ,z_{n}\in V$ then

\forall y(F(y,z_{1},\dots ,z_{n})\rightarrow y\in V)\rightarrow \exists x(x\in V\land \forall y(y\in x\leftrightarrow F(y,z_{1},\dots ,z_{n}))).

4) Completeness axioms for $V$

x\in y\land y\in V\rightarrow x\in V

(sometimes called the axiom of heredity)

x\subseteq y\land y\in V\rightarrow x\in V.

5) Axiom of regularity for sets:

x\in V\land \exists y(y\in x)\rightarrow \exists y(y\in x\land \lnot \exists z(z\in y\land z\in x)).

Relation to Zermelo–Fraenkel set theory

Let $F$ be a first-order formula in the language $L_{\in }=\{\in \}$ (so $F$ does not contain the constant $V$ ). Define the "restriction of $F$ to the universe of sets" (denoted $F^{V}$ ) to be the formula which is obtained by recursively replacing all sub-formulas of $F$ of the form $\forall xG(x,y_{1}\dots ,y_{n})$ with $\forall x(x\in V\rightarrow G(x,y_{1}\dots ,y_{n}))$ and all sub-formulas of the form $\exists xG(x,y_{1}\dots ,y_{n})$ with $\exists x(x\in V\land G(x,y_{1}\dots ,y_{n}))$ .

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

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