What is the strength of adding limitation of size and a simple version of reflection to Ackermann set theory?

Question

The following theory is formulated in first order predicate logic with extra-logical primitives of equality $``="$, membership $``\in"$, and a single primitive constant symbol $V$ denoting the class of all sets.

The axioms are those of first order identity theory +

1. Extensionality: $\forall x (x \in a \leftrightarrow x \in b) \to a=b$

2. Class comprehension: if $\varphi(y)$ is a formula in which the symbol $``y"$ occurs free, then all closures of: $\exists x \forall y (y \in x \leftrightarrow y \in V \wedge \varphi(y))$ are axioms.

3. Reflection: if $\varphi(y, x_1,..,x_n)$ is a formula in $FOL(=,\in)$, in which only $y,x_1,..,x_n$ occur free, then:

$$\forall x_1,..,x_n \in V \\ [\exists y (\varphi(y,x_1,..,x_n)) \to \exists y \in V (\varphi(y,x_1,..,x_n))]$$

is an axiom

4. Super-transitive: $x \in V \wedge y \subset x \to y \in V$

/

This system would interpret the whole of Ackermann's set theory [Harvey Friedman]! Yet to me it looks more elegant than Ackermann's. However my question here is that if we replace the last axiom by a limitation of size axiom which states that $V$ is a class of all subsets of it that are strictly smaller than it in cardinality, i.e. formally this is:

4. Limitation of Size: $\forall x (x \in V \leftrightarrow x \subset V \wedge |x|<|V| )$

then how much this would increase the consistency strength of this theory?

I mean this would increase the strength beyond $ZFC$ and $MK$, since $V$ would be inaccessible, and this is describable in a first order logic formula, and so by reflection there would exist a set in $V$ that is inaccessible.

Answer 1

Let me denote as $\mathsf{K}(V)$ your system 1.+2.+3.+Super Transitivity. And as $\mathsf{K}^{+}(V)$ your system 1.+2.+3.+Limitation of size.

Note that the well-founded part translation gives an interpretation of $\mathsf{K}(V)+\mathsf{Foundation}$ in $\mathsf{K}(V)$ and $\mathsf{K}^+(V)+\mathsf{Foundation}$ in $\mathsf{K}^+(V)$. Hence we equivalently could calculate the consistency strength of the versions of the systems with Foundation.

The theory $\mathsf{K}^{+}(V)+\mathsf{Foundation}$ proves the same pure set-theoretic sentences as the theory $\mathsf{ZF}+\mathsf{M}$, where the scheme $\mathsf{M}$ is "any first-order definable club on the class $On$ contains a strongly inaccessible". Formally, $\mathsf{M}$ is the scheme $$\forall \alpha\in On \exists \beta>\alpha\; \varphi(\beta)\land \forall \alpha\in On(\forall \beta<\alpha\exists \gamma\in[\beta,\alpha)\; \varphi(\gamma)\to \varphi(\alpha))\to \exists \kappa(\varphi(\kappa)\land \mbox{``$\kappa$ is strongly inaccessible''}).$$ The intended models of the theory $\mathsf{ZF}+\mathsf{M}$ are $\mathsf{V}_{\kappa}$, where $\kappa$ is a Mahlo cardinal (in the same way the intended models of $\mathsf{ZF}$ are $\mathsf{V}_{\kappa}$, where $\kappa$ is strongly inaccessible).

From Fiedman we know that $\mathsf{K}(V)+\mathsf{Foundation}$ proves all the axioms of $\mathsf{ZF}$. Let us prove that $\mathsf{K}^{+}(V)+\mathsf{Foundation}$ proves all the instances of $\mathsf{M}$ (in the language without $V$). By reflection principle it is enough to prove in $\mathsf{K}^{+}(V)+\mathsf{Foundation}$ that $\mathsf{M}$ holds only for classes $C$ that are given by a pure set-theoretic formula with parameters from $V$. Note that for any pure set-theoretic formula $\varphi(\vec{x})$ the theory $\mathsf{K}(V)\vdash\vec{x}\in V\to (\varphi^V(\vec{x})\leftrightarrow\varphi(\vec{x}))$. Thus $C$ is unbounded in $V\cap On$. Hence $(V\cap On)\in C$. Therefore, $C$ contains an inaccessible.

Recall the standard fact that for any finite family of first-order formulas $\varphi_i(\vec{x}_i)$ the theory $\mathsf{ZF}$ proves that there exists $\alpha$ such that $V_{\alpha}$ reflects all $\varphi_i$, e.g. $\forall \vec{x}_i\in V_{\alpha}\;(\varphi_i(\vec{x}_i)\leftrightarrow \varphi_i^{V_\alpha}(\vec{x}_i))$. Observe that moreover for any finite family of first-order formulas closed under subformulas $\mathsf{ZF}$ proves that the class of all $\alpha$ s.t. $V_{\alpha}$ reflects all the formulas from the family is a club. Hence $\mathsf{ZF}+\mathsf{M}$ proves that any finite family of formulas is reflected on an inaccessible cardinal. Now assume $\mathsf{K}^{+}(V)+\mathsf{Foundation}$ proves some pure set-theoretic sentence $\psi$. Let consider all the family of all $\varphi_i(\vec{x})$ from the instances of reflection used in the proof. To prove $\psi$ in $\mathsf{ZF}+\mathsf{M}$ we interpret $V$ as an inaccessible cardinal that reflects all $\varphi_i$'s.