A calculus for modal compact Hausdorff spaces

The symmetric strict implication calculus 𝖲^2𝖨𝖢, introduced in [5], is a modal calculus for compact Hausdorff spaces. This is established through de Vries duality, linking compact Hausdorff spaces with de Vries algebras-complete Boolean algebras equipped with a special relation. Modal compact Hausdorff spaces are compact Hausdorff spaces enriched with a continuous relation. These spaces correspond, via modalized de Vries duality of [3], to upper continuous modal de Vries algebras. In this paper we introduce the modal symmetric strict implication calculus 𝖬𝖲^2𝖨𝖢, which extends 𝖲^2𝖨𝖢. We prove that 𝖬𝖲^2𝖨𝖢 is strongly sound and complete with respect to upper continuous modal de Vries algebras, thereby providing a logical calculus for modal compact Hausdorff spaces. We also develop a relational semantics for 𝖬𝖲^2𝖨𝖢 that we employ to show admissibility of various Π_2-rules in this system.