Why relative consistency results by forcing arguments are provable in finitistic metatheory It is claimed in many textbooks that relative consistency results, such as $\text{Con}(\text{ZFC})\rightarrow\text{Con}(\text{ZFC}+2^{\aleph_0}\geq\aleph_2)$, are provable in the finitistic metatheory.
It is also claimed by MO users that it is actually provable in PA. 
Formal proof of Con(ZFC) => Con(ZFC + not CH) in ZFC
However, PA may still be too strong for being finitistic. According to Simpson's Subsystems of Second Order Arithmetic, systems like PRA or $I\Sigma_1^0$ may be accepted by some finitists.
Question: are those relative consistency results provable in finitistic systems, such as PRA or $I\Sigma_1^0$? If yes, how to see that? If not, which is the weakest natural system we need to produce the proof?
I have also notice the answer Formal systems needed to formalize relative independence results. But more details are prefered.
====================================
I am trying to do as much as I can. 
Fix a forcing notion, say $\mathbb{P}=\text{Fn}(\aleph_2\times\aleph_0,2)$. I think it can be shown that there is a primitive recursive mapping taking each sentence $\sigma$ in the language of set theory (not the forcing language) to the the set theory statement $1\Vdash\sigma$ (or $\forall p\in\mathbb{P}~ p\Vdash\sigma$).
Fix $\sigma\in(\text{ZFC}+2^{\aleph_0}\geq\aleph_2)$. I think the Robinson arithmetic $Q$ is sufficient to prove: $\text{ZFC}\vdash (1\Vdash\sigma)$.
Now the question is are the following provable in $I\Sigma^0_1$?


*

*$\forall x[x\in(\text{ZFC}+2^{\aleph_0}\geq\aleph_2)\rightarrow\text{ZFC}\vdash(1\Vdash x)]$;

*$\forall x\big[\big((\text{ZFC}+2^{\aleph_0}\geq\aleph_2)\vdash x\big)\rightarrow\text{ZFC}\vdash(1\Vdash x)\big]$.

 A: @AsafKaragila  
This is really a comment, not an answer, but the system wouldn't let me enter it as a comment.  (My apologies if this is inappropriate.)
I did some work on this approach to forcing (the one you heard of from Magidor) many years ago.  I'll describe it, but I'm not sure whether this is all commonly-known folklore; I haven't seen it published.
The motivation was to extend a nice property of Prikry forcing to forcing in general — namely, that one can actually carry out Prikry forcing, in an appropriate sense, without passing to a generic extension.
Let κ be a measurable cardinal with some given normal ultrafilter, and let P be the partial ordering for Prikry forcing (which would make κ cofinal with ω).  Then there is an inner model M and an elementary embedding j: V ⧼ M such that you can carry out (in V) Prikry forcing over M: there exists (in V) an M-generic filter over j(P).
Because of the elementary embedding, having a Prikry sequence through j(κ) for M is more or less as good as having a Prikry sequence through κ for V.  But the nice thing is that we can actually get an M-generic sequence in V.
(The proof proceeds by taking iterated ultrapowers of V by the original normal ultrafilter on κ.  M is the ωth iterate, the elementary embedding j is jω, and the desired Prikry sequence over M is 〈jn(κ) | n < ω〉.)
One can carry out a similar sort of "internal forcing" for any notion of forcing P, by extending the collection of dense open sets of P to an ultrafilter U, and letting j be the elementary embedding mapping V to a submodel M of the ultrapower (one uses a limit ultrapower containing "eventually constant" functions with respect to P).  As I recall, names can be used as usual to construct a generic extension M[G] over j(P).
Note that this is all taking place in V.  The catch, of course, is that M will generally not be well-founded, so it won't be isomorphic to a transitive class with the usual membership relation.
Incidentally, one way to think of M[G] is as a limit ultraproduct, a submodel of an ultraproduct Πp∈P M[Gp] / U, where Gp is an M-generic filter (not necessarily in V) on P containing p.
