First of all, I'm only starting to study independence results in set theory. And there is one obstacle that confuses me a lot. Probably such questions have already been asked, but I haven't found anything that clarifies it for me. I'm new to that subject, so please feel free to correct me if I'm using wrong terminology or reasoning.
Here is how I understand the reasoning behind proving that a statement $\varphi$ is not a theorem of a theory $T$. From mathematical logic we know that $T \not\vdash \varphi$ if and only if $\mbox{Con}(T + \neg \varphi)$. From Gödel's Completeness theorem it follows that $\mbox{Con}(T)$ if and only if $T$ has a model (that is a set with a collection of operations, relations and constants). So in order to prove something like $\mathsf{ZFC} \not\vdash \mathsf{CH}$ we should produce a model of $\mathsf{ZFC} + \neg\mathsf{CH}$. On the other hand, by Gödel's Incompleteness theorem this can't be done inside $\mathsf{ZFC}$. So all consistency results should be relative and be of the form $$\mbox{Con}(\mathsf{ZFC}) \rightarrow \mbox{Con}(\mathsf{ZFC} + \varphi).$$
As I've understood, when the method of forcing is used, we start with the assumption like $\mbox{Con}(\mathsf{ZFC})$ that gives us a (set) model $(M, \in)$ of $\mathsf{ZFC}$ from which (using Löwenheim–Skolem theorem) we can get a countable model of $\mathsf{ZFC}$. After that we extend this model to another model $(N, \in)$ that satisfies some desired statement $\varphi$ obtaining a model of $\mathsf{ZFC} + \varphi$. Such reasoning looks perfectly fine to me, since we are working with set models of $\mathsf{ZFC}$ whose existence is based on the assumption $\mbox{Con}(\mathsf{ZFC})$.
The question is about class models of $\mathsf{ZFC}$. For example, there is the Gödel's constructible universe $L$ that is a model for $\mathsf{ZFC} + V = L$ (and also for $\mathsf{AC}$ and $\mathsf{CH}$). My main question is
How can we formally deduce from the existence of such a (class) model that $$\mbox{Con}(\mathsf{ZFC} + V = L)?$$ In other words, how the existence of a class model for $T$ implies $\mbox{Con}(T)$?
Is there some kind of Gödel's completeness theorem for class models? Or again we are starting with some set model of $\mathsf{ZFC}$ and constructing $L$ inside it? If so, how this changes the proof of that $L$ is a model of $\mathsf{ZFC}$? It seems like I'm missing some basic fact (and commonly used technique) that allows to go from class models to set models. I would be very grateful if someone could explain me in details how this issue is resolved. Thanks in advance!
The theorem that $\operatorname{Con}\sf (ZF)$ implies $\operatorname{Con}\sf (ZF+\mathit{V=L})$ is a meta-theorem.
It is formulated in the meta-theory, and not internally. You are absolutely right that we can't quite formulate this internally without violating Godel's incompleteness theorem. But the nice thing is that what we can prove is that for every axiom $\varphi$ of $\sf ZFC$, $\sf ZF\vdash\varphi^L$, where $L$ is the class defined via the axiom of constructibility.
So while $\sf ZF$ does not prove that $L\models\sf ZFC$, it does prove that every axiom of $\sf ZF$ is relatively true. This tells us even a bit more than just the meta-theorem, which is great.