Residuated Basic Logic II. Interpolation, Decidability and Embedding

2014/02/24 by Minghui Ma, Zhe Lin, Ma, Minghui +1
Computer Science · Mathematics · #03B47 #F.4.1 #FOS: Computer and information sciences #FOS: Mathematics #Logic (math.LO) #Logic in Computer Science (cs.LO) #acm:03B47 #cs.LO #math.LO #msc:03B47

paper · pdf · doi:10.48550/arxiv.1404.7401

17 pages with 1 figure

arxiv created 2014/02/24 · arxiv updated 2014/04/30

Abstract

We prove that the sequent calculus \mathsfL_RBL for residuated basic logic RBL has strong finite model property, and that intuitionistic logic can be embedded into basic propositional logic BPL. Thus RBL is decidable. Moreover, it follows that the class of residuated basic algebras has the finite embeddability property, and that BPL is PSPACE-complete, and that intuitionistic logic can be embedded into the modal logic K4.

Related

• Residuated Basic Logic I
• Intuitionistic modal logic LIK4 is decidable
• Nested Sequents for Intuitionistic Multi-Modal Logics: Modularity, Cut-Elimination, and Undecidability
• First-Order Intuitionistic Logic with Decidable Propositional Atoms
• Intuitionistic modal logics: new and simpler decidability proofs for FIK and LIK