As Andreas says, it is in fact provable in PA and even much weaker theories - the difficulty of course being how to remove the "semantic" content. However, it's worth noting that we can show provability in PA without doing any major changes, via conservativity. Here's an outline:
First, consider the theory ACA$_0$. This is a conservative extension of PA - every sentence in the language of arithmetic which is provable in ACA$_0$ is provable already in PA, and PA $\subseteq$ ACA$_0$ - but is able to talk about sets, and hence models. Moreover, the second-order axioms of ACA$_0$ are enough to prove basic facts about logic, especially that $(i)$ every consistent theory is contained in a consistent complete theory, $(ii)$ every consistent theory has a model, and $(iii)$ every theory with a model is consistent (note that in the setting of ACA$_0$, all theories are sets of natural numbers, hence countable, as are all models). (In fact ACA$_0$ is more than enough - I'm not shooting for optimality here.)
Now we just repeat the usual proof inside ACA$_0$. Reasoning inside ACA$_0$, we suppose ZFC is consistent; then it has a model $M$. This model is "explicitly countable" - precisely because of the paucity of ACA$_0$'s framework, $M$ has domain $\subseteq\omega$! This means that we can prove in ACA$_0$ that $M$-generic filters exist, phrased appropriately, for any $M\models$ ZFC.
Letting $G$ be such a generic filter, we want to argue inside ACA$_0$ that $M[G]$ exists since $M$ does. On this face of it this might be worrying because of the amount of transfinite recursion needed to define the forcing extension; however, since all that recursion takes place inside the ground model (here, $M$), it really boils down to "externally" arithmetical facts about $M$, which ACA$_0$ can reason about appropriately. (In fact, per Hamkins/Miller/Williams things are much simpler than one might guess!)
So after following the usual argument with a bit of care, we get that ACA$_0$ proves (for example) that ZFC has a model iff ZFC+CH has a model.
Now ACA$_0$ proves the soundness and completeness theorems as observed above, so ACA$_0$ also proves that ZFC is consistent iff ZFC+CH is consistent. But this is an arithmetical fact; since ACA$_0$ is conservative over PA, this means PA proves that ZFC is consistent iff ZFC+CH is consistent, and we're done!
This suggests a neat approach to "finitizing" forcing arguments: if you have a semantic proof that Con(T) implies Con(S), and you want to prove Con(T)$\implies$Con(S) in some weak theory of arithmetic $A$, you look for a conservative extension $\hat{A}$ of $A$ which can run the appropriate semantic arguments directly. However, this seems fundamentally limited; in particular, the bigger system $\hat{A}$ really needs to be able to prove the completeness theorem, which forces us to include weak Konig's lemma, and this limits the theories which have such a conservative extension. (E.g. replace PA with PRA above and I'm not sure what to do.) So that seems like it won't work to get these relative consistency results proved in truly weak arithmetics. Instead, I think work needs to be done to really excise the semantic content from the usual arguments and as Andreas says turn them into arguments about proof manipulation.
It's possible I'm wrong, and there are ways we can get around the "completeness barrier," but my understanding is that to go significantly below PA we really do want to give up semantics, at least to a large extent, rather than trying to shoehorn it in by finding serendipitous conservative extensions.
And when we go far enough down, things can indeed get truly weird. There are extremely weak systems of arithmetic which are just barely strong enough for it to be meaningful to ask what they think about logic, but which allow for totally ridiculous possibilities. For example, in the paper Oracle bites theory, Visser looks at the possibility of a consistent theory having inconsistent deductive closure. So at that level, anything's possible.
