What is the consistency strength of this kind of reflection principle?

Question

If $\psi$ is a predicate that is definable in $FOL(\in,=)$ by a formula from parameters in $V$, then if $\psi$ hold of the class $\small ORD$ of all ordinals in $V$, then the class of all cardinals in $V$ satisfying $\psi$ is non empty and is isomorphic on membership with $\small ORD$

Formally this is: $\psi(\small ORD) \to \forall x (x = \{y| \ y \text{ is a cardinal } \wedge \psi(y)\} \to x \neq \emptyset \wedge x \cong \small ORD)$

Now this axiom scheme is to be added on top of axioms of the following theory formulated in 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 +

1. Extensionality: $\forall x (x \in a \leftrightarrow x \in b) \to a=b$
2. Foundation over all classes: $\exists m \in x \to \exists y \in x (y \cap x = \emptyset)$
3. Class comprehension axiom: if $\phi(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 \phi(y))$ are axioms.

Define $\{|\}: x=\{y|\phi(y)\} \iff \forall y (y \in x \leftrightarrow y \in V \wedge \phi(y))$

4. Transitivity: $x \in V \wedge y \in x \to y \in V$

5. Supertransitivity: $x \in V \wedge y \subseteq x \to y \in V$

6. Pairing: $a,b \in V \to \{a,b\} \in V$

7. Set Union: $a \in V \to \{x| \exists y \in a (x \in y)\} \in V$

8. Power: $a \in V \to \{x| x \subseteq a\} \in V$

9. Limitation of size: $|x| < |V| \wedge x \subset V \to x \in V$

Where $``||"$ denotes cardinality function defined in the usual manner.

Now its clear that this theory goes beyond $ZFC$, since $\small ORD$ would provably be a regular cardinal and so the set of all regular cardinals in $ORD$ must be isomorphic on membership with $ORD$, and so we must have inaccessible cardinals in $ORD$, actually it is even simpler than that, simply take the property of being "inaccessible cardinal" which is definable in the pure language of set theory, clearly $ORD$ fulfills that, so there must be an inaccessible cardinal in $ORD$. However it is not clear to me how far this theory can go to?

Question: what is the consistency strength of this theory?

Answer 1

I claim that this is equiconsistent with "$ORD$ is Mahlo" (This is not the same as $Ord$ being actually Mahlo, as I have explained elsewhere). It turns out "$ORD$ is Mahlo" is a natural limit point for these kind of Ackermann/$KM$ based theories. Let $T$ be your theory.

First, the easy part. The consistency strength of "$ORD$ is Mahlo" $\ge$ the consistency strength of $T$. Let $C=\{\alpha|V_\alpha\prec W\}$, where $W=\{x|x=x\}$. Note that if $\alpha\in C$ and $\phi(\alpha)$, then $\exists\beta(\beta\gt\alpha\land\phi(\beta))$. The reason for this is that else $\psi(\alpha)\leftrightarrow\beta\text{ is the largest } \beta\text{ such that }\phi(\beta)$ would be a definition of $\alpha$, and so $V_\alpha\vDash\exists x(\psi(x))$, which is a contradiction. Now, if $\phi(\alpha)$ with $\alpha\in C$, then $\phi(\alpha)\land\alpha\text{ is a cardinal}$ and so $V_\alpha\vDash\forall\eta(\exists\beta\gt\eta(\phi(\beta\land\beta\text{ is a cardinal}))$. Therefore, whenever $\kappa$ is inaccessible reflecting $V_\kappa\vDash T$, and the existsence of an inaccessible reflecting cardinal is equiconsistent with "$ORD$ is Mahlo."

Second, the hard part. The consistency strength of $T\ge$ the consistency strength of "$ORD$ is Mahlo." Let $C=\{\alpha|\phi(\alpha,p)\}$, and let $C^V=\{\alpha|\phi^V(\alpha,p)\}\cap Ord$ be club in $Ord$. Then you can see $\{\alpha|\phi^V(\alpha,p)\}$ is club (In the real class of ordinals); in particular $\phi^V(Ord,p)\land Ord\text{ is regular}$. Then we can find a non-empty class of regular $\kappa\in C^V$, and so $\phi^V$ when $ZFC+ORD\text{ is Mahlo}\vdash\phi\rightarrow\phi^V$. Therefore, if $M\vDash T$ then $V^M\vDash ZFC+ORD\text{ is Mahlo}$