Is it possible to prove $Con(ZFC) \rightarrow Con(ZFC + \neg CH)$ purely within ZFC? To prove this (using forcing) one seems to need a countable transitive model of ZFC. The texts I am reading avoid this by proving Con(T + CH) for all (suitable) finite fragments T of ZFC using the Reflection principle to prove the existence of a countable transitive model of T. But doesn't the Reflection principle operate outside of ZFC? From what I understand it just shows how, given a list of axioms of ZFC, one can write down a proof that constructs a model of these axioms.
Am I confused here or is there an other way to achieve this?



Formal proof of Con(ZFC) => Con(ZFC + not CH) in ZFC
The reflection principle is a theorem scheme; each of its instances is provable in ZFC. 


The following proof works entirely in ZFC:


1. Assume Con(ZFC) together with not-Con(ZFC+non-CH) and aim for a contradiction.
2. By assumption plus completeness theorem, there is a model (M,E) of ZFC. M may be nonstandard in the sense that its ordinals (even its natural numbers) are not well-founded.
3. By compactness, there is some finite sub theory ZFC\* of ZFC such that ZFC\*+non-CH is inconsistent.
4. Find a (slightly larger) finite sub theory ZFC\*\* of ZFC such that ZFC\*\* proves all theorems you need about forcing, including that ZFC\* plus non-CH holds in the extension.
5. (M,E) satisfies reflection for ZFC\*\* , so there is some x in M which M thinks is a ctm (countable transitive model) of ZFC\*\* . So M can find a Cohen extension y of x which satisfies ZFC\* plus non-CH.
6. By the easy direction of the completeness theorem, M therefore thinks that ZFC\*+non-CH is consistent.
7. But then this theory is really consistent. (Because any proof of an inconsistency would be coded by a natural number, which is represented in M.)


Btw, I think the sketch I just gave is not ideal since it seems to rely on the existence of infinite sets. The implication from Con(ZFC) to Con(ZFC+non-CH) can really be shown in ZF minus infinity, or even in a weak version of Peano arithmetic. 


