# ZFC + $\exists$ Standard model $\rightarrow$ Con(ZFC + $\exists \omega$-model)

$ZFC + \exists V_\alpha$ model of $ZFC \vdash Con(ZFC + \exists$ transitive standard model of $ZFC)$

and then

$ZFC + \exists$ transitive standard model of $ZFC \vdash Con(ZFC + \exists \omega-model$ of $ZFC)$

For the first one :

We can always find a countable extentional $M \subset V_\alpha$ elementary equivalent to $V_\alpha$. Let $M'$ be the mostowski collapse of $M$. $M' \approx M$ so $M'$ is model of ZFC. And because $M'$ is countable and transitive then $M' \in V_\alpha$ (since $H_{\omega_1} \subset V_{\omega_1}$ and $\alpha$ is surely far larger than $\omega_1$).

So $V_\alpha$ is the model of '$\exists$ a standard transitive model of ZFC'.

For the second one :

I don't really know how to do it... Does anyone have an idea ?

-
I'm not quite sure about the question. E.g. for (1), are you trying to prove that $(ZFC + (\exists a)(V_\alpha \vDash ZFC)) \vdash \mathrm{Con}(ZFC + (\exists x)(\text{x is a countable transitive model of ZFC}))$, or are you trying to prove in the metatheory that any model of $ZFC + (\exists a)(V_\alpha \vDash ZFC)$ can be used to create a model of $ZFC + (\exists x)(\text{x is a countable transitive model of ZFC})$? The former is done, essentially, by formalizing the proof of the latter in ZFC. –  Carl Mummert Apr 18 '11 at 21:49
sorry, It was confusing, I fixed it. I want to do what you mention first. –  Archimondain Apr 18 '11 at 22:12

Part 1 is correct. [And note that we get more: For example, your $M'$ in fact is a model of Con(ZFC+there is a transitive model of ZFC).]
For part 2: The statement "There is an $\omega$-model of ZFC" is $\Sigma^1_1$: Note that if there is an $\omega$-model, there is a countable one (take a countable elementary substructure), and now we can express this by saying that "there is a real $x$ coding a model of ZFC, and there is a real $y$ coding an order isomorphism of $\omega$ onto the natural numbers of the model coded by $x$".
Mostowski's absoluteness theorem gives us that any transitive model of ZFC is correct about $\Sigma^1_1$ statements (see Section 13 of Kanamori's book, for example). In particular, your transitive model is a model of the statement that there is an $\omega$-model.
I don't understand what you mean, but I ll have a look at what $\Sigma_1^1$ means. Somehow I managed something else (probably equivalent) : Any standard model is also an $\omega$-model, so assuming $Con(ZF)$, any $\omega$-model is also a model of $Con(ZF)$ (otherwise we would have a standard proof of 0=1, which is impossible assuming Con(ZF)). So by completness theorem, our standard model $M$ is model of $\exists (N,E) \vDash ZFC$. I just don't see why $(N,E)$ would be an $\omega$-model, but this is a good start I think ;) –  Archimondain Apr 18 '11 at 22:03
Archimondian: the problem with your approach is the following: Assume only that there is an $\omega$-model $M$. Exactly the argument you suggest gives you that $M$ is a model of Con(ZFC), so it contains models of ZFC. But certainly we cannot expect those models to be $\omega$-models, or we contradict second incompleteness. So this approach cannot succeed. We need in the case you are interested in to use some some additional absoluteness fact that allows us to conclude that we have not just a model but an $\omega$-model. $\Sigma^1_1$-absoluteness does the trick in this case. –  Andres Caicedo Apr 18 '11 at 22:38
Kanamori's book is a good place to look this up; I think Jech also explains this material carefully. The argument is relatively simple: $\Sigma^1_1$ statements are statements of the form "There is a real $x$ such that $\phi(x)$", where $\phi$ is recursive. The key insight is that this is equivalent to saying that certain trees have branches, but ill-foundedness of trees is absolute. –  Andres Caicedo Apr 18 '11 at 22:40
Well, I am a bit disappointed with the $\Sigma_1^1$ thing, it seems like a there is a big connection I did not suspected at all between 'set theory (independance proof)' and 'descriptive set theory'. (and so a lot of work to do in order to get all of it...). Thanks a lot for your answer. I'll have a look at kanamori's book. –  Archimondain Apr 18 '11 at 22:51