What does Cohen independence theorem say? In his celebrated paper, the independence of the continuum hypothesis, P. Cohen proved that there is a model of Z-F in which the continuum hypothesis fails. As a corollary, continuum hypothesis is independent to Z-F. This is indeed a famous story in math -- perhaps most graduate students know about it and can roughly recite the heuristic.
However, thinking a little more led me wondering what this statement really means. In particular, I'm not comfortable with the meaning of the term "model". Whatever a model is, suppose there are two models of Z-F, $M_1$ and $M_2$, in which CH holds and fails respectively. Since the $M_i$'s are models of the set theory, what is a set depends on $i$. That is to say, a set in the sense of $M_1$ is not necessarily a set in the sense of $M_2$. However, all definitions I've seen for the term "model" depend on the notion of a set.
Thus my first question: What is a model in this context? If you'd like to use the term "set" in your definition, then in which sense does that mean?
The answer, as I guess, could be that either the term "model" or "set" isn't formally defined here. That's fine, as in the end there must be some undefined terms, and this could be one of them. However, if that's the case, then in what sense can we say that such model exists? That is, we might not know what a model formally is, but at least we should know what qualifies a mathematical work to be a legit construction of a model. This is my second question.

EDIT I was benefited much from the comments, answers, and discussions below, and am grateful for it. What follows is my understanding.
By a "model" we mean a set in ZF theory. By a "set" in ZF theory we mean a class $A$ that exists in the von Neumann universe $V$, or simply denoted by $A \in V$. By "$V$" we mean the syntactic expression $\{x | x = x\}$, and by "exists in $V$" (or $A \in V$) we mean the expression given here.
Therefore, a "model" is really just a syntactic expression derivable from the ZF axioms that satisfy a bunch of syntactic requirements.. but we rather think of it as a real set that we call "set". It is the "set" that we talk about in usual mathematical context (e.g. in a finite group theory course). This answers my first question, and deprecates the second.
 A: Can I try an alternative angle on this that may help. In a theory like ZF, you cannot construct a model of ZF, but you can give a perfectly rigorous definition of what is to be a model of a first-order theory like ZF. To coin a pun, ZF doesn't know much about the art of constructing models, but it knows a good model when it sees one. From this point of view, statements like "if ZF has a model, then it has a countable model" and "if ZF has a countable model, then so so does ZF+$\lnot$CH" are perfectly meaningful statements of ZF (and ZF can prove them). The "ontological" outcome of this is benign and informative. It is benign because the definitions are rigorous and all the ontological assumptions are explicit. It is informative, because if our metalanguage includes ZF and we were to make the ontological assumption that ZF has a model in our metalanguage (e.g., by allowing Grothendieck universes), then we know that our assumptions imply that ZF+$\lnot$CH would have a model too.
A: Cohen showed that if $M$ is a countable transitive model of $V=L$,1 then there is another, larger model, $M[G]$, which is also countable and transitive, has the same ordinals as $M$, and in $M[G]$ the Continuum Hypothesis fails. Indeed, a model is simply a set with a binary relation, and in Cohen's case, it is a [countable] transitive set in some ambient universe of $\sf ZF$, with the relation that is the real $\in$ of that ambient universe (restricted to the model).
By restricting to transitive models, Cohen ensures that the notion of sethood does not change from one model to the next.
Of course, that raises the obvious question: can we do forcing without countable transitive models? Indeed, without any models of $\sf ZF$? The answer is yes, and from a technical standpoint there is little to no difference: start with a countable transitive model, look at the proofs from $\sf ZF$ that the forcing theorem holds for whatever statement we wish to prove, and extract a finite fragment $\sf ZF^*$ which is sufficient for this proof; next given any finite extension of this fragment, we can find a countable transitive model of this fragment and force over that; finally, by a meta-theoretic argument we get that $\sf ZF$ cannot prove $\sf AC$, and $\sf ZFC$ cannot prove $\sf CH$, etc.
But it really is simpler to just take countable transitive models on the chin and move on. Finally the main counterpoint to your issue with "different sethood" is that $M$ is a submodel of $M[G]$, so that $M[G]$ and $M$ agree on the sets of $M$, and their elements, and their elements' elements, and so on.
In fact, in Cohen's case, the forcing does not even change cofinalities of ordinals. So $M$ and $M[G]$ agree on which ordinal is $\omega_1$ and which one is $\omega_2$, etc. The thing they disagree on, for example, is to what extent subsets of $\omega$ are in the model: in $M[G]$ there are more subsets of $\omega$ than in $M$, to the point that there is no longer a way to match them with $\omega_1$ (of $M$ or $M[G]$) inside $M[G]$ itself. And again, because these models are transitive, they also agree with $V$, with the "real universe", as to what are subsets of $\omega$. It's simply that they don't know all the subsets.


*

*Cohen does not assume transitivity, but just that the $\in$ relation is the correct one, but these are all isomorphic to a transitive model, and so he also assumes this.

