Return to Answer

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.

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 Friedman 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.

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{ZFC}+\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{ZFC}+\mathsf{M}$ are $\mathsf{V}_{\kappa}$, where $\kappa$ is a Mahlo cardinal (in the same way the intended models of $\mathsf{ZFC}$ 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{ZFC}$. 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{ZFC}$ 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{ZFC}$ proves that the class of all $\alpha$ s.t. $V_{\alpha}$ reflects all the formulas from the family is a club. Hence $\mathsf{ZFC}+\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{ZFC}+\mathsf{M}$ we interpret $V$ as an inaccessible cardinal that reflects all $\varphi_i$'s.

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.

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{ZFC}+\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 $$\exists \alpha\in On\; \varphi(\alpha)\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{ZFC}+\mathsf{M}$ are $\mathsf{V}_{\kappa}$, where $\kappa$ is a Mahlo cardinal (in the same way the intended models of $\mathsf{ZFC}$ 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{ZFC}$. 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{ZFC}$ 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{ZFC}$ proves that the class of all $\alpha$ s.t. $V_{\alpha}$ reflects all the formulas from the family is a club. Hence $\mathsf{ZFC}+\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{ZFC}+\mathsf{M}$ we interpret $V$ as an inaccessible cardinal that reflects all $\varphi_i$'s.

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{ZFC}+\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{ZFC}+\mathsf{M}$ are $\mathsf{V}_{\kappa}$, where $\kappa$ is a Mahlo cardinal (in the same way the intended models of $\mathsf{ZFC}$ 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{ZFC}$. 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{ZFC}$ 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{ZFC}$ proves that the class of all $\alpha$ s.t. $V_{\alpha}$ reflects all the formulas from the family is a club. Hence $\mathsf{ZFC}+\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{ZFC}+\mathsf{M}$ we interpret $V$ as an inaccessible cardinal that reflects all $\varphi_i$'s.