Encoding Modal Logics in Logical Frameworks

We present and discuss various formalizations of Modal Logics in Logical Frameworks based on Type Theories. We consider both Hilbert- and Natural Deduction-style proof systems for representing both truth (local) and validity (global) consequence relations for various Modal Logics. We introduce several techniques for encoding the structural peculiarities of necessitation rules, in the typed -calculus metalanguage of the Logical Frameworks. These formalizations yield readily proof-editors for Modal Logics when implemented in Proof Development Environments, such as Coq or LEGO. Keywords: Hilbert and Natural-Deduction proof systems for Modal Logics, Logical Frameworks, Typed -calculus, Proof Assistants. Introduction In this paper we discuss the possibility of designing generalized Natural Deduction-style systems for the important class of non-classical logics, consisting of modal logics. As definition of generalized Natural Deduction-style (ND-style), we take the one provided by type-the..