Proving Unprovability: Is Compactness Used in the Metathory? I am reading Halbeisen's "Combinatorial Set Theory", and it certainly provides a great exposition of forcing (bar its notation conventions for forcing...). The very short chapter 16 is dedicated to formalising the idea of proving independence.
(1) In essence, he proposes the following: let $\Phi$ be a finite fragment of ZFC. Then, by the reflection principle (which is a theorem schema in ZFC), there is a set $M$ that models $\Phi$. In particular, there is a $V_{\lambda}$ for some limit ordinal $\lambda$ that satisfies this, and hence is even transitive.
(2) Now that we have a transitive model of $\Phi$, we can apply the Mostowski collapse (provided $\Phi$ contains the axiom of Extensionality, since then $M$ itself is extensional) to obtain a countable transitive model $M'$ of $\Phi$. This is also a theorem of ZFC since $M$ and its transitive collapse $N$ are necessarily both sets, and so is the unique isomorphism $\pi$.
(3) Finally, if we are now able to extend $M'$ to some $M'[G]$, using forcing for example, so that $M'$ satisfies some additional sentence $\varphi$, then we may deduce by compactness that $\text{ZFC} + \varphi$ has a model, and is hence consistent.
Just to clarify: This application of compactness must happen in the meta theory, since otherwise ZFC would prove that it had a model. (This contradiction would, if I understand correctly, already appear just after step (2), as the reflection principle implied that any finite fragment of ZFC has a model.
Is this reasoning valid?
 A: You seem to be correct that the argument is framed as an application of compactness in the metatheory. The issue is not that compactness can only be applied in the metatheory in general: it's a theorem of ZFC. Rather, the issue is that the reflection theorem is not a theorem of ZFC but rather a theorem scheme. It gives us "for each finite subtheory T of ZFC, ZFC proves Con(T)", not "ZFC proves 'for each finite subtheory T of ZFC, Con(T)'." You are correct that if the latter were the case instead, compactness (in ZFC) would yield a contradiction with incompleteness.
(HT to Noah Schweber, who wrote something like what I just wrote about the reflection theorem in an answer but deleted it, presumably to let me have all the glory. I figured I should include it cause it seems like it could potentially be a point of confusion.)
However, you don't really need to use the compactness theorem in the metatheory here. All you really need is its much simpler syntactic analogue that says any proof of inconsistency would come from a finite number of axioms. 
If there were a proof of inconsistency from ZFC + $\varphi,$ let it use the axioms $A_1,\ldots, A_n$ of ZFC. Then you just need to confirm that the proof that the forcing extension satisfies $A_1,\ldots, A_n, \varphi$ only depends on the ground model satisfying some finite number of ZFC axioms $A_1',\ldots, A_m'.$
So then, we could produce a contradiction in ZFC by using the reflection theorem to show there is a countable transitive model of $A_1',\ldots, A_m',$ then prove that a forcing extension exists that satisfies $A_1,\ldots A_n,\varphi,$ and then relativize the proof of contradiction to the forcing extension, which amounts to a proof of contradiction. 
(You can view this last part as using the soundness theorem in the metatheory, which is a much weaker and finitary theorem than compactness theorem.)
