In ZFC+Con(ZFC), one can prove ZFC is consistent, so has a model. But how can I construct a model of ZFC in ZFC+Con(ZFC) formally?
I think the Con(ZFC) only says "the ZFC is consistent", not a technical statement, so if we formally construct a model of ZFC in ZFC+Con(ZFC), then there might be only axioms of ZFC in the way of constructing the model, so it can be also constructed in ZFC. It contradicts the Goedel's second incompleteness theorem. Therefore, we cannot formally construct a model of ZFC even in ZFC+Con(ZFC). Is this argument right?
Thank you.
No, that argument isn't right. $\mathsf{ZFC}$ proves the completeness theorem, and so in particular does indeed prove "$Con(\mathsf{ZFC})$ implies $\mathsf{ZFC}$ has a model."
Looking at the proof of the completeness theorem will demystify this: the proof actually constructs a model of the consistent theory in question, and the point is that that construction can be performed in $\mathsf{ZFC}$.
What this won't do is construct a transitive model of $\mathsf{ZFC}$. Indeed, the theory $$\mathsf{ZFC}+Con(\mathsf{ZFC})+\mbox{ "$\mathsf{ZFC}$ has no transitive model"}$$ is consistent (as long as $\mathsf{ZFC}+Con(\mathsf{ZFC})$ is). To see this, let $M\models\mathsf{ZFC}+Con(\mathsf{ZFC})$ and suppose $M\models$ "$\mathsf{ZFC}$ has a transitive model" (otherwise we're done). Let $\alpha$ be the least $M$-ordinal such that $M\models$ "$(L_\alpha)^M\models\mathsf{ZFC}$." Then $L_\alpha^M\models$ "$\mathsf{ZFC}$ has no transitive model" since otherwise (the $L$ of) that model would give us a level of $M$'s $L$-hierarchy below $\alpha$ which ($M$ thinks) is a transitive model of $\mathsf{ZFC}$.
So the models that the completeness theorem lets us construct from mere consistency are not particularly nice. But, they are models!