Embedding from multilattice logic into classical logic and vice versa
Norihiro Kamide, Yaroslav Shramko · Journal of Logic and Computation · 2016
This article presents some theorems for syntactic and semantic embeddings of a Gentzen-type sequent calculus MLn for 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 MLn, as well as a modified Craig interpolation theorem. Some of these results are then extended to the first-order system FMLn with implications and co-implications.