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