[EDIT] The criteria for a founding theory of mathematics, especially if it uses large cardinal axioms that I want to refer to are those of Harvey Friedman's 2000 criteria given in pages 5-6 of the referred article of his, see section: circumstances surrounding actual adoption of new axioms. Also in connection to that I will refer to Muller's 2000 criteria for a theory that is sufficient to found mathematics and Category theory. A similar theory is one that I've posted lately to this section of StachExchange under title:Does Reflective Set Theory “RfST” fulfill the requirements of founding Category Theory and Mathematics?. However this theory is of course a different one.
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. Actually we have a more elegant axiom system here, 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 ALL subsets 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 ∃y (x ∈ y)
Class Comprehension: if φ is a formula in which x doesn't occur free, from parameters x1,x2 then:
∀x1,x2 ∃!x ∀y [y ∈ x <-> φ ∧ element(y)];
is an axiom.
Define: x=V iff ∀y [y ∈ x <-> element(y)]
Subworld: W ∈ V
Reflection: if φ is a formula that doesn't use the symbol W, from parameters x1,x2, then:
∀x1,x2 in W [∃x ∈ V(φ) -> ∃x (φ ∧ ∀y ⊂ x (y ∈ W))] ;
are axioms.
Choice Foundation: x ≠ ∅ -> C(x) ∈ x ∧ ∀y ∈ x (y ∉ 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. The idea is that the piece whereby this theory interpret the Category of sets as required by Muller doesn't by itself increase the strength of this theory about sets. However the set section of this theory (i.e. the W world) is itself strong. 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 accepted natural ways 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.
The large difference between the situation with this theory and the one with the prior theory posted to this group is that the first one fulfills all of Muller's criteria, i.e. the strength is not going beyond that of ZFC, while here this goes far beyond that. However I'd argue in a relative manner, that the increment in strength in this theory was not due to the attempt to found the Category of sets of this theory in this theory, no! it is native to contemplation about sets themselves, and so in a "relative" sense this theory can also be regarded as abiding by Muller's criteria.
Question: How far this theory is from Harvey Friedman and Muller's criteria, especially as compared with ZFC's stance from those criteria?
