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$
Comprehension: $\exists x \forall y \, (y \in x \leftrightarrow y \in W \land \varphi)$; if $x$ doesn't occur free in formula $\varphi$.
Heredity: $(x \in y \lor x \subseteq y) \land y \in W \to x \in W$
Reflection: if $\varphi$ is a formula in ${\sf FOL} (=,\in)$, with all its free variables among "$x,\vec{p}$ "; then: $$\vec{p} \in W \land \exists x ( \varphi) \to \exists x \in W(\varphi)$$
The above is basically Ackermann's set theory minus Regularity. It's easy to recover Ackermann's schema from the simple reflection scheme here. Now, I want to add the following $\omega$-inference rule:
De-schematization rule: If "$\phi(x_1,..,x_n)$" is a metatheoretic expression that ranges over all formulas in $\sf FOL(=,\in)$ having exactly "$x_1,..,x_n$" as free variables, and if $S_{\phi}$ is a metatheoretic expression in which "$\phi(x_1,..,x_n)$" occurs, and if $S_{\Phi}$ is the formula in $\sf FOL(=,\in)$ that results from merely replacing each "$\phi(x_1,..,x_n)$" occurrence in $S_{\phi}$ by "$\langle x_1,..,x_n\rangle \in \Phi$", [where $\langle x_1,..,x_n \rangle $ is the $n$-tuple of the appearing $x_i$'s, and $\langle x_1\rangle =x_1$]; and if $S_{ \phi | \varphi}$ is the $\sf FOL(=,\in)$ formula that results from substituting each occurrence of "$\phi(x_1,..,x_n)$" in $S_\phi$ by the $\sf FOL(=,\in)$ formula $\varphi(x_1,..,x_n)$. Then:
$ \underline { \text{if for each } \varphi:\ \vdash (S_{\phi | \varphi})^W} \\ \vdash \forall \Phi \subseteq W^n: (S_{\Phi})^W$
Where $W^n= \{\langle x_1,..,x_n\rangle \mid x_1,..,x_n \in W\}$. And $ (\psi)^W$ is the formula resulting from merely bounding each quantifier in $\psi$ by $W$.
/
The de-schematization rule is an $\omega$-rule, it takes a schema as an input, and outputs a single sentence.
This rule is strong! Ackermann set theory doesn't prove that all set sized subsets of $W$ are sets, but here by simply de-schematizing Replacement, this would be proved, and so this theory would prove the following schema when relativized to $W$: $$\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 \kappa \text { is strongly inaccessible}).$$
But, now de-schematize this and we get $On^W$ being a Mahlo, but by then this would get reflected inwardly in $W$, so we get $n$-Mahlo's , and so on.. etc.
How far this can go?
Closely related is this question of mine.
