Philosophy of forcing and ctm

Question

I asked a similar question on SE before and received an answer. Not completely convinced, I decided to ask it here with some modifications. Note: I understand how forcing works and how it proves relative consistency statement in the metatheory; this question is more about the philosophical interpretation, hence the tag "soft-question".

There are mainly two approaches to forcing as far as I know: the internal approach, usually with a complete Boolean algebra, and the external approach, using a countable transitive model (ctm). While the internal approach is elegant and intuitive in my opinion, it only creates a Boolean-valued model instead of a usual transitive model. Moreover my impression is that this is not how people usually think about forcing; I feel that when people do forcing they really imagine that some new set is created out of thin air and thrown into the current universe.

Now for the ctm approach. The problem (I feel) is that it only creates a ctm. All kinds of stange stuff can happen for ctm:

1. (Hamkins) A ctm can be pointwise definable.
2. (Hamkins) Every ctm embeds into its own constructible universe.
3. There exists a statement $\phi$ such that ZFC+"there is a countable transitive model of ZFC$+\phi$" is consistent (relative to some reasonable hypothesis), while it becomes inconsistent if the word countable is changed to uncountable. An example of $\phi$ is "there does not exist ctm of ZFC" (consider the minimal model). Is there a more interesting example? I think if a statement has no uncountable transitive model then it "obviously should not be true", even if there is a consistency proof via forcing or whatever. Edit: seems like such a $\phi$ cannot be too interesting, because as long as $\phi$ is consistent with "$Ord$ is Mahlo", then by reflection there exists inaccessible $\kappa$ such that $V_\kappa\models\phi$.

Basically, my question is why should one believe that forcing is meaningful? Yes forcing shows there is a ctm of $\lnot$CH, so $\lnot$CH is consistent, but could that be merely a pathology about ctm, just like 1-3 above? I mean there is also a model of ZFC+$\lnot$Con(ZFC), but it has to be ill-founded so nobody believes this should actually be the case; I don't feel much better about ctm than ill-founded model. For the particular case of $\lnot$CH, another doubt of mine is that the von-Neumann hierarchy picture is often used to justify the consistency of ZFC, but the idea of forcing seems to say that we actually never reach the "true" power set of a set, so the hierarchy cannot proceed in the first place. Of course large cardinals directly imply the consistency of $\lnot$CH, but that is another story.

Here is another fun thought (to add more vagueness to this question): set theory people often start a sentence with "collapse $X$ to a countable set". If we take this seriously, does it mean actually all sets are countable, and uncountability is just an illusion? Dana Scott seems to share a similar view in his foreword to the book Set Theory: Boolean-Valued Models and Independence Proofs:

......Perhaps we would be pushed in the end to say that all sets are countable (and that the continuum is not even a set) when at last all cardinals are absolutely destroyed. But really pleasant axioms have not been produced......

Answer 1

It's not clear to me exactly what your question is. Certainly nobody literally thinks that if a statement can be forced then it is probably true, since we can force mutually contradictory statements. The primary role that forcing plays in day-to-day life is to investigate consistency rather than truth.

Maybe you're asking about the debate, reported in Scientific American and elsewhere, about whether to "accept" forcing axioms such as Martin's Maximum, as opposed to something like V = Ultimate L that is more motivated by inner models. From what I've heard, even the proponents of forcing axioms don't argue that "forcing is meaningful" in the sense that forcing directly suggests to us what is true. Rather, the motivation is that forcing axioms (allegedly) are more "fruitful," facilitating investigations into various mathematical structures. So if you're casting around for insights into what is "really true," then I don't think that forcing is going to give you any joy, at least not directly.

As for whether uncountable sets are illusory—if you want to argue the point mathematically as opposed to purely philosophically, then the burden of proof is on you to come up with some kind of mathematical framework in which (for example) Cantor's diagonal argument is blocked. As Dana Scott said, nobody seems to have come up with any attractive proposals in this direction.

Answer 2

