Proof-Theoretic Embedding from Visser's Basic Propositional Logic to Modal Logic K4 via Non-labelled Sequent Calculi
Proof-Theoretic Embedding from Visser's Basic Propositional Logic to Modal Logic K4 via Non-labelled Sequent Calculi
复制标题
通过非标记序列演算从 Visser 的基本命题逻辑到模态逻辑 K4 的证明理论嵌入
DOI：
10.1007/978-981-10-6355-8_12
复制
发表时间：
2017
期刊：
影响因子：
--
通讯作者：
Sakiko Yamasaki and Katsuhiko Sano
中科院分区：
文献类型：
--
作者：
Ryo Hatano;Katsuhiko Sano;and Satoshi Tojo;Sakiko Yamasaki and Katsuhiko Sano
Albert Visser从Kripke语义学中去掉了对直觉逻辑的反身性要求，从而引入了一种称为基本命题逻辑（Basic Propositional Logic）的次直觉逻辑，并通过语义学方法证明了它可以嵌入模态逻辑。本文给出了一个无压缩的非标号的割演算，并证明了该演算具有割的容许性。此外，我们通过Gödel-McKinsey-Tarski翻译建立了一个证明理论嵌入。
Albert Visser introduced a subintuitionistic logic called Basic Propositional Logic () by dropping the requirement of reflexivity from Kripke semantics for intuitionistic logic, and he showed thatcan be embedded into modal logicby a semantic method. This paper provides a contraction-free non-labelled sequent calculus forand shows that the calculus enjoys the admissibility of cut. Moreover, we establish a proof-theoretic embedding fromintovia a Gödel–McKinsey–Tarski translation.