Abstracting the general forcing argument from case-specific arguments

Question

I've found myself wondering whether the literature has an abstraction of what the forcing argument shows in general, in order to separate it from the case-specific arguments that result in specific independence results. What I'm thinking would be something along the lines of:

Suppose $T$ is a theory on the language of ZFC + nullary function symbols $\mathbb{P}, \le$ such that $T \vdash ZFC$ and $T \vdash$ $(\mathbb{P}, {\le})$ is a partial order. Define the corresponding theory $T_f$ on the language of ZFC + nullary function symbols $\mathbb{P}, \le$ + a unary predicate $\cdot \in M$ + a unary function symbol $\cdot^G$ to consist of:

• $T^M$
• $\mathbb{P} \in M$, ${\le} \in M$
• $M$ is transitive
• $G := \{ (p, \check p) \mid p \in \mathbb{P} \}^G$ is an $M$-generic filter of $\mathbb{P}$
• $\forall x, \exists \tau\in M, x = \tau^G$
• $\forall \sigma, \tau \in M, \sigma^G \in \tau^G \leftrightarrow \exists (p, \sigma') \in \tau, p \in G \wedge \sigma^G = (\sigma')^G$.
• $\forall \sigma, \tau \in M, \sigma^G = \tau^G \leftrightarrow [\forall (p, \sigma') \in \sigma, p \in G \rightarrow (\sigma')^G \in \tau^G$ and vice versa$]$.

Then $T_f \vdash ZFC$; and if $T$ is consistent, then so is $T_f$.

---

So, the idea of the proof would be the standards: for the external construction, take an appropriate finite subset of $T$, construct a countable transitive model $M$ of $T$, find a generic filter $G$ of $\mathbb{P}$, and show that $M[G]$ satisfies a finite subset of $T_f$; and given that this works for an arbitrary finite subset of $T_f$, we conclude that $T_f$ is consistent by compactness. For the internal construction, show that $T \vdash (\Vdash \phi)$ for each axiom $\phi$ of $T_f$, and that given a formal proof of $\Gamma \vdash \phi$ in the language of $T_f$ we have $T \vdash (\Gamma \Vdash \phi)$.

And then, we could prove general results which will be useful in the specific cases. So for example, I would hope that $\forall \tau_1, \ldots, \tau_n \in M, \phi(\tau_1^G, \ldots, \tau_n^G) \leftrightarrow \exists p \in G, (p \Vdash \phi(\tau_1, \ldots, \tau_n))^M$ would be a metatheorem of $T_f$. Similarly, we could show $T_f \vdash (ORD^M = ORD)$, and a result that if $T \vdash \mathbb{P}$ has the countable chain condition, then $T_f \vdash (\forall \alpha, \beta \in ORD^M, \alpha = \beta \rightarrow (\alpha = \beta)^M)$.

And finally, for example in the proof that CH is independent, we could set $T$ to be $ZFC + (\mathbb{P}, \le) = \operatorname{Fn}(\aleph_2 \times \aleph_0, 2)$ and show that in this case, $T_f \vdash 2^{\aleph_0} \ge \aleph_2$.

---

I admit that I'm not sure whether my definition of $T_f$ is complete (or even complete enough to show the desired properties), or on the other hand whether $T_f$ might be redundant (in particular, I suspect the condition that $G$ is an $M$-generic filter of $\mathbb{P}$ might be redundant). And there might need to be a variant for ordinal-definable forcing to get various models of $ZF + \lnot AC$. I just wanted to see if something like this has been written up before.

Answer 1

(I'll ignore the issue about finite fragments of the theory - instead, I'll treat the whole $T_f$ at once using a stronger-than-necessary metatheory, and leave it as an exercise to "fragmentize" it. :P)

Forcing can be developed over arbitrary countable models. This means that we can prove that $T_f\models ZFC$ and that $T_f$ is consistent if $T$ is by just copying the usual arguments, via downwards Lowenheim-Skolem:

• To show that $T_f\models ZFC$, suppose WLOG that $T_f$ is consistent (otherwise it's trivial). Let $A$ be a countable model of $T_f$; then $A$ literally is a set forcing extension of its $M$, which is a countable model of ZFC and so we get $A\models ZFC$ as usual.

• Now suppose $T$ is consistent. Let $M$ be a countable model of $T$ and $\mathbb{P}\in M$ a poset. Since $M$ is countable, there really does exist a $G\subseteq\mathbb{P}$ which is $\mathbb{P}$-generic over $M$. Buidling $M[G]$ as usual we get that the obvious expansion of $M[G]$ satisfies $T_f$.

But contra your title, note that the forcing theorems - which we're using here - are not "case-by-case;" I don't see what generality the $T_f$-approach adds to the usual one. In particular, proving the relative consistency of $ZFC+\neg CH$ requires us to write down the appropriate definition of $Fn(\omega,2)$ (or similar) either way, so that in either case specific applications require specific definitions while the method itself and key lemmas are fully general.

Answer 2

The thing is that once you get over the hump of the meta-theoretical issues of forcing, you simply switch to "forcing over the universe", that is just work in $V$, take a partial order, and assume that somehow, you also have a $V$-generic filter for your partial order, even if $V$ was supposed to be the universe of "all" sets.

There is a utilitarian approach to mathematics which says that adding axioms that simplify an argument, even if they are unnecessary, and even if the simplification is "algorithmic", is a good thing. This justifies using set theoretic meta-theory over something as weak as Primitive Recursive Arithmetic, and it is a justification for always assuming we have a countable transitive model of whatever theory we want, if we so desire to do our forcing.

There is no need to go through the Feferman trick of adding a new symbol for a countable elementary submodel of the universe. To that end, this model is not going to be a model of $\sf ZFC$, internally speaking. And that's fine with us, because the argument is meta-theoretic. So why are we bothering so much?

Indeed, looking back at my early days of using forcing arguments the only issue with "just force over the universe" is that it can be confusing to newcomers. Which is why it's important that we have good books that explain forcing, and people answering questions online, etc. But as I said, once you go over that hump, the clearest and most straightforward forcing proofs are just "forcing over the universe".

Answer 3

In my opinion, this or something similar is the "right" way to summarize what forcing accomplishes in general. I assume your $T_f$ includes the recursive definition of evaluation of names $\tau^G$; if it doesn't, then you should probably add it (and it might make some of your axioms redundant). Also, you might want to add that all ordinals are in $M$ (unless your axioms already imply that).

More precisely, I would state the basic general fact about forcing as follows (because I prefer Boolean-valued models for the general theory): Let $B$ be the regular open Boolean algebra of $\mathbb P,\leq$. Then the usual construction of the Boolean-valued universe provides a $B$-valued interpretation of $T_f$ in $T$.

That result can be applied in several ways: (1) As it stands, it covers forcing over the universe. (2) Applied in a $T$-model, it provides the $B$-valued extension of that ground model. You can then divide by an arbitrary ultrafilter in $B$ to get a $2$-valued model. If your ground model is countable, you can divide by a generic ultrafilter and get the usual construction of forcing extensions of a countable model. (3) Since the interpretation is syntactic, you can use it to give a finitary proof that, if $T$ is consistent, then so is $T_f$.

Of course, as others have pointed out and as was already implicit in your question, any particular application of forcing will require inventing a suitable $\mathbb P$ for that particular purpose. The proof that your $T_f$ implies the desired conclusion will then be essentially the same as the traditional proof that the desired conclusion is forced by $\mathbb P$. So this $T_f$ approach doesn't save you any work in particular problems, but (in my opinion) it gives a clearer than usual understanding of what forcing in general is about.