Lets work with Harvey's [Friedman](https://cpb-us-w2.wpmucdn.com/u.osu.edu/dist/1/1952/files/2014/01/TalkAxiomSetThy-ts05xn.pdf) 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)]$$



Is it consistent to add a generalization axiom on top of Ext.+Subworld Separation+Reduciblity?
Generalization holds in K(W). Suppose it did not, that ¬(W) holds and ∀infinite∈:.


Then ∃X((infiniteX)∧¬), since this is true when X is W. By Reducibility


∃X∈W((infiniteX)∧¬). But this contradicts the fact that ∀infinite∈:.