I think the point of the countable transitive model approach is twofold. On the one hand it eliminates independence in independence results (which even just sounds icky) and on the other hand it ties independence back to proof theory, which I think is the right way to think of independence (though this is probably controversial). Let me be a little more specific.

First observe the following:

Theorem: It is independent of ZFC + ``there is a standard model of ZFC" whether or not there exists an uncountable standard model of ZFC + $\neg$CH.

Proof: As noted in the comments (though somewhat incorrectly-later corrected in a separate question), Cohen observed that $V= L$ (in fact ``every real is constructible") implies that every standard uncountable model must satisfy CH. This is because any such model contains all countable ordinals hence all constructible reals (and hence all reals) and can recognize then that all reals are constructible so CH holds. Conversely for any forcing notion $\mathbb P$ and any cardinal $\kappa$ Martin's Axiom for $\mathbb P$ at $\kappa$ is equivalent to the statement that all transitive models $M \ni \mathbb P$ of a sufficient fragment of ZFC of size $\leq \kappa$ have a $\mathbb P$-generic $G$. In particular if there is a standard model $M$ of ZFC of size $\aleph_1$ and Martin's Axiom holds at $\aleph_1$ for the forcing to add $\aleph_2$ many Cohen reals then we can force over $M$ to obtain a model of $\neg$CH.

The point of all this is that the assumptions $V=L$ and Martin's Axiom hold not in the model $M$ but rather in the ambient set theoretic universe (what set theorists somewhat blithely refer to as ``the real world" on occasion). By contrast forcing over countable models is a ZFC theorem so one need not assume anything about the real world. In particular if $V=L$ for example then there may still be countable transitive models of $V\neq L$ and even $\neg$CH so we didn't have to assume anything from the get-go to prove the independence result which is obviously desired.

But maybe you still think countable models are somehow artificial. This may be true but if you read Cohen's ``The Discovery of Forcing" he notes his original idea for proving independence was to somehow diagonalize over proofs, which I actually think is a good idea. We're saying there is no proof of BLAH and diagonalization is the method par excellence for logicians of proving there isn't a BLAH (a countable enumeration of the reals, a PA proof of the consistency of PA, an algorithm for solving the halting problem...). Now there are only countably many proofs in ZFC and to my mind what's really going on in forcing over countable models is that we are handeling them one at a time in countably many steps. The ctm is simply a stand in for this type of enumeration.

Let me explain. By the truth lemma every statement true in a forcing extension was forced to be true by some specific condition i.e. there is some relatively concrete witness to its truth (it's not a coincidence realizability semantics use the forcing symbol as well). At the stage where we forced some given statement we gave a concrete example as to why there is no proof in ZFC for its negation. Since there are only countable many proofs, the use of a countable model is justified in guiding our construction.

Obviously this is a philosophical point that satisfies my intuition, though not necessarily anyone else's, however I hope it's at least a new perspective. Let me just end by saying that both forcing and inner model constructions are predicative/vaguely intuitionistic (though obviously not in a formal sense) and I think that it's not a coincidence that these are the only methods we have for proving independence over ZFC. Both rely on the translation of proof theoretic ideas to a model theoretic context and this seems necessary since ultimately we're making a proof theoretic argument.

Answer 3

A little while ago, I wrote a paper addressing some linked worries to what you have here:

Barton, N. Forcing and the Universe of Sets: Must We Lose Insight?. J Philos Logic 49, 575–612 (2020). https://doi.org/10.1007/s10992-019-09530-y

I'll add a very brief summary of what I argue there:

1. There's pressure to want to provide "nice" interpretations of forcing, since forcing is more than just a tool for proving relative consistency. We can also formulate axioms about uncountable sets using forcing (e.g. remarkable cardinals) and prove theorems about uncountable sets in the universe using forcing (cf. Todorčević and Farah's book, Malliaris and Shelah's result that $\mathfrak{p}=\mathfrak{t}$).

2. You can get "nice" interpretations of forcing within the universe, where the model you use is very "close" to $V$ in certain senses. In this sense, studying forcing can be differentiated from the case of $\sf ZFC$ + $\neg Con(\mathsf{ZFC})$ that you point to.