Categorical and Kripke Semantics for Constructive S4 Modal Logic

Abstract. We consider two systems of constructive modal logic which are computationally motivated. Their modalities admit several computational interpretations and are used to capture intensional features such as notions of computation, constraints, concurrency, etc. Both systems have so far been studied mainly from type-theoretic and category-theoretic perspectives, but Kripke models for similar systems were studied independently. Here we bring these threads together and prove duality results which show how to relate Kripke models to algebraic models and these in turn to the appropriate categorical models for these logics.

• Type: Conference
• Year: 2001
• Where: CSL
• Authors: Natasha Alechina, Michael Mendler, Valeria de Paiva, Eike Ritter
• Keywords: Appropriate Categorical Models, Automated Reasoning, Constructive Modal Logic, CSL 2001, Kripke Models