Henkin's theorem asserts that if a theory is consistent, then it has a countable model, say $M$. Does it mean the existance of $M$ can be deduced in ZFC?
Am I right that Gödel's 2-nd theorem implies that if ZFC is consistent, and hence have a model $M$, then the existance of $M$ can not be deduced in ZFC?
Something of this must be wrong since otherwise we get a contradiction.
The theorem that if a theory is consistent, then it has a countable model is a theorem of ZFC. So if we can prove a theory is consistent in ZFC, then we can prove it has a countable model in ZFC.
The converse is also a (easier) theorem of ZFC. So if we can prove there is a model of a theory in ZFC, then we can prove it is consistent in ZFC.
Godel’s theorem implies ZFC cannot prove ZFC is consistent. By the above considerations, this means ZFC cannot prove there is a (countable) model of ZFC. This doesn’t mean that a model doesn’t exist, just that ZFC can’t prove it.