Cut elimination and strong separation for substructural logics: An algebraic approach

Abstract. We develop a general algebraic and proof-theoretic study of substructural logics that may lack associativity, along with other structural rules. Our study extends existing work on (associative) substructural logics over the full Lambek Calculus FL (see e.g. [36, 19, 18]). We present a Gentzen-style sequent system GL that lacks the structural rules of contraction, weakening, exchange and associativity, and can be considered a non-associative formulation of FL. Moreover, we introduce an equivalent Hilbert-style system HL and show that the logic associated with GL and HL is algebraizable, with the variety of residuated lattice-ordered groupoids with unit serving as its equivalent algebraic semantics. Overcoming technical complications arising from the lack of associativity, we introduce a generalized version of a logical matrix and apply the method of quasicompletions to obtain an algebra and a quasiembedding from the matrix to the algebra. By applying the general result to spec...

• Type: Journal
• Year: 2010
• Where: APAL
• Authors: Nikolaos Galatos, Hiroakira Ono
• Keywords: APAL 2010, Associativity, Structural Rules, Substructural Logics