Residuated Basic Logic I

2014/02/24 by Minghui Ma, Zhe Lin, Ma, Minghui +1
Computer Science · Mathematics · #03B47 #F.4.1 #FOS: Computer and information sciences #FOS: Mathematics #Logic (math.LO) #Logic in Computer Science (cs.LO) #acm:03B47 #cs.LO #math.LO #msc:03B47

paper · pdf · doi:10.48550/arxiv.1403.3354

18 pages with 1 figure

arxiv created 2014/02/24 · arxiv updated 2014/03/14

Abstract

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

Related

• Residuated Basic Logic II. Interpolation, Decidability and Embedding
• The Distributive Full Lambek Calculus with Modal Operators
• Subreflexive Logic: Completeness without Identity
• Residuation algebras with functional duals
• Injectives in residuated algebras