# Modal Logic of Forcing The technique of [[forcing]] in set-theory allows us to take a certain model of [[ZFC]] and construct from it a new, larger model. This larger model, called a forcing extension, may satisfy different statements than the original one. We may then say that the statements holding in some forcing extension are "possible" from the point of view of the original model, while statements holding in all forcing extensions are "necessary". This naturally suggests using [[modal logic]] to investigate the properties of the forcing technique, and it also fits well with the [[Kripke semantics|"possible worlds" semantics]] for modal logic - with models of ZFC as worlds, and the accessibility relation being "is a forcing extension of..." . In their paper [[Hamkins, Löwe - The modal logic of forcing|The modal logic of forcing]], Hamkins and Löwe laid the foundation for this investigation, and proved that if ZFC is consistent, then the ZFC-provable principles of forcing, i.e. modal statements $\psi (q_0,...,q_n)$ such that for every set-theoretic statements $\phi_0,...,\phi_n$, $\mathrm{ZFC} \vdash \psi (\phi_0,...,\phi_n)$, are exactly the modal theory known as $\mathsf{S4.2}$. For an extended review see [[Modal logic of forcing - seminar lectures.pdf|here]]. ## Papers on the topic - [[Stavi, Väänänen - Reflection principles for the continuum]] - [[Hamkins - A simple maximality principle]] - [[Hamkins, Löwe - The modal logic of forcing]] - [[Hamkins, Leibman, Löwe - Structural connections between a forcing class and its modal logic]] - [[Hamkins, Löwe - Moving Up and Down in the Generic Multiverse]] - [[Inamdar - On the modal logics of some set-theoretic constructions]] - [[Block, Lowe - MODAL LOGICS AND MULTIVERSES]] - [[Piribauer - The modal logic of generic multiverses]] - [[Hamkins, Linnebo - The modal logic of set-theoretic potentialism and the potentialist maximality principles]] - [[Ya'ar - The modal logic of σ-Centered forcing and related forcing classes]] - [[Xiao - Modal logics and intermediate logics motivated by an open problem on ccc forcing]]