**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][1] minus Regularity. Its easy to recover [Ackermann's schema][2] from the simple reflection rule here. Now, I want to add the following $\omega$-inference rule: 

**De-schematization rule:**
If "$\phi(x_1,..,x_n)$" is metatheoretic expression than 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)$ 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 of 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][3] 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][4] question of mine.


  [1]: https://en.wikipedia.org/wiki/Ackermann_set_theory#Axioms
  [2]: https://en.wikipedia.org/wiki/Ackermann_set_theory#4._Ackermann's_schema
  [3]: https://mathoverflow.net/a/317663/95347
  [4]: https://mathoverflow.net/q/425342/95347