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

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]$.
• This is a nice question, and I would be interested to see a careful, thorough treatment of it. Which very weak meta-theories are sufficient to undertake the various meta-mathematical results in set theory? In addition to all the forcing results, one would want to know about the large cardinal results and so on. For example, what do you need in the meta-theory to prove if ZFC plus a measurable cardinal is consistent, then so is ZFC plus a measurable with exactly one normal measure? And so on... Jun 23 '16 at 13:11
• Do you accept that using inner models to prove consistency of statements can be done finitistically? (For example the construction of $L$ to get the consistency of GCH and AC with ZF.) Jun 23 '16 at 13:23
• Emil Jeřábek provides a substantial answer at the OP's second link, so perhaps what the OP wants is a more developed account of Emil's answer there? mathoverflow.net/a/189032/1946 Jun 23 '16 at 13:24
• Well, then. Given a forcing $P$ we can construct a class which satisfies ZFC and whatever it is that you wanted to be forced. It is not a well-founded relation, so it cannot be collapsed to a transitive class. But you can still run the same argument. Jun 23 '16 at 14:09
• @ganganray: No, you take all the dense open sets of P, this is a filter, so you extend it to an ultrafilter. Now you interpret the names, and you interpret the membership the same you would normally in forcing. This defines a class and a relation on that class. And we can show, essentially the forcing theorem, that the axioms of ZFC continue to hold, and whatever was necessarily forced is also true in that class model. If you are familiar a bit with the Boolean-valued approach to forcing, this is the same idea only without going through the Boolean-valued model first. Jun 23 '16 at 14:24

@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.

• Since comments are very limited in length, posting something like this is reasonable even for "privileged users". Also, welcome to MathOverflow! Jun 23 '16 at 21:21