Is "ZFC + Omega rule for finite sets" a complete theory?

Question

Omega rule for finite sets $\omega^{fin}$: if $\phi(y), \psi(y)$ are formulas in one free variable symbol $y$, then:

From:

for $ n=0,1,2,3,...; \text { we have: } \forall y \ [y=\{x_1,...,x_n\} \wedge \phi(y) \to \psi(y)]$

We Infer

$\forall y \ [ finite(y) \wedge \phi(y) \to \psi(y)]$

Question: Is $ZFC + \omega^{fin}$ complete?

The idea is that if we take $\phi(y)$ to be "y is a finite von Neumann", then clearly this would be the Omega rule for standard naturals, and since ZFC interprets PA, then we'd have PA + Omega rule for standards. But would that be sufficient enough in itself to make the above theory complete?

Answer 1

Unless I'm wildly misunderstanding your question, the answer is no - any $\omega$-model of ZFC automatically satisfies the $\omega^{fin}$-rule, but some $\omega$-models of ZFC satisfy CH and others don't.

More generally, we can develop forcing over arbitrary countable models of ZFC (and indeed, arbitrary models, if we use the Boolean-valued approach rather than the actual-generic-extension approach); since forcing doesn't add new natural numbers, any forcing extension of a model satisfying $\omega^{fin}$ will continue to satisfy $\omega^{fin}$.