On mathoverflow I've posed the question in the title in connection to Muller's 2001 criteria for a founding theory of mathematics, which largely raised in connection to Category theory [see here]. Some aspects of this question are mathematical, specifically those concerning the consistency of RfST and whether the Counter-Reflection schema adds un-necessary strength beyond what is stipulated in Muller's criteria.
Here I want to discuss the philosophical aspect, that is: how far that theory fits Muller's criteria, and how far it's from H.Friedman's criteria, (pages:5-6) for founding mathematics (which largely raised in connection with large cardinal axioms)?
I personally think that RfST can prove ℘^ω(V), i.e. the union of all finite power iterations of V.
Muller's argument seem to suggest that this is not needed, specifically note this quote from him:
The conclusion of this brief informal analysis coincides partly with an assertion of Fraenkel, Bar-Hillel, Levy ´ and Van Dalen [1973, p. 143]: Category Theory involves only objects which are members of the classes V, ℘V, ℘℘V, . . ., ℘nV, where V is the class of all sets and n is some fixed finite number.
[end of page 10].
And also this quote from the very next page:
What is needed and sufficient is ‘only’ a denumerable sequence of increasing cumulation sets Ψ(i1 + 1) for ℘V, Ψ(i1 + 2) for ℘2V, until Ψ(i1 + ω), but certainly no more.
Anyhow, I think this theory might construct more classes, but it is a bit more and not mindbogglingly, flabbergastingly abundant as to constitute a violation of Bourbaki.
One of the points against simply upgrading class existence to class separation axiom as to get ARC of Muller's, is that it can be attacked as ad-hoc. I don't see a clear justification for it. By doing that we are replacing a very natural principle of class existence after predicates, by the technical fix of class separation. I'd prefer class separation to be a theorem rather than an axiom. And I think the plausible basis for it lies in Counter-Reflection, i.e. it is a part of a reflection process in the opposite direction, i.e. from sets to classes, this makes matters more thematic (to conform to Friedman's terminology) and less ad-hoc.
More generally speaking I see all axioms of RfST being very natural and nicely fit what's expected of a founding set\class theory for Category theory, and for most of mathematics in general.
Reflective Set Theory RfST is formulated in mono-sorted first order predicate logic with extra-logical primitives of equality ‘‘=", membership ‘‘∈", and a single primitive constant symbol V denoting the class of all sets.
The axioms are those of first order identity theory +
- Extensionality: ∀x(x∈a ↔ x∈b) → a=b
- Class comprehension: if φ(y) is a formula in which the symbol ‘‘y" occurs free, then all closures of: ∃x∀y(y∈x ↔ y∈V ∧ φ(y)), are axioms.
- Super-Transitivity: y⊂x ∧ x∈V → y∈V
Reflection: if φ is a formula that doesn't use the symbol V, in which only y,x1,..,xn occur free, then: ∀x1,..,xn∈V[∃y(φ) → ∃y∈V(φ)], is an axiom.
Counter-Reflection: if φ is a sentence that doesn't use the symbol V, and φV is the sentence obtained by merely bounding every quantifier in φ by V, then: (φV→φ) is an axiom.
- Foundation: ∃m∈x → ∃y∈x ∀z∈x(z∉y)
- Choice: ∀m,n∈X(∄k∈m(k∈n)) → ∃Y∀x∈X(x≠∅ → ∃!y∈Y(y∈x))