Substructural logic with Galois connection

2014 Fiscal Year Final Research Report

• Project/Area Number: 24500024
• Research Category: Grant-in-Aid for Scientific Research (C)
• Allocation Type: Multi-year Fund
• Section: 一般
• Research Field: Fundamental theory of informatics
• Research Institution: Tokyo Denki University
• Principal Investigator: KONDO Michiro 東京電機大学, 情報環境学部, 教授 (40211916)
• Project Period (FY): 2012-04-01 – 2015-03-31
• Keywords: 部分構造論理 / 剰余束 / 決定可能性 / ガロア結合

Outline of Final Research Achievements

In order to solve the open problem "Is the Intuitionistic tense logic decidable?", we generalized the problem to that of substructural logic with Galois connection and considered algebraic properties of residuated lattices with Galois connection. At first we proved the characterization theorem of residuated lattices with an operator representing the modal operator. Next we considered properties of residuated lattices with two operators as Galois connection and proved that the intuitionistic modal logic was decidable. Moreover we also verified that the intuitionistic tense logic was a fusion of intuitionistic modal logics. It follows from a well-known result that a fusion of decidable logics is also decidable that our results give a proof that the intuitionistic tense logic is decidable, which was the open problem since at least 1984.

Free Research Field

数理論理学