Joel David Hamkins gave a talk last night on the modal logic of forcing, based on work he had done with Benedikt Löwe. (The talk isn’t listed here yet, but several related ones are.) He said that the aim was to do for forceability what Solovay had done for provability. The idea is that if M is a model of ZFC, and G is some generic filter over some partial order in M, then M[G] is a model of ZFC that is accessible from M, because M has names for all the elements of M[G], and can prove many of the logical relations between facts about M[G] (in fact, in many cases it knows the truth value in M[G] of every sentence with no free variables). Using this accessibility relation, with the “worlds” being models of set theory, we can then define a modal logic. I’ll now write p to be the sentence of set theory (which is in fact expressible standardly) that says that p is true in every generic extension of the actual universe, and <>p the sentence that says that p is true in some generic extension.
It’s easy to see that the following modal axioms are all true for any sentence p:
K is true in any class of worlds with any accessibility relation. S is true because there are partial orders whose forcing is trivial (so M[G]=M). 4 is true because if N=M[G], then N[H]=M[GH], where GH is generic over a sort of product of the partial orders involved in the two individual extensions. .2 is true because we can force over two independent partial orders in the ground model, and the order of the forcing doesn’t matter.
Some other standard axioms for modal logic are false in this interpretation:
5: <>p->p (let p be the claim that some cardinal in L is not a cardinal in V)
M: <>p-><>p (let p be CH)
W5: <>p->(p->p) (let p be the disjunction of the above two claims)
Löb: (p->p)->p (let p be CH)
…and so on.
The goal of the project is to characterize exactly which axioms are valid for the modal logic of forcing. Apparently Solovay showed that S4+Löb is exactly the logic of provability. Hamkins and Löwe have shown that Con(ZFC) implies that the axioms that ZFC proves to be true of this modal logic are exactly those of S4.2 listed above.
However, this is just what ZFC can prove – individual models of ZFC might validate further modal axioms, because they place additional constraints on what forcing extensions are possible. However, they have shown that the class of valid modal axioms will always be a subclass of S5 – at a talk at Berkeley three years ago, Hamkins showed that Con(ZFC) implies there are models for which S5 is the appropriate modal logic (basically, we do some iterated forcing (as in the proof of consistency of Martin’s Axiom) to “push all the buttons”, where a “button” is a sentence that, once it’s forced to be true, will be true in all forcing extensions, so (p->p), like the above claim that some cardinal in L is not a cardinal in V). They don’t yet know whether any intermediate system is possible – one possibility that would give rise to an intermediate system is one in which there is one “unpushed button”, but no two independent buttons. However, they don’t yet know if such a scenario is consistent.