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]](https://cpb-us-w2.wpmucdn.com/u.osu.edu/dist/1/1952/files/2014/01/TalkAxiomSetThy-ts05xn.pdf)! 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. 



What is the strength of adding limitation of size and a simple version of reflection to Ackermann set theory?
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.


