I´m a bit puzzled by the non-ctm (countable transitive model) approach to forcing as described in Kunen (see here). Kunen calls this "forcing over the universe". I can see how the proofs of (a), (b) and (c) wold go (although I haven't yet sat down to work through them), and how, once we have them, we can get relative consistency results. However, I'm lost as to how one actually gets $\mathbb{1}\Vdash^* \neg $CH.

When looking at the proof involving ctms, we start with a ctm $M$, consider the poset (inside $M$) Add$(\aleph_2,\omega)$, and see that in the generic extension we have $\aleph_2$-many new reals, using the fact that this poset preserves cardinals since its ccc. This uses the definition of $\Vdash$ at several points, i.e. $p\Vdash \phi$ iff for every $M$-generic $G$ with $p\in G$, $M[G]\models\phi$ (with the required interpretations).

Now, if we never define $\Vdash$ nor talk about models, how can we get $\mathbb{1}\Vdash^* \neg $CH? The definition of $p\Vdash^*\phi$ is by recursion on the length of $\phi$, and unwinding something like $\neg$CH is not doable. Moreover, results like

Forcing with such or such poset preserves cardinals.

wouldn´t make sense if I don't have the models $M$ and $M[G]$ to talk about.

Plus, Kunen states it without further comment, so I assume there's something elementary which I' overlooking.

I know that the forcing over the universe approach is doable through Boolean valued models, but can we still make sense of the above without introducing them?

  • $\begingroup$ I don't see why writing down $\lnot\mathrm{CH}$ is not doable. And saying that a forcing preserves cardinals just in terms of the forcing relation should also be fine: you just have to say that if there wasn't a small ordinal bijective with $\check{\kappa}$ in the ground model (you can do this by quantifying over the ground model's powerset of $\kappa$, i.e. its check name) then $\check{\kappa}$ is a cardinal. $\endgroup$ Feb 27, 2019 at 7:41
  • $\begingroup$ @MihaHabič What I meant by "writing down ¬CH is not doable" is that turning ¬CH into a statement in the language of set theory, just using $\in$, would be incredibly complicated. Now, the definition of $\Vdash^*$ is by recursion on complexity, so if we were to work only with $\Vdash^*$ and had no models to speak of, I saw no way of actually proving $\Vdash^*\neg$CH. $\endgroup$
    – Reveillark
    Feb 27, 2019 at 14:30
  • $\begingroup$ "how can we get 1⊩∗¬CH? The definition of p⊩∗ϕ is by recursion on the length of ϕ"; the idea is actually to exploit the combinatorial properties of $\mathbb{P}$-names and the partial order $\mathbb{P}$ to establish the non-existent of objects which could (when appropriately interpreted) witness $CH$ in some hypothetical extension. In this scenario, the forcing relation creeps in, when we reduce the existence of certain $\mathbb{P}$-names (with hypothetical bad properties) to the existence of ones with a specific (and exhaustible) form. $\endgroup$
    – Not Mike
    Mar 2, 2019 at 1:09
  • $\begingroup$ ... And when establishing that certain extremely low complexity statements can always be forced densely often. $\endgroup$
    – Not Mike
    Mar 2, 2019 at 1:19

3 Answers 3


Here it something, very close to Boolean-valued models, that I learned from my advisor.

Let $\Bbb P$ be a forcing notion, and let $V^\Bbb P$ be the class of names. Note that the collection of dense open sets is a filter base, since intersection of finitely many dense open sets is dense open. So use choice to extend it to an ultrafilter on $\Bbb P$, say $U$. (Here we mean ultrafilter in the sense of a maximal filter on the partial order.)

Now use your filter to interpret the names. This defines a class $(M,E)$ where the objects in $M$ are the equivalence classes of $V^\Bbb P/U$ (using Scott's trick as necessary to turn those proper classes into sets again), with $\dot x =_U\dot y$ if and only if there is some $p\in U$ such that $p\Vdash\dot x=\dot y$. And Similarly $\dot x E\dot y$ if there is a condition forcing that.

We can now prove the usual truth lemma for the forcing relation. Finally, let's go back to your question.

We know that the forcing relation can be defined internally, so $1\Vdash\lnot\sf CH$ is something that you can define and prove internally to $V$ about $\Bbb P$. So now take $\Bbb P$ to be $\operatorname{Add}(\omega,\omega_2)$, and you're done.

Oh. Yeah. You want to ask now, if you have a filter that meets all the dense open sets, how is it not a generic filter? Well. Extending it to an ultrafilter makes it a bit more icky. And since $(M,E)$ is not well-founded, there's no reason for $U$ to be truly generic.

  • $\begingroup$ Thank you for your answer. To clarify, when you say $p\Vdash \dot{x}=\dot{y}$, you mean the usual $\in$-recursive definition of $\Vdash$? And the statement of the Truth Lemma would be $(M,E)\models \phi\iff \exists p\in U (p\Vdash \phi)$? I'm also a bit confused by your last comment relating genericity and well-foundedness. Thank you so much for your help! $\endgroup$
    – Reveillark
    Feb 27, 2019 at 15:29
  • $\begingroup$ There is a nice theorem about Boolean-valued models, that given the Boolean-valued model $V^B$ and an ultrafilter $U$ over $B$, then $V^B/U$ is well-founded (externally!) if and only if $U$ is generic. The approach I outline here is the same as Boolean-valued models, so it suffers from the same problems. $\endgroup$
    – Asaf Karagila
    Feb 28, 2019 at 0:02

One point is: because the internal forcing relation $\Vdash^*$ respects all the rules of first-order logic, you don't necessarily have to work directly with evaluating $p \Vdash^* \lnot CH$; instead, you can apply any valid proof methods using axioms of ZFC. Namely, the relevant result would be:

Suppose $\Gamma \vdash \phi$ in ZFC, and for some $p \in \mathbb{P}$, $p \Vdash^* \psi$ for each $\psi \in \Gamma$. Then $p \Vdash^* \phi$. (And as a corollary, if $\Vdash^* \psi$ for each $\psi \in \Gamma$, then $\Vdash^* \phi$.)

So, suppose you have proved that $\Vdash^* \check \aleph_0 = \aleph_0$, $\Vdash^* 2^{|\check\aleph_0|} \ge |\check\aleph_2|$ and also that $\Vdash^* |\check \aleph_0| < |\check \aleph_1| < |\check \aleph_2|$ (as cardinals); then if you imagine constructing a formal proof within ZFC that $\check \aleph_0 = \aleph_0, 2^{|\check \aleph_0|} \ge |\check\aleph_2|, |\check \aleph_0| < |\check \aleph_1| < |\check \aleph_2| \vdash \lnot CH$, then applying the above result will give that $\Vdash^* \lnot CH$.

The proof of the above result proceeds by structural induction on the formal proof of $\Gamma \vdash \phi$. As a sample part of the proof, let's suppose that our formal proof system is some variant of natural deduction, and we will show the inductive step for a proof by $\vee$-elimination. Thus, suppose that $\Gamma \vdash \alpha \vee \beta$; $\Gamma, \alpha \vdash \gamma$; and $\Gamma, \beta \vdash \gamma$; and we also assume the inductive hypothesis for these subproofs. Now, the conclusion of this step of the formal proof will be $\Gamma \vdash \gamma$. So, suppose that $p \Vdash^* \psi$ for each $\psi \in \Gamma$, and we will want to show that $p \Vdash^* \gamma$. Then by the inductive hypothesis for $\Gamma \vdash \alpha \vee \beta$, $p \Vdash^* \alpha \vee \beta$. By definition, this means that the set of $q$ such that $q \Vdash^* \alpha$ or $q \Vdash^* \beta$ is dense below $p$. For $q$ such that $q \Vdash^* \alpha$, then by the inductive hypothesis for $\Gamma, \alpha \vdash \gamma$, we will get that $q \Vdash^* \gamma$; and similarly, for $q$ such that $q \Vdash^* \beta$, the other inductive hypothesis will give that $q \Vdash^* \gamma$. Therefore, the set of $q$ such that $q \Vdash^* \gamma$ is also dense below $p$, implying that $p \Vdash^* \gamma$.

(One additional detail is that for a proof constructed using equality elimination, a.k.a. the substitution rule, you will need to proceed by structural induction on the formula involved in the substitution.)

Now as for the arguments that go back and forth between forcing relations and properties of $M[G]$ in order to relate properties of $\mathbb{P}$ and $M$ with properties of $M[G]$: it should usually be straightforward to recast these as pure forcing proofs. For this, it will often be useful to extend the language of ZFC for forcing statements to include a unary predicate $\dot V$ (with syntactic sugar $\cdot \in \dot V$) and define $p \Vdash \dot V(\tau)$ if and only if the set of $q$ such that there exists $x$ such that $q \Vdash^* \tau = \check x$ is dense below $p$. Then it is straightforward to show that $\Vdash^* \dot G$ is a $\dot V$-generic filter of $\check{\mathbb{P}}$ (where $\dot G = \{ (p, \check p) \mid p \in \mathbb{P} \}$ is the usual name for the generic filter).

Outline for the genericity part: suppose for some name $D$, $p \Vdash^* D \in \dot V$ and $p \Vdash^* D$ a dense subset of $\check{\mathbb{P}}$. Then for any $q$ in the dense set below $p$, choose some corresponding $D_0$ such that $q \Vdash^* D = \check D_0$. The fact that $q \Vdash^* D$ a dense subset of $\check{\mathbb{P}}$ implies that $D_0$ is a dense subset of $\mathbb{P}$. Therefore, there exists $r \le q$ with $r \in D_0$. Now, $r \Vdash^* \check r \in \dot G \cap \check D_0$, so $r \Vdash^* \dot G \cap D \ne \emptyset$. This shows that the set of $r$ such that $r \Vdash^* \dot G \cap D \ne \emptyset$ is dense below $p$, so $p \Vdash^* \dot G \cap D \ne \emptyset$.

I will now proceed to give some more details on how you would prove that $1 \Vdash^* |\check \aleph_2| \le 2^{|\check \aleph_0|}$. To begin with, if you trace through the definitions a bit, you can eventually see that for $\alpha \in \aleph_2$, a name for the $\alpha$th subset of $\check \aleph_0$ is:

$$\dot S_\alpha := \{ (p, \check n) \mid p \in \mathbb{P}, n \in \aleph_0, (\alpha, n) \in \operatorname{dom}(p), p(\alpha, n) = 1 \}.$$

We now prove some results regarding $\dot S_\alpha$:

Lemma: Suppose $p \in \mathbb{P}$ satisfies $p(\alpha, n) = 1$. Then $p \Vdash^* \check n \in \dot S_\alpha$.

Proof: This is a straightforward application of the definition of $p \Vdash^* \cdot \in \cdot$ (and in particular the special case that if $(q, \sigma) \in \tau$ then $q \Vdash^* \sigma \in \tau$).

Lemma: Suppose $p \in \mathbb{P}$ satisfies $p(\alpha, n) = 0$. Then $p \Vdash^* \check n \notin \dot S_\alpha$.

Proof: We need to show that for each $q \le p$, $q \not\Vdash^* \check n \in \dot S_\alpha$. So, suppose to the contrary that for some $q \le p$, we had $q \Vdash \check n \in \dot S_\alpha$. Then there exists $r \le q$ and $(s, \tau) \in \dot S_\alpha$ such that $r \le s$ and $s \Vdash^* \tau = \check n$. However, since $(s, \tau) \in \dot S_\alpha$, then $\tau$ is of the form $\check m$, and $s \Vdash^* \check m = \check n$ implies $m = n$. Furthermore, $s(\alpha, m) = 1$, so $s(\alpha, n) = 1$. But then, $s \le p$ and $p(\alpha, n) = 0$ gives a contradiction. $\square$

Lemma: Suppose $\alpha, \beta \in \aleph_2$ with $\alpha \ne \beta$. Then $1 \Vdash^* \dot S_\alpha \ne \dot S_\beta$.

Proof: It suffices to show that for any $p \in \mathbb{P}$, there exists $q \le p$ such that $q \Vdash^* \dot S_\alpha \ne \dot S_\beta$. But every $p \in \mathbb{P}$ has finite domain; therefore, there exists some $n \in \aleph_0$ such that neither $(\alpha, n)$ nor $(\beta, n)$ is in $\operatorname{dom}(p)$. Now define $q := p \cup \{ ((\alpha, n), 0), ((\beta, n), 1) \}$. Then by the above lemmas $q \Vdash^* \check n \notin \dot S_\alpha$ and $q \Vdash^* \check n \in \dot S_\beta$. But ZFC (and in fact pure first-order logic) proves that $\check n \notin \dot S_\alpha, \check n \in \dot S_\beta \vdash \dot S_\alpha \ne \dot S_\beta$. Therefore, applying the main result above, we get that $q \Vdash^* \dot S_\alpha \ne \dot S_\beta$. $\square$

Now, based on these facts, we will collect the $\dot S_\alpha$ into a name for an injective function $\check \aleph_2 \to P(\check \aleph_0)$. Namely, define $$\dot S := \{ \dot{\operatorname{ordpair}} (\check\alpha, \dot S_\alpha) \mid \alpha \in \aleph_2 \}$$ where $\dot{\operatorname{ordpair}}(\sigma, \tau) = \{ (1, \{ (1, \sigma) \}), (1, \{ (1, \sigma), (1, \tau) \} ) \}$ is a name for the notional ordered pair $(\sigma^G, \tau^G) = \{ \{\sigma^G\}, \{\sigma^G,\tau^G\} \}$. (It should be straightforward to show $1 \Vdash^* \dot{\operatorname{ordpair}}(\sigma, \tau) = (\sigma, \tau)$ where the right hand side is the ZFC statement that the object on the left satisfies the property defining the ordered pair of $\sigma$ and $\tau$. In particular, a corollary of this, using the main result, will be that $1 \Vdash^* \dot{\operatorname{ordpair}}(\sigma, \tau) = \dot{\operatorname{ordpair}}(\sigma', \tau') \leftrightarrow \sigma=\sigma' \wedge \tau=\tau'$.)

Lemma: $1 \Vdash^* \dot S$ is a function $\check \aleph_2 \to P(\check \aleph_0)$.

Proof: From the definition of $\dot S$, it should be straightforward to check that $1 \Vdash^* \dot S \subseteq \check \aleph_2 \times P(\check \aleph_0)$. (For this, it will be handy to use the lemma that $p \Vdash^* \sigma \subseteq \tau$ if and only if for each $(q, \alpha) \in \sigma$ and each $r \le p, q$, we have $r \Vdash^* \alpha \in \tau$.)

Now, suppose we have some $p \in \mathbb{P}$ and some name $\tau$ such that $p \Vdash^* \tau \in \check \aleph_2$. Then for each $q \le p$, there exists $r \le p$ and $(1, \check \alpha) \in \check \aleph_2$ for $\alpha \in \aleph_2$ such that $r \Vdash^* \tau = \check \alpha$. Now, $1 \Vdash^* \dot{\operatorname{ordpair}}(\check \alpha, \dot S_\alpha) \in \dot S$, so $r \Vdash^*$ the same thing. But in ZFC, $\tau = \check \alpha, \dot{\operatorname{ordpair}}(\check \alpha, \dot S_\alpha) \in \dot S \vdash \exists x, \dot{\operatorname{ordpair}}(\tau, x) \in \dot S$; so $r \Vdash^* \exists x, \dot{\operatorname{ordpair}}(\tau, x) \in \dot S$. This shows that $1 \Vdash^* \forall \tau \in \check \aleph_2, \exists x, \dot{\operatorname{ordpair}}(\tau, x) \in \dot S$.

(For brevity, I'll drop the $\dot{\operatorname{ordpair}}$ notation from now on.)

Similarly, suppose we have $p \in \mathbb{P}$ and names $\tau, \sigma, \sigma'$ such that $p \Vdash^* (\tau, \sigma) \in \dot S \wedge (\tau, \sigma') \in \dot S$. Then for every $q \le p$, there exists $r \le q$ and $(1, (\check \alpha, \dot S_\alpha)) \in \dot S$ such that $r \Vdash^* (\tau, \sigma) = (\check \alpha, \dot S_\alpha)$. Similarly, there exists $s \le r$ and $(1, (\check \beta, \dot S_\beta)) \in \dot S$ such that $s \Vdash^* (\tau, \sigma') = (\check \beta, \dot S_\beta)$. But then, $s \Vdash^* \tau = \check \alpha$ and $s \Vdash^* \tau = \check \beta$, so $s \Vdash^* \check \alpha = \check \beta$, implying that $\alpha = \beta$. Also, $s \Vdash^* \sigma = \dot S_\alpha$ and $s \Vdash^* \sigma' = \dot S_\beta$; and in our base universe, $\dot S_\beta = \dot S_\alpha$. So, applying the main result above, we get that $s \Vdash^* \sigma = \sigma'$. We have now shown that the set of $s$ with $s \Vdash^* \sigma = \sigma'$ is dense below $p$, so $p \Vdash^* \sigma = \sigma'$.

This was what we needed to show to get $1 \Vdash^* \forall \tau, \sigma, \sigma', (\tau, \sigma) \in \dot S \wedge (\tau, \sigma') \in \dot S \rightarrow \sigma = \sigma'$. $\square$

Lemma: $1 \Vdash^* \dot S : \check \aleph_2 \to P(\check \aleph_0)$ is injective.

Proof: Similarly to the above, suppose we have some $p \in \mathbb{P}$ and names $\tau, \tau', \sigma$ such that $p \Vdash^* (\tau, \sigma) \in \dot S \wedge (\tau', \sigma) \in \dot S$. We then claim that $p \Vdash^* \tau = \tau'$. Suppose not; then there is some $q \le p$ such that $q \Vdash^* \tau \ne \tau'$. Now, since $q \Vdash^* (\tau, \sigma) \in \dot S$, there exists some $r \le q$ and $(1, (\check\alpha, \dot S_\alpha)) \in \dot S$ such that $r \Vdash^* (\tau, \sigma) = (\check\alpha, \dot S_\alpha)$. Similarly, since $r \Vdash^* (\tau', \sigma) \in \dot S$, there exists some $s \le r$ and $(1, (\check\beta, \dot S_\beta)) \in \dot S$ such that $s \Vdash^* (\tau', \sigma) = (\check\beta, \dot S_\beta)$. Now, using some applications of the main result, we conclude that $s \Vdash^* \check \alpha \ne \check \beta$, so $\alpha \ne \beta$. But then by an above lemma, $s \Vdash^* \dot S_\alpha \ne \dot S_\beta$. We can now use the main result to derive a contradiction $s \Vdash^* \bot$.

The previous paragraph then proves $1 \Vdash^* \forall \sigma, \tau, \tau', (\tau, \sigma) \in \dot S \wedge (\tau', \sigma) \in \dot S \rightarrow \tau = \tau'$. Since in ZFC, this statement is sufficient to show that $\dot S$ is injective, by the main result we get that $1 \Vdash^* \dot S$ is injective. $\square$

Corollary: $1 \Vdash^* |\check\aleph_2| \le 2^{|\check\aleph_0|}$.

Proof: In ZFC, $\dot S$ is an injective function $\check\aleph_2 \to P(\check\aleph_0)$ implies that $|\check\aleph_2| \le 2^{|\check\aleph_0|}$. Therefore, applying the main result on this proof in ZFC and the previous lemma gives the result. $\square$

  • $\begingroup$ Thank you for your answer. I see what you mean regarding the proof theoretic properties of $\Vdash^*$, but when you say "suppose you have proved $\Vdash^* 2^{|\check\aleph_0|} \ge |\check\aleph_2|$", it seems that the problem has shifted from seeing $\Vdash^*\neg CH$ to $\Vdash^* 2^{|\check\aleph_0|} \ge |\check\aleph_2|$, which still seems non-trivial to me, seeing as how we don't have any models and are just doing syntactical trickery. $\endgroup$
    – Reveillark
    Mar 14, 2019 at 0:00
  • $\begingroup$ By $2^{|\check \aleph_0|} \ge |\check \aleph_2|$ I meant that as syntactic sugar for the formalization of "there exists an injective function $\check \aleph_2 \to P(\check \aleph_0)$". And there, what you actually prove is forced is the formalization of: $\bigcup \dot G$ is a function $\check \aleph_2 \times \check \aleph_0 \to \{ 0, 1 \} \check{}$ which induces an injective function $\check \aleph_2 \to P(\check \aleph_0)$. $\endgroup$ Mar 14, 2019 at 0:03
  • $\begingroup$ I think I'll go ahead and expand the argument that $\Vdash^* |\check \aleph_2| \le 2^{|\check \aleph_0|}$ a bit and hopefully that will make it a bit clearer how you use the quoted result in practice. $\endgroup$ Mar 14, 2019 at 19:14
  • $\begingroup$ That would be very helpful, thank you :) $\endgroup$
    – Reveillark
    Mar 14, 2019 at 19:23
  • $\begingroup$ OK, the revision is done now. $\endgroup$ Mar 14, 2019 at 21:53

