论文标题
Wijesekera风格的建设性模态逻辑
Wijesekera-style constructive modal logics
论文作者
论文摘要
我们定义了一个命题的建设性模态逻辑家族，将每个逻辑都与不同的经典模态系统相对应。逻辑是通过Wijesekera的建设性模态逻辑的风格定义的，并且在理论上和语义上都是证明的。一方面，它们对应于经典模态逻辑的标准序列结石的单度限制。另一方面，它们是通过将直觉的Kripke模型的遗传性纳入模态公式的经典满意度子句中获得的。我们表明，对于经典的逻辑，证明理论和语义方法返回相同的建设性系统。
We define a family of propositional constructive modal logics corresponding each to a different classical modal system. The logics are defined in the style of Wijesekera's constructive modal logic, and are both proof-theoretically and semantically motivated. On the one hand, they correspond to the single-succedent restriction of standard sequent calculi for classical modal logics. On the other hand, they are obtained by incorporating the hereditariness of intuitionistic Kripke models into the classical satisfaction clauses for modal formulas. We show that, for the considered classical logics, the proof-theoretical and the semantical approach return the same constructive systems.
