Why relative consistency results by forcing arguments are provable in finitistic metatheory

Question

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$?

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

Answer 1

@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 〈j_n(κ) | 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[G_p] / U, where G_p is an M-generic filter (not necessarily in V) on P containing p.