There is another way to see that generally what is provable about $\Vdash$ relativised to a ctm is provable about $\Vdash^\ast$ in $V$. Recall the following theorem that is used to justify ctms in the first place:

Whenever $T$ is a consistent theory extending $ZFC$, the thoery $T_{ctm}= ZFC+ ``\dot M\text{ is transitive and countable}"+ ZFC^{\dot M}$ is consistent, where $\dot M$ is an extra constant symbol.

So in for example in your case, assume for a contradiction that $\varphi=$ "$1\not\Vdash^\ast\neg CH$ for the forcing $Add(\omega, \aleph_2)$" holds in $V$. That means that $T=ZFC+\varphi$ is consistent. By the above theorem, we can take $W$ to be a model of $T_{ctm}$ and let $M=\dot M^W$. Suddenly, this situation contradicts what we know about forcing with the countable transitive model $M$ in $W$! Notice that it is not important whether or not $W$ and $M$ are wellfounded from the meta-perspective, as long as $M$ is transitive from the perspective of $W$.

  • 2
    $\begingroup$ The problem with this approach is that it requires a nontrivial metatheoretical action. Namely, reflection and compactness. The approaches where we force over the universe have the benefit that any finitely many classes can be internalized into ZF(C) if necessary, because that does not change the proof by much. So the forcing relation is in fact internalized for any finite part of the theory, including any and all axioms one would use to prove CH. $\endgroup$
    – Asaf Karagila
    Feb 28, 2019 at 0:00

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .