# Is it consistent to add a generalization axiom on top of Ext.+Subworld Separation+Reduciblity?

Lets work with Harvey's Friedman theory $${\sf K}(W)$$, formulated in the language of set theory with a primitive constant symbol $$W$$ added, i.e. in $${\sf FOL}(\in,W)$$

Axioms:

Extensionality: $$\forall Z \, (Z \in X \iff Z \in Y) \implies \\\forall Z \, (X \in Z \iff Y \in Z)$$

Subworld Separation: $$\forall A \in W \, \exists X \in W \, \forall Y \, (Y \in X \iff Y \in A \land \phi)$$; where formula $$\phi$$ doesn't use the symbol "$$X$$".

Reducibility: if $$\phi$$ is a formula in $${\sf FOL} (\in)$$, with all parameters among "$$X,\vec{P}$$ " then: $$\forall \vec{P} \in W [ (\exists X: \phi) \implies \exists X \in W: \phi]$$

/

Which is equiconsistent with ZFC.

Is it consistent to add the following principle:

Generalization: if $$\phi$$ is a formula in $${\sf FOL} (\in)$$, with all parameters among symbols "$$X,\vec{P}$$ "; then: $$\forall \vec{P} \in W [(\forall \operatorname {infinite} X \in W: \phi) \implies \phi(W)]$$