Constructive Embedding from Extensions of Logics of Strict Implication into Modal Logics
Constructive Embedding from Extensions of Logics of Strict Implication into Modal Logics
复制标题
从严格蕴涵逻辑扩展到模态逻辑的构造性嵌入
DOI：
10.1007/978-3-662-48357-2_11
复制
发表时间：
2015
期刊：
影响因子：
--
通讯作者：
Sakiko Yamasaki and Katsuhiko Sano
中科院分区：
文献类型：
--
作者：
Keigo Nakajima;Ryozo Ooka;Hideki Kikumoto;山﨑紗紀子;Sakiko Yamasaki and Katsuhiko Sano
Dyckhoff和Negri（Arch Math Logic 51：71-92（2012），[8]）通过标记相继演算给出了从中间逻辑到模态逻辑的Gödel-McKinsey-Tarski嵌入的构造性证明。然后，他们把直觉主义逻辑中原子命题的单调性看作是一个初始条件，即，公理然而，我们把单调性作为一个额外的推理规则，并采用一个修改的翻译发送一个原子变量Pto推广他们的结果从Corsi的严格蕴涵逻辑的扩展到模态逻辑的正常扩展的嵌入。在这个过程中，我们提供了一个风格的标记的Kripke演算的扩展，并表明，我们的演算承认切割规则，并享有健全性和完整性的Kripke语义。
Dyckhoff and Negri (Arch Math Logic 51:71–92 (2012), [8]) give a constructive proof of Gödel–Mckinsey–Tarski embedding from intermediate logics to modal logics via labelled sequent calculi. Then, they regard a monotonicity of atomic propositions in intuitionistic logic as an initial sequent, i.e., an axiom. However, we regard the monotonicity as an additional inference rule and employ a modified translation sending an atomic variablePtoto generalize their result to an embedding from extensions of Corsi’sof logic of strict implication to normal extensions of modal logics. In this process, we provide a-style labelled sequent calculi for extensions ofand show that our calculi admit the cut rule and enjoy soundness and completeness for Kripke semantics.