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]$.