Recently I read throught Jech's proof of the independence of the continuum hypothesis.
However there was something that bothered me a lot, the whole idea of the generic filter. Beginning the section of forcing in Jech's set theory the author stated that Cohen's original approach was to assume the existence of a countable transitive model of $\mathsf{ZFC}$, and then get a generic filter with respect to the required forcing conditions, then the author states that this cannot be done since such model canoot be proved to exists in $\mathsf{ZFC}$ unless $\mathsf{ZFC}$ is inconsistent, later stating that the usual way of working with forcing was postulating the existence of the generic filter for the required forcing notion.
I found Jech's approach really incomplete, so I searched on the internet and saw the following theorem:
If $\Lambda\subseteq ZFC$ is finite, then $\mathsf{ZFC}\vdash\exists M[M \text{ is transitive}\wedge|M|=\aleph_0\wedge M\models ZC\cup \Lambda].$
Then I argued as follows:
Suppose $\mathsf{ZFC}\vdash\mathsf{CH}$, then there exists some finite $\Lambda\subseteq\mathsf{ZFC}$ such that $\Lambda\vdash\mathsf{CH}$.Let $P$ be the notion of forcing such that for any generic $G$ of $P$ we have $M[G]\models2^{\aleph_0}\geq\aleph_2$. Let $G$ be generic over $M$; such $G$ exists as $M$ is countable.
Reading Jech's proof of the generic model theorem we can get a finite $\Omega\subseteq\mathsf{ZFC}$ such that $\Omega\supseteq\Lambda$ and if $M\models\Omega\cup\mathsf{ZC}$, then $M[G]\models\Lambda\cup\mathsf{ZC}$; the extension is required only for the different instances of the replacement axiom in $\Lambda$. Then clearly this is a contradiction as there exists such a countable $M$. Therefore $\mathsf{ZFC}\nvdash\mathsf{CH}$.
Is my approach correct?
Yes. This approach works out just fine. In reality (i.e. research papers) people often just assume there are transitive models of set theory, if only for convenience. It's easier this way.
Another approach, which is actually what Jech does in every book of him that I read so far (counting three by now), is using Boolean valued models of set theory. This is a definable class which is a model of set theory where truth values are not $0-1$, but rather taken from a complete Boolean algebra. Then one can show that if $\varphi$ is a statement whose truth value in some Boolean valued model is neither $0$ nor $1$, then we cannot prove it from $\sf ZFC$.
This method was used originally by Scott and Solovay to prove the independence of the continuum hypothesis using random variables (taking the Boolean algebra to be very large).