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.
翻译:我们定义了一套与不同的经典模式体系相对应的推定模式逻辑。这些逻辑以Wijesekera的建设性模式逻辑的风格来定义,既有证据理论动机,也有语义动机。一方面,它们与对传统模式逻辑标准序列计算法的单项限制相对应。另一方面,它们通过将直觉学Kripke模型的异端性纳入模式公式的典型满足条款而获得。 我们表明,对于所考虑的经典逻辑而言,证据理论和语义方法回归了同样的建设性体系。