Residuated Basic Logic II. Interpolation, Decidability and Embedding

We prove that the sequent calculus ${\mathsf{L}}_{\mathsf{R}\mathsf{B}\mathsf{L}}$ for residuated basic logic $\mathsf{R}\mathsf{B}\mathsf{L}$ has strong finite model property, and that intuitionistic logic can be embedded into basic propositional logic $\mathsf{B}\mathsf{P}\mathsf{L}$. Thus $\mathsf{R}\mathsf{B}\mathsf{L}$ is decidable. Moreover, it follows that the class of residuated basic algebras has the finite embeddability property, and that $\mathsf{B}\mathsf{P}\mathsf{L}$ is PSPACE-complete, and that intuitionistic logic can be embedded into the modal logic $\mathsf{K}\mathsf{4}$.