Embedding from multilattice logic into classical logic and vice versa
Embedding from multilattice logic into classical logic and vice versa
复制标题
从多格逻辑嵌入经典逻辑，反之亦然
DOI：
10.1093/logcom/exw015
复制
发表时间：
2017
影响因子：
0.7
通讯作者：
Yaroslav Shramko
中科院分区：
文献类型：
--
作者：
Norihiro Kamide;Yaroslav Shramko
本文给出了多格逻辑的Gentzen型序列演算ML到经典逻辑的Gentzen型序列演算LK的语法和语义嵌入定理，反之亦然。这些嵌入定理被用来证明ML的割消去、可判断性和完备性定理，以及修正的Craig插值定理。然后将这些结果中的一些结果推广到一阶系统FML，并给出了它们的含义和共同含义。
This article presents some theorems for syntactic and semantic embeddings of a Gentzen-type sequent calculus MLfor multilattice logic into a Gentzen-type sequent calculus LK for classical logic and vice versa. These embedding theorems are used to prove cut-elimination, decidability and completeness theorems for ML, as well as a modified Craig interpolation theorem. Some of these results are then extended to the first-order system FMLwith implications and co-implications.