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}$.
Categories: math.LO cs.LO