Residuated Basic Logic I

TL;DR

This paper introduces residuated basic logic ($ ext{RBL}$), an extension of basic propositional logic with algebraic and sequent calculus formalizations, demonstrating cut elimination and subformula properties.

Contribution

It develops an algebraic system for $ ext{RBL}$, showing it conservatively extends $ ext{BPL}$, and formalizes it via a sequent calculus with key proof-theoretic properties.

Findings

$ ext{RBL}$ is a conservative extension of $ ext{BPL}$

The sequent calculus $ ext{L}_{ ext{RBL}}$ admits cut elimination

The calculus satisfies the subformula property

Abstract

We study the residuated basic logic ($\mathsf{RBL}$) of residuated basic algebra in which the basic implication of Visser's basic propositional logic ($\mathsf{BPL}$) is interpreted as the right residual of a non-associative binary operator $\cdot$ (product). We develop an algebraic system $\mathsf{S_{RBL}}$ of residuated basic algebra by which we show that $\mathsf{RBL}$ is a conservative extension of $\mathsf{BPL}$. We present the sequent formalization $\mathsf{L_{RBL}}$ of $\mathsf{S_{RBL}}$ which is an extension of distributive full non-associative Lambek calculus ($\mathsf{DFNL}$), and show that the cut elimination and subformula property hold for it.