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)\; ightarrow\; 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)\; ightarrow\; y\; in\; V)\; ightarrow\; 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)\; ightarrow\; y\; in\; V)\; ightarrow\; 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\; ightarrow\; x\; in\; V$:$x\; subseteq\; y\; land\; y\; in\; V\; ightarrow\; x\; in\; V$

5) Axiom of regularity for sets::$x\; in\; V\; land\; exists\; y\; (\; y\; in\; x)\; ightarrow\; exists\; y\; (\; y\; in\; x\; land\; lnot\; exists\; z\; (z\; in\; y\; land\; z\; in\; x))$

Relation to Zermelo-Frankel 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\; x\; G(x,y\_1dots,\; y\_n)$ with $forall\; x\; (x\; in\; V\; ightarrow\; G(x,y\_1dots,\; y\_n))$ and all sub-formulas of the form $exists\; x\; G(x,y\_1dots,\; y\_n)$ with $exists\; x\; (x\; in\; V\; land\; G(x,y\_1dots,\; 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$.

See also

* Axiomatic set theory
* Zermelo set theory

Bibliography

* Ackermann, Wilhelm "Zur Axiomatik der Mengenlehre" in Mathematische Annalen, 1956, Vol. 131, pp. 336--345".
* Levy, Azriel, "On Ackermann's set theory" "Journal of Symbolic Logic Vol. 24, 1959 154--166"
* Reinhardt, William, "Ackermann's set theory equals ZF" "Annals of Mathematical Logic Vol. 2, 1970 no. 2, 189--249"