Residuated Basic Logic II. Interpolation, Decidability and Embedding

TL;DR

This paper establishes the decidability of residuated basic logic by proving its strong finite model property, demonstrates the embedding of intuitionistic logic into basic propositional logic, and analyzes complexity and algebraic properties.

Contribution

It proves the strong finite model property for residuated basic logic and shows embeddings of intuitionistic logic into both basic propositional and modal logics, advancing understanding of their relationships.

Findings

Residuated basic logic has the strong finite model property.

Intuitionistic logic can be embedded into basic propositional logic.

BPL is PSPACE-complete and residuated basic algebras have the finite embeddability property.

Abstract

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