Inmathematics andlogic,Ackermann set theory (AST, also known as[1]) is an axiomaticset theory proposed byWilhelm Ackermann in 1956.[2]
AST differs fromZermelo–Fraenkel set theory (ZF) in that it allowsproper classes, that is, objects that are not sets, including a class of all sets.It replaces several of the standard ZF axioms for constructing new sets with a principle known as Ackermann's schema. Intuitively, the schema allows a new set to be constructed if it can be defined by a formula which does not refer to the class of all sets.In its use of classes, AST differs from other alternative set theories such asMorse–Kelley set theory andVon Neumann–Bernays–Gödel set theory in that a class may be an element of another class.
William N. Reinhardt established in 1970 that AST is effectively equivalent in strength to ZF, putting it on equal foundations. In particular, AST isconsistentif and only if ZF is consistent.
AST is formulated infirst-order logic. Thelanguage of AST contains onebinary relation denotingset membership and oneconstant denoting theclass of all sets. Ackermann used a predicate instead of; this is equivalent as each of and can be defined in terms of the other.[3]
We will refer to elements of assets, and general objects asclasses. A class that is not a set is called a proper class.
The following formulation is due to Reinhardt.[4]The five axioms include twoaxiom schemas.Ackermann's original formulation included only the first four of these, omitting theaxiom of regularity.[5][6][7][note 1]
If two classes have the same elements, then they are equal.
This axiom is identical to theaxiom of extensionality found in many other set theories, including ZF.
Any element or a subset of a set is a set.
For any property, we can form the class of sets satisfying that property. Formally, for any formula where is notfree:
That is, the only restriction is that comprehension is restricted to objects in. But the resulting object is not necessarily a set.
For any formula with free variables and no occurrences of:
Ackermann's schema is a form of set comprehension that is unique to AST. It allows constructing a new set (not just a class) as long as we can define it by a property thatdoes not refer to the symbol. This is the principle that replaces ZF axioms such as pairing, union, andpower set.
Any non-empty set contains an element disjoint from itself:
Here, is shorthand for. This axiom is identical to theaxiom of regularity in ZF.
This axiom is conservative in the sense that without it, we can simply use comprehension (axiom schema 3) to restrict our attention to the subclass of sets that are regular.[4]
Ackermann's original axioms did not include regularity, and used a predicate symbol instead of the constant symbol.[2] We follow Lévy and Reinhardt in replacing instances of with. This is equivalent because can be given a definition as, and conversely, the set can be obtained in Ackermann's original formulation by applying comprehension to the predicate.[3]
Inaxiomatic set theory, Ralf Schindler replaces Ackermann's schema (axiom schema 4) with the followingreflection principle:for any formula with free variables,
Here, denotes therelativization of to, which replaces allquantifiers in of the form and by and, respectively.[8]
Let be the language of formulas that do not mention.
In 1959,Azriel Lévy proved that if is a formula of and AST proves, thenZF proves.[3]
In 1970, William N. Reinhardt proved that if is a formula of and ZF proves, then AST proves.[4]
Therefore, AST and ZF are mutuallyinterpretable inconservative extensions of each other. Thus they areequiconsistent.
A remarkable feature of AST is that, unlikeNBG and its variants, a proper class can be an element of another proper class.[7]
An extension of AST forcategory theory called ARC was developed by F.A. Muller. Muller 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".[9]