Kripke and Boolean Toposes on a Forcing Site over a Countable Model of ZFC

Fix a countable transitive model M of ZFC + CH and allow two kinds of forcing step: adding one Cohen real, or adding ℵ₂ Cohen reals (with ℵ₂ computed in M). The set F_M of models reachable from M by finite chains of such steps carries two natural toposes: the Kripke topos [F_M, Set], whose subterminal objects are the up-sets of F_M, and its double-negation subtopos, the Boolean topos of dense-topology sheaves. For persistent sentences the passage from the first to the second is the modal operator □◇. We compute the continuum hypothesis at three levels: over this site ¬CH is a proper subterminal object of the Kripke topos whose intuitionistic negation is ⊥, while its double negation is the top element. By a theorem of Woodin, F_M is not directed, so the Boolean topos is not Set; but every persistent sentence has a trivial Boolean value. Finally, we prove that the modal logic of F_M under parameter-free sentence valuations is Grz.3 + bd_3 when M is not a one-Cohen-real extension of a ground, and Grz.3 + bd_2 when it is; either way it is strictly stronger than S4.3. The classification was stated by J. D. Hamkins on MathOverflow. Section 5 treats starting models without CH: the logic is always Grz.3 + bd_k with k the number of distinct theories among M, M[c] and M[G], and one coincidence pattern is left open. Sections 1 to 3 are expository; the ingredients of Section 4 are standard and are cited.