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 consists of one binary relation and one constant . We will write for. The intended interpretation of is that the object is in the class. The intended interpretation of 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
1) Axiom of extensionality:
2) Class construction axiom schema: Let be any formula which does not contain the variable free.
3) Reflection axiom schema: Let be any formula which does not contain the constant symbol or the variable free. If then
4) Completeness axioms for
5) Axiom of regularity for sets:

Relation to Zermelo–Fraenkel set theory

Let be a first-order formula in the language . Define the "restriction of to the universe of sets" to be the formula which is obtained by recursively replacing all sub-formulas of of the form with and all sub-formulas of the form with.
In 1959 Azriel Levy proved that if is a formula of and A proves, then ZF proves
In 1970 William Reinhardt proved that if is a formula of and ZF proves, then A proves.

Ackermann set theory and Category theory

The most remarkable feature of Ackermann set theory is that, unlike Von Neumann–Bernays–Gödel set theory, a proper class can be an element of another proper class.
An extension of Ackermann set theory 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".