Is ZFC ω-consistent over ZF?

Question

Gödel proved that if ZF is consistent, then ZFC is also consistent. He did this by showing that his constructible universe is a model of ZFC. Gödel also introduced the notion of an $\omega$-consistent theory. Has it been proved that if ZF is $\omega$-consistent, then ZFC is also $\omega$-consistent? Can already Gödel's consistency proof be extended to show this? (Or is this angle of attack unlikely to so succeed, because we don't have a corresponding completeness result for $\omega$-consistent theories, which would ensure the existence of a sufficiently well behaved model (of ZF)?)

Answer 1

Any witness of $\omega$-inconsistency of ZFC can be effectively transformed to a witness of $\omega$-inconsistency of ZF as follows. Suppose $\phi(x)$ is a formula such that for each numeral $n$, ZFC proves $\phi(n)$ and also $(\exists x \in \omega)\neg \phi(x)$. Let $\psi(x) = \phi^L(x)$ be obtained from $\phi(x)$ by restricting its quantifiers to $L$. Then for each numeral $n$, ZF proves $\psi(n)$ since ZFC theorems when relativized to $L$ are theorems of ZF. Also $L$ is transitive so $(\exists x \in L \cap \omega) \neg \psi(x)$ is equivalent (in ZF) to $(\exists x \in \omega) \neg \psi(x)$. Hence $\psi(x)$ witnesses the $\omega$-inconsistency of ZF.