This is a theory that I'd think deserve to have a foundational status. The axioms are very natural and short, and the theory is stronger than ZFC, yet I don't see it less natural than it at all. In some sense ZFC is seen as the maximal known naturally looking set theory, but I think this is not correct, since I argue that this set theory is as natural as ZFC, and actually have a more elegant axiom system, but this theory is much stronger than ZFC.
Informal account: this theory is a class theory, every object is a class, classes are constructed uniquely (almost naively) after formulae, as the classes of all "elements" that satisfy those formulae, i.e. following Morse-Kelley approach. Now this theory includes a sub-world denoted by W which is an element. Now Reflection would reflect any property definable in the pure set theoretic language (i.e.; doesn't use W) from parameters in W, that holds of an element, to the inside of W in a COMPLETE manner, i.e. there must be an element of W that would satisfy that property such that ALLsubsets of it are elements of W as well. Global choice and foundation also added in one axiom. This theory has a very natural genre, it is based on W being imagined as a kind of a sub-universe, and since it is a universe then it must be big, and so it cannot be captured by a property that is definable in the pure-set theoretic language from parameters inside it, i.e. it is too big to be reachable by pure set expressions from the inside of it. The Counter-Reflection axiom is a plausible extension of this theory, it would generalize the set theoretic rules inside W over all V.
FORMAL EXPOSITION Language: mono-sorted first order predicate logic with primitives of "= , in , W, C" denoting, Equality, Membership, Sub-World, and Choice, respectively; where W is a constant symbol, and C is a one place total function symbol.
Axioms: those of identity theory +
Define: element(x) iff exists y (x in y)
Class Comprehension: if phi is a formula in which x doesn't occur free, from parameters x1,x2 then:
forall x1,x2 exists! x forall y [y in x <-> phi & element(y)];
is an axiom.
Define: x=V iff forall y [y in x <-> element(y)]
Subworld: W in V
Reflection: if phi is a formula that doesn't use the symbol W, from parameters x1,x2, then:
forall x1,x2 in W [exists x in V(phi) -> exists x (phi & forall y subseteq x (y in W))] ;
are axioms.
Choice Foundation: x =/= {} -> C(x) in x & forall y in x (y not in C(x))
it would be plausible to extend this theory with a Counter-Reflection axiom, that informally means that all rules closed under W are also closed under V, formally this is:
Counter-Reflection: if phi^X denotes a sentence in which all of its quantifiers are bounded in X and X doesn't occur otherwise, then: phi^W -> phi^V; is an axiom.
/Theory definition finished.
I want to argue that this theory is as natural as ZFC. But "naturalness" is an undefined notion, its more of a feel. The strength of this theory needs to be taken into notice, it is very strong when compared to ZFC, it is much stronger than ZFC, it might go beyond Mahlo cardinals, perhaps up to zero^sharp. One wouldn't generally expect from such a theory having that simply presented axiomatics to be so strong. The end result of this theory in terms of traditionally known theories, is a theory that combines both Ackermann's set theory and Morse-Kelley set theory at the same time, both theories of which are considered as very natural theories that are almost included among the standard line of set theories. Moreover this theory satisfies all requirements given by Muller as regards being a founding theory of mathematics, since it is sufficient to found Category theory in it. I don't personally see why "natural" discourse about "sets" needs to stop at ZFC level, so I don't grant Muller's point about not going beyond ZFC's strength, the point here is that going to such strength was not the side effect of trying to found category theory in set theory, no it is thought here to be genuine of natural contemplation about sets and classes themselves, that it can found category theory is an additional merit of this theory. To me personally this theory is as natural as ZFC, it even has a simpler axiomatic exposition than that of ZFC, and even from the conceptual viewpoint the axiomatics of this theory is captured by a simple theme, that of having a sub-universe that is not reachable by pure set theoretic expressiblilty from the inside of it, which looks reasonable to me, and so its less diverge than the themes capturing axioms of ZFC. The rest of axiomatics, i.e. those of classes, choice and foundation, are pretty much the most natural way to think about sets and classes. Now Counter-Reflection is a plausible addition to this theory since it won't leave the rest of classes, i.e. those beyond W, without specifying rules for them, and rules applicable inside W are seen to generalize over the whole of the universe V of all elements, this further supports the image of W being a sub-universe functionally speaking to V, i.e. of W being subdued by V, since rules applicable to W must be part of the rules applicable to the whole universe V, which in my own opinion seems to be very natural.
ADDENDUM: a possibly nicer version is to remove subworld and write reflection as:
x1, x2 in W & exists x subset W(phi(x)) -> exists x in W (phi(x))
if phi doesn't use W.
and add an axiom of size limitation on W, i.e.
x subset W & |x| <|W| <-> x in W
This would easily interpret MK.
See the following more rercent update
Reflective Class Theory "RCT":
Informal account: this theory is a class theory, every object is a class, classes are constructed uniquely after formulae, as the classes of all "elements" that satisfy those formulae. Now this theory includes a sub-world denoted by W. Reflection would reflect any property definable in the pure set theoretic language (i.e.; doesn't use W) from parameters in W, that hold of a subset of W, to the inside of W, i.e. there must be an element of W that would satisfy that property. Foundation also added. A counter-reflection axiom to the effect that generalizes rules closed over W to be closed over V. This theory has two versions of the last axiom, one is that W is supertransitive, and the other stronger version is a limitation of size axiom stating that for all subsets of W, their membership in W is equivalent to them being strictly smaller than W. Clearly the last axiom would let this theory interpret ZFC, since the class of all elements of W that are hereditarily elements of W would be a Von Neumann Hierarchy of sets. This theory of course pushes further into the large cardinal world. It both interprets MK and Ackermann set theory.
FORMAL EXPOSITION Language: mono-sorted first order predicate logic with primitives of ‘‘=,∈,W" denoting, Equality, Membership, Sub-World, respectively; where W is a constant symbol.
Axioms: those of identity theory +
Class Comprehension: if φ(y) is a formula in which x doesn't occur free, then all closures of:
∃!x ∀y [y∈x↔φ(y)∧∃z(y∈z)]
; are axioms.
Define: x=V⟺∀y [y∈x↔∃z(y∈z)]
Reflection: if φ(x) is a formula that doesn't use the symbol W, then all closures of:
parameters ∈W→[∃x⊆W(φ(x))→∃x∈W(φ(x))]
; are axioms.
Counter-Reflection: if φX denotes a sentence in which all of its quantifiers are bounded ∈X and X doesn't occur otherwise, then:
φW→φV
; is an axiom.
Foundation: x≠∅→∃y∈x∀z∈x(z∉y)
Plus one of two versions of axiom 5 that are:
Supertransitive: x∈W∧y⊂x→y∈W
or
Size limitation: x⊂W→(|x|<|W|↔x∈W)
/Theory definition finished.
See this site: