The Internal Modal Logic of Forcing

We connect modal set theory with Boolean-valued models by developing an \emph{internal} Kripke semantics for modal formulas whose atomic propositions are set-theoretic sentences. Given a complete Boolean algebra $B$, we view its elements as ``local perspectives on truth'' inside the Boolean-valued universe $V^{(B)}$ and interpret the modal operators using an accessibility relation $R$ on $B$ defined by \emph{co-consistency} (equivalently, Boolean compatibility): $aRb$ iff $a\wedge b\neq 0$. Our central conceptual point is that, for set-theoretic sentences $p$, the internal modality $\Diamond p$ holds at $b$ iff there is an ultrafilter $U$ of $B$ containing $b$ such that the classical quotient $V^{(B)}/U$ satisfies $p$. We compute several general and algebra-dependent modal validities, and analyze the special behavior of complete atomic Boolean algebras. Finally, adopting a translation-based semantics on the nonzero part $B^+=B\setminus\{0\}$, we prove a soundness-and-completeness theorem: the normal logic $\KTB$ is exactly the set of modal formulas valid in all translated co-consistency models with parameters.