Dual-context Modal Logic as Left Adjoint of Fitch-style Modal Logic
-
- Kakutani Yoshihiko
- Department of Computer Science, The University of Tokyo
-
- Murase Yuito
- Department of Computer Science, The University of Tokyo
-
- Nishiwaki Yuichi
- Department of Computer Science, The University of Tokyo
Abstract
<p>In the stream of studies on intuitionistic modal logic, we can find mainly three kinds of natural deduction systems. For logical aspects, adding axiom schemata is a simple and popular way to construct a system. The Curry-Howard correspondence, however, gives us a connection between logic and computer science. From the viewpoint of programming languages, two more important systems, called a dual-context system and a Fitch-style system, have been proposed. While dual-context systems for S4 are heavily used in the field of staged computation, a dual-context system for K is also studied more recently. In our previous studies, categorical semantics for Fitch-style modal logic is proposed and usefulness of levels is noticed. This paper observes an interesting fact that the box modality of the dual-context system is in fact a left adjoint of that of the Fitch-style system. In order to show the statement, we embed both the two systems, which are refined with levels, into the adjoint calculus that equips an adjunction a priori. Moreover, the adjunction is refined with polarity and the adjoint calculus is extended to polarized logic.</p>
Journal
-
- Journal of Information Processing
-
Journal of Information Processing 27 (0), 77-86, 2019
Information Processing Society of Japan
- Tweet
Details 詳細情報について
-
- CRID
- 1390845713038345088
-
- NII Article ID
- 130007580064
-
- ISSN
- 18826652
-
- Text Lang
- en
-
- Data Source
-
- JaLC
- Crossref
- CiNii Articles
- KAKEN
-
- Abstract License Flag
- Disallowed