The following theory is a modification of Harvey Friedmann $\sf K(W)$ theory.

Language: first order logic with equality, membership, and a constant symbol $W$.

Axioms:

Extensionality: $\forall z \, (z \in x \leftrightarrow z \in y) \to x=y$

Subworld Replacement: if $\varphi(x,y,a,\vec{p})$ is a formula that doesn't use "$b$", having all of its free variables among "$x,y,a,\vec{p}$"; then: $$ \forall x \in a \exists z \forall y \, [ \varphi(x,y,a,\vec{p}) \to y=z \land (z \in a \lor z \in W)] \\\land a \in W \\ \to \exists b \in W : b=\{y\mid \exists x \in a \, \varphi(x,y,a,\vec{p})\}$$

Reducibility: if $\phi$ is a formula in ${\sf FOL} (=,\in)$, with all its free variables among "$x,\vec{p}$ "; then: $$\vec{p} \in W \land \exists x ( \phi) \to \exists x \in W(\phi)$$

Foundation: as in $\sf ZFC$.

Choice: as in $\sf ZFC$.

/

This blows up its strength to $\sf ORD \ is \ Mahlo$. (see here for a proof of that result in a related theory, where I don't see the extra-class features related to that theory being used in the proof of that result)

Is this theory bi-interpretable with $\sf ZFC + ORD \ is \ Mahlo$? The latter is the scheme: $$\forall \alpha \exists \beta>\alpha\; \varphi(\beta)\land \\\forall \alpha(\forall \beta<\alpha\exists \gamma\in[\beta,\alpha)\; \varphi(\gamma)\to \varphi(\alpha))\\\to \\\exists \kappa(\varphi(\kappa)\land \kappa \text { is strongly inaccessible}).$$ Where $\alpha $ range over ordinals.

The following theory is a modification of Harvey Friedman $\sf K(W)$ theory.

Language: first order logic with equality, membership, and a constant symbol $W$.

Axioms:

Extensionality: $\forall z \, (z \in x \leftrightarrow z \in y) \to x=y$

Subworld Replacement: if $\varphi(x,y,a,\vec{p})$ is a formula that doesn't use "$b$", having all of its free variables among "$x,y,a,\vec{p}$"; then: $$ \forall x \in a \exists z \forall y \, [ \varphi(x,y,a,\vec{p}) \to y=z \land (z \in a \lor z \in W)] \\\land a \in W \\ \to \exists b \in W : b=\{y\mid \exists x \in a \, \varphi(x,y,a,\vec{p})\}$$

Reducibility: if $\phi$ is a formula in ${\sf FOL} (=,\in)$, with all its free variables among "$x,\vec{p}$ "; then: $$\vec{p} \in W \land \exists x ( \phi) \to \exists x \in W(\phi)$$

Foundation: as in $\sf ZFC$.

Choice: as in $\sf ZFC$.

/

This blows up its strength to $\sf ORD \ is \ Mahlo$. (see here for a proof of that result in a related theory, where I don't see the extra-class features related to that theory being used in the proof of that result)

Is this theory bi-interpretable with $\sf ZFC + ORD \ is \ Mahlo$? The latter is the scheme: $$\forall \alpha \exists \beta>\alpha\; \varphi(\beta)\land \\\forall \alpha(\forall \beta<\alpha\exists \gamma\in[\beta,\alpha)\; \varphi(\gamma)\to \varphi(\alpha))\\\to \\\exists \kappa(\varphi(\kappa)\land \kappa \text { is strongly inaccessible}).$$ Where $\alpha $ range over ordinals.