Residuated Basic Logic I

We study the residuated basic logic ($\mathsf{R}\mathsf{B}\mathsf{L}$) of residuated basic algebra in which the basic implication of Visser’s basic propositional logic ($\mathsf{B}\mathsf{P}\mathsf{L}$) is interpreted as the right residual of a non-associative binary operator $\cdot$ (product). We develop an algebraic system ${\mathsf{S}}_{\mathsf{R}\mathsf{B}\mathsf{L}}$ of residuated basic algebra by which we show that $\mathsf{R}\mathsf{B}\mathsf{L}$ is a conservative extension of $\mathsf{B}\mathsf{P}\mathsf{L}$. We present the sequent formalization ${\mathsf{L}}_{\mathsf{R}\mathsf{B}\mathsf{L}}$ of ${\mathsf{S}}_{\mathsf{R}\mathsf{B}\mathsf{L}}$ which is an extension of distributive full non-associative Lambek calculus ($\mathsf{D}\mathsf{F}\mathsf{N}\mathsf{L}$), and show that the cut elimination and subformula property hold for it.