Modal Logic of Transition Systems in the Topos of Trees
Colin Riba, Guilhem Jaber · HAL (Le Centre pour la Communication Scientifique Directe) · 2017
We investigate the adjunction between the category of transition systems (with not nec. bounded morphisms) and the topos of trees S from the perspective of the basic modal logic K on transition systems. More specifically, we show how the modal logic K over an object of S seen as a transition system can be lifted back as a subobject of S. This relies on the usual mutually transpose formulations of modal satisfaction as either a map of transition system or as a map of Boolean algebras with operators. Moreover, thanks to the usual geometric morphism from the Boolean topos Psh(|N * |) of presheaves over the discrete category of natural numbers to S , we can give a characterization of modal satisfaction within S as a map from formulae to total subobjects of S whose image in the Boolean topos Psh(|N * |) is an internal map of Boolean algebras.