Let's work with Harvey Friedman's theory ${\sf K}(W)$ as in his seminar notes "Axiomatization of Set Theory by Extensionality, Separation, and Reducibility", 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)]$$
Best Answer
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πβπ:π.