Does $\omega$-consistency of ZF imply $\omega$-consistency of ZFC

Question

Does $\omega$-consistency of ZF imply $\omega$-consistency of ZFC?

Are there any related results where $\omega$-consistency of some intuitionistic logic implies $\omega$-consistency of ZFC?

Does this question even make sense to state?

Answer 1

Yes, since the constructible universe $L$ is an $\omega$-interpretation (interpretation preserving natural numbers) of $\mathsf{ZFC}$ in $\mathsf{ZF}$. The question does make sense: the $\omega$-consistency of a theory $T\supseteq \mathsf{ZF}$ (usually) is the assertion that for any formula $\varphi(x)$ theory $T$ couldn't simultaneously prove $\exists x\in \omega (\lnot\varphi(x))$ and all $\varphi(\underline{n})$, for individual natural numbers $n$. You could formulate $\omega$-consistency in the language of first-order arithmetic. And the construction that I have mentioned above in fact shows that over $\mathsf{PRA}$ the $\omega$-consistencies of $\mathsf{ZFC}$ and $\mathsf{ZF}$ are equivalent.