Kunen's use of Countable Transitive Models Hi,
I have a doubt concerning Kunen's exposition of forcing in his classical book (arguably $the$ book on forcing). When dealing with Countable Transitive Models to set up the forcing machinery, Kunen is always very careful with letting this C.T.M. to model $only$ finite fragments of ZFC. I recently read in one of the answers to this MO question that the point is that CON(ZFC) cannot prove the existence of countable transitive models of ZFC, and I don't understand why not... wouldn't this be just a matter of taking a set model for ZFC (by consistency of ZFC, which we are assuming), which without loss of generality can be countable (by L\"owenheim-Skolem) and then apply the Mostowski collapsing lemma to this in order to get a C.T.M. of the $full$ ZFC?
Also, a professor once told me that Kunen did things this way in order to avoid assuming CON(ZFC), but I didn't understand this explanation either (isn't it pointless avoiding to assume CON(ZFC)... if the negation holds, everything would be provable anyways!!!)
I'm pretty sure there's something about this issue that I'm not taking into account, I would like to know what that is... I'm kindly asking for your help with that!
 A: Here are some examples that might help in understanding.  If ZFC is consistent, then it follows we have a set model $M$ of the theory.  Consider a nonprincipal ultrafilter $U$ on $\omega$ and let $M^{\omega}/U$ be the induced ultrapower.  $M^{\omega}/U$ is a model of ZFC, but it cannot be well-founded because its $\omega$ has nonstandard elements.  Specifically, for any strictly increasing function $g: \mathbb{N} \rightarrow \mathbb{N}$ and $n \in \mathbb{N}$, we have $M^{\omega}/U \models \omega > (g)_{U} > n$ where the $\omega$ here is of course the nonstandard one.  
Also, if you don't want to work with ultrapowers directly, you can simply appeal to the Compactness theorem.  Introduce a set of constants $\{c_n| n \in \mathbb{N}\}$ into your language and for each $n \in \mathbb{N}$, define $\varphi_n := c_0 \ni c_1 \ni \ldots \ni c_n$.  If ZFC is consistent, then every finite fragment of $ZFC + \{\varphi_n| n \in \mathbb{N}\}$ is consistent so the entire theory is by the Compactness theorem.  This then gives us a model $N$ of ZFC that externally can be seen to have an infinite descending chain:
$c_0 \quad \ni_N \quad c_1 \quad \ni_N \quad c_2 \quad \ni_N \quad \ldots \quad \ni_N \quad c_n \ldots$.
Note this is not an actual infinite $\in$-descending chain as Stefan points out, but merely a binary relation on the set $N$.  For example, if $N = M^{\omega}/U$ is the ultrapower induced by a nonprincipal ultrafilter $U$ on $\omega$, then $\in_N$ would be defined by $(g)_U \quad\in_N\quad(h)_U$ exactly when $\{n \in \mathbb{N}| g(n) \in h(n)\} \in U$.
You may also be interested in:
Clearing misconceptions: Defining “is a model of ZFC” in ZFC
A: If there is any ordinal $\alpha$ such that $L_\alpha$ satisfies ZFC, then consider the least one.  This is some countable ordinal $\beta$.  It is easy to show that $L_\beta \vDash$ "There is no transitive model of ZFC."  However, by absoluteness, it will still think that ZFC is syntactically consistent, and therefore has a (non-well-founded) model.  Actually this also shows that any transitive model of ZFC with rank higher than this $\beta$ thinks that there is a transitive model of ZFC, so the existence of transitive models fails only for the very shortest ones.
A: It is true that you can use Löwenheim Skolem to get a countable model $M$ of ZFC assuming $Con(ZFC)$. But to use Mostowski you need additionally the well foundedness of that model, which doesn't have to be true, even though that model satisfies the axiom of regularity. The point here is that $M$ 'thinks' that it is wellfounded but from the 'outside' it is not.
Moreover, remember that $CON(ZFC)$ is merely an artihmetical statement, which doesn't tell you anything about the 'real' consistency of $ZFC$. So assuming $\lnot Con (ZFC)$ will not prove you anything you want, it will just prove you that 'there exists a proof for anything you want' (the statement 'there exists a proof...' is again an arithmetical statement).
