It seems that, "A can be forced to equal B," allows, "A is possibly equal to B." In possible-worlds lingo, this gets us, "There is a possible world where A = B." Since there are plenty of Bs that plenty of As can be forced to equal, this seems to give us plenty of possible worlds with different set-theoretic facts to their name.

I know there are modal-logic accounts of forcing; is this how they play out?

I ask this because some of the premises in the argument I'm working on are:

  1. ∄ℵω → □(℘(ℵn) = ℵm)
  2. ♢□(℘(ℵn) = ℵm)

But the second statement seems (to me) to possibly(!) beg the question relative to the multiverse point of view, modulo the forcing phenomenon. The first one seems fine except it doesn't seem based on necessity = in all possible worlds...

  • 1
    No. You do not need forcing for this, it follows from the Löwenheim–Skolem theorem that first order theories have multiple models. If you interpret each as a "universe" you'll get a "multiverse". But a platonist does not need to pin their ontology on what's provable in a first order theory we currently happen to use. They can still believe in "one true set universe", Gödel did.
    – Conifold
    Commented Apr 16, 2021 at 18:41

1 Answer 1


While forcing does certainly have serious foundational consequences, I think this is a situation where bringing forcing into the picture makes things seem more mysterious and powerful than they actually are.

Really there are two basic ways we can attach a modal logic to (roughly) a family of structures which are relevant to your OP; one yields a propositional modal logic and the other yields a first-order modal logic. "Models of set theory + forcing" is merely one among many; it helps us understand certain foundational pictures, especially relating to multiverse ideas, but in no sense does it prove any of them. Really, I'd say instead that forcing indicates a rich "modal aspect" to set theory, but this is quite a different thing.

In the rest of this answer I sketch the two approaches mentioned above. This does take things a fair distance from your specific OP, but I think this is still worth doing: I think understanding the more general framework(s) that the various set-theoretic modal logics exist in will help clarify what they (don't) do, foundationally speaking.

(CAVEAT: I've mentioned some as-yet-unpublished work by myself and Wesley Holliday below, since it's relevant; that said, obviously I'm biased as to its significance, so please take this with a grain of salt.)

Ignoring "size issues," here are the two constructions mentioned above (if one really cares, size issues can be fixed as usual by either "setifying" everything a la Grothendieck/Tarski or by just working in a (hyper)class theory).

  • Suppose we have a collection A of structures in the same first-order language and an accessibility relation R between the structures in A. Then there is a natural propositional modal logic attached to the pair (A,R).

  • Suppose we have a collection A of structures in the same first-order language and a collection of maps H between the structures in A. Then there is a natural first-order modal logic attached to the pair (A,H).

Of course we can generalize much further (e.g. look in an arbitrary category), but these are already very interesting. Note that the expressions you mention in your question mix quantification and modalities, so they fall into the second bulletpoint; by contrast, things like "the modal logic of forcing" belong to the first bulletpoint.

Here are the constructions corresponding to the bulletpoints above:

  • The pair (A,R) already defines a Kripke frame with set of worlds A and accessibility relation R. However, we can further restrict attention to "good interpretations" of propositional atoms: we restrict attention to valuations where, for each propositional atom p, there is some first-order sentence p such that p is made true in exactly those elements of A satisfying p according to first-order semantics. This is similar to what happens in provability logic. Basically, we're looking at a Kripke frame together with a semantic commitment about what the propositional atoms could be.

    • To see an example of how this can play out, suppose A is the set of models of T for some complete first-order theory T and R is the complete graph on A (every world sees every other world). In the usual Kripke semantics, "p implies []p" is not validated in the frame (A,R). However, since T is complete every pair of elements of A satisfy all the same first-order sentences, so every "good interpretation" in the above sense makes all worlds look alike and "p implies []p" is part of the modal logic associated to (A,R) per the above! So the restriction on interpretations above is genuinely contentful.

    • This is the context where the modal logic of forcing a la Hamkins/Loewe lives: basically, A is a collection of models of set theory and R is the relation "is a forcing extension of." To emphasize, this is a propositional modal logic.

  • In the second case, the idea is that H carries more information than R: it tells us how one structure can "access" another. This lets us make sense of, for example, "For all x([]P(x))" at a world/structure w in A: that sentence is true iff for every element a of w and every map h: w->u in H we have that P(a) is true in u. This construction, in the specific case where A is the collection of all graphs and H is the collection of all graph embeddings, was studied by Hamkins/Woloszyn here, and with a somewhat different focus by myself and Holliday (sadly languishing, but email me if you're interested in details).

    • This is the situation which fits the examples in your post. Interestingly, while very similar to a large number of approaches to first-order modal logic in the literature (e.g. constant-domain semantics, where in particular at most one map exists between a pair of worlds), I don't know of this exact approach being taken before.

    • Incidentally, we can actually go well beyond first-order modal logic here: there is really a general mechanism for assigning, to a pair (A,H) as above and an abstract logic L, a "modal L-theory" for that pair. This is something I've been looking at recently; interestingly, as far as we know it needs large cardinals to develop a "smooth" theory, although it's not currently known that they're necessary. (This is still being written up, but again email me if you're interested in details.)

  • A quick set of questions before I reveal my vast ignorance: "p implies [] p" means "p implies necessarily p"? Is [] the box operator? Does "P(x)" read as "possibly x"? Commented Apr 17, 2021 at 1:42
  • @KristianBerry Yeah, [] is the box operator; "P" here is just some predicate (I shouldn't have used that letter, I'll fix it in a bit). Commented Apr 17, 2021 at 1:50
  • While I am interested in the details, I fear that I'm not far enough along in my studies to absorb them well enough... For example, I only recently started to understand how large cardinals and model theory are linked, due to reading part of an older article by Levy iirc. Your reply itself opened my eyes to the n-order difference between propositional and predicate logic (I read that propositional logic is considered zeroth-order). So I have a lot to learn... Commented Apr 17, 2021 at 21:17

You must log in to answer this question.

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