The language of this theory is first order predicate calculus with extra-logical primitive symbols of ‘‘=;∈,W" , where ‘‘W" is a constant symbol.
Axioms: those for identity theory +
Extensionality: ∀A∀B:∀Z(Z∈A⇔Z∈B)⟹A=B
Define: set(X)⟺∃Y(X∈Y)
Class Comprehension: if ϕ is a formula in which Y is free, and X not free, then all closures of the following are axioms:
∃X∀Y(Y∈X⟺set(Y)∧ϕ)
Define: X={Y|ϕ}⟺∀Y(Y∈X⇔ϕ(Y))
Define: X=V⟺∀Y(set(Y)⇒Y∈X)
Foundation: ∀X:X≠∅⟹∃Y∈X(Y∩X=∅)
Pairing: ∀A,B∈V∃X∈V:X={A,B}
Define: H<W(X)⟺∀Y∈Tr.cl({X})(Y<W)
Where: Y<W⟺(∃f:Y↪W∧∄g:W↪Y)
Where ‘‘↪" signifies injection.
Tr.cl(A)stands for "the transitive closure class of A", defined in the usual manner as the intersection of all transitive classes having A as a subclass of.
A formula is said to be class theoretic formula if all of its terms are variables and only uses symbols ‘‘=,∈" as predicate symbols.
A formula is said to be set theoretic formula if it results from the mere bounding of all of quantifiers in a class theoretic formula by the symbol V
Reflection: if ϕ is a set theoretic formula whose free variable symbols are among symbols of Y,P, then:
∀P⃗ [H<W[P⃗ ]∧∀Y(ϕ(Y)⇒H<W(Y))
This theory can interpret MK [Limitation of size replaced by the axiom of: any class equinumerous to a set is a set] in a straightforward manner. So it proves the consistency of ZFC via MK. I don't think that foundation is necessary for that interpretation.
⟹∃X<W:X={Y|ϕ}]
I don't see an easy way to prove every class of hereditarily strictly subnumerous to Wsets (i.e. the H<W) to be a set? Which is what's needed to provide a direct interpretation of Ackermann's set theory. However, this theory can of course indirectly interpret Ackermann via interpreting MK.
How far this theory can go? What is the least large cardinal this theory cannot prove the existence of?
[Afternote] It happens that this theory (if consistent) would directly interpret Muller's theory of sets and classes, which he advocated as a foundational theory of mathematics. Also to be noted is that if we add an axiom of: H<W↪W; that is, the class of all H<W sets is subnumerous to W [thus equinumerous with W], and add an axiom of any class equinumerous with a set is a set, then global choice would be enacted over H<W, and we get to interpret directly both full MK and full Ackermann's since all subclasses of H<W would be sets. My guess is that this would add strength, though I don't know how much.
A more clean version would be change the consequent of Reflection to ∃∈W:X={Y|ϕ}
Denote this version of Reflection by Reflection*
This way we get |W|=|H<w|, and of course global
choice over W for free. Now if we add an axiom
size limitation over V like that in MK or the weaker
version of every class subnumerous to a set is a set.
Then we'll get to interpret Ackermann set theory
where classes in Ackermann would be sets in our
theory and sets in Ackermann would be H<w sets
of our theory. Of course MK is already interpreted
over all sublasses of H<w
in this version. So this version of our theory
would easily interpret both MK (full version) and
Ackermanns class theory, and also Muller's theory of
sets and classes in almost unified manner. Of course
foundation is not really needed for that interpretation
so we can do without it, so we only need five axioms
Extensionality
Class comprehension
Pairing
Limitation of size
Reflection*
The theory we get is by the way strong possibly up to
ORD is mahlo or something near that.
-----------------------------------------------------------------------------
Reflective Megethology
Language: first order predicate calculus with equality == and primitives of ∈,s∈,s where ss is a one place predicate symbol standing for "is small".
Axioms: ID axioms +
Extensionality: ∀A∀B:∀Z(Z∈A⇔Z∈B)⟹A=B
Define: set(X)⟺∃Y(X∈Y)
Class Comprehension: if ϕϕ is a formula in which YY is free, and XX not free, then all closures of the following are axioms:
Define: X={Y|ϕ}⟺∀Y(Y∈X⇔ϕ)
Define: X=V⟺∀Y(set(Y)⇒Y∈X)
Limitation of Size: X∈V⟺∄f:V↪X
Where ↪↪ signifies an "injection".
Smallness: s(X)∧(∃f:Y↪X)⇒s(Y)
Define: Hs(X)⟺∀Y∈Tr.cl({X}):s(Y)
Where ‘‘Tr.cl(A)"‘‘Tr.cl(A)" signifies the transitive closure class of A, defined in the usual manner as the intersectional class of all transitive classes having A as a subclass of them.
A formula is said to be a pure class theoretic formula if all of its terms are variables and only uses symbols ‘‘=,∈" as predicate symbols.
A formula is said to be a pure set theoretic formula if it results from the mere bounding of all of quantifiers in a class theoretic formula by the symbol V
Reflection: if ϕ is a pure set theoretic formula whose free variable symbols are among symbols of Y,P⃗ , then:
∃X∀Y(Y∈X⟺set(Y)∧ϕ)
∀P⃗ (Hs[P⃗ ]∧∀Y(ϕ⇒Hs(Y))
→∃X:s(X)∧X={Y|ϕ})
In English: any pure set theoretic formula that is closed on the hereditarily small class world, defines a small class!
Foundation: X≠∅⟹∃Y∈X(Y∩X=∅)
Now it can be easily seen that this theory does prove pairing for sets (the pair of any two sets is a set) and thus can speak of relations between any two classes. The theory proves the class Hsto be closed under pairing, union, power, and limitation of size, and also there exists an infinite set among its elements. So it satisfies all axioms of ZFC, and it can interpret a version of MK where limitation of size axiom is replaced by an axiom of replacement for sets and an axiom of choice added over sets. Also it can interpret Ackermann where classes in Ackermann's are sets here, and sets in Ackermann are hereditarily small sets here. Also Muller's extension of Ackermann is straightforwardly interpreted along the same lines since the class separation axiom is true of the set world here. Accordingly, per Muller, it can be used as a foundation for Categories, and thereby of Mathematics. Now the motivation for this theory is very appealing and it can be seen to closely parallel the intuition that David Lewis justified axioms of ZFC after, namely after respecting a size notion of smallness. (see Mathematics is Megethology), but here this is pushed further to apply to any pure set theoretic formula, so the closure of the hereditarily small sets over some pure set theoretic property would entail having a class of all sets per such a closure, that is small also, so here we have a reflective smallness notion. So, this theory can be viewed as reflectively extending Lewis's views about the notion of smallness, one may call it as Reflective Megethology. However, this theory proves to be very strong up to ORD is Mahlo, a consistency argument for this theory might be covered by the argument here. So, this theory seems to be both naturally motived and technically powerful.
Going without a new primitive
This theory uses a reflection principle similar to Ackermann but on a size notion that is definable in the language of set theory.
Define: set(X)⟺∃Y(X∈Y)
Extensionality: ∀A∀B:∀Z(Z∈A⇔Z∈B)⟹A=B
Comprehension: ∃X∀Y(Y∈X⟺set(Y)∧ϕ)
where X not free in ϕ.
Limitation of Size: X∈V⟺∄f:V↪X
‘‘↪"for "injections"; V is the class of all sets.
Foundation: X≠∅⟹∃Y∈X(Y∩X=∅)
Reflection: if ϕ1,..,ϕn are pure set theoretic formulas in which Y is free, and their parameters among symbols A,B; and if πi is the formula
‘‘∀A,B are H<W[∀Y(ϕi⇒H<W(Y))→
∃X<W∀Y(Y ∈X⇔ϕi)]"
then: ∃W:π1∧...∧πn
Where H<W is the predicate "hereditarily strictly subnumerous to W defined by the predicated classes being strictly subnumerous to W and every element of their transitive closures being also strictly subnumerous to W; and < stands for strict subnumerousity defined in the usual sense. A pure set theoretic formula means a bounded ‘‘∈V" formula whose predicates are ∈,= and its terms are variables, except V which only appears in bounding all quantified variables in it.
The claim is that this theory can interpret Ackermann and Morse-Kelley set theory [with modified size limitation axiom of every class equinumerous to a set is a set], and also Muller's extension of Ackermann's. Also, I think it interprets Tarski–Grothendieck set theory (TG). I'm not really sure if it reaches up to the consistency of ORD is Mahlo which is the consistency strength of adding size limitation principle on sets in Ackermann set theory. It does all of that in the usual language of set theory (first order logic with equality and membership).