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!