模态逻辑的双重语境演算
摘要：用于K、T、K4、GL和S4正常模态逻辑的必然性片段的自然演绎系统和相关的模态λ演算被提出。这些系统采用双重上下文风格：它们具有两个不同的假设区域，其中一个可以被认为是模态的，另一个是直观的。我们展示了这些演算的根源是序言演算。然后我们研究它们的元理论，为它们提供了可合流且强范化的化简概念，并且证明它们与通常的希尔伯特系统在可证明性上是一致的。最后，我们研究了一种范畴语义，将模态性解释为一个保留乘积的函子。
作者：G. A. Kavvos
论文ID：1602.04860
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-22