Cut elimination and strong separation for substructural logics: an algebraic approach (Q636346)

By their previous works the authors have already established an algebraic foundation for the study of substructural logics over full Lambek calculus FL by means of residuated lattice-ordered monoids with unit. This paper extends the framework for the sequent system, called GL, obtained from FL by removing the associativity of comma in a sequent. Accordingly, GL is shown to be algebraizable by the variety, called RLUG, of residuated lattice-ordered groupoids with unit. The lack of associativity brings about some technical complications, which however are passed by generalizing the notion of logical matrix and applying the method of quasi-completions to obtain an algebra as well as a quasi-embedding from the matrix to the algebra. On the base of this algebraization the authors show some general results, from which follow several important logical and algebraic properties such as cut elimination for GL, the strong separation of the Hilbert-style system HL equivalent to GL, the finite generation of RLUG, and so on. Moreover, the formalization of GL is presented by taking account of the uniformity and modularity for some principal extensions. That is, depending on how to interpret metavariables used for the formalization it gives rise to FL, Gentzen's LJ, etc., in such a way, for example, as non-associative sequences for GL, sequences for FL, sets for LJ, and so on. Thus, some observations for such extensions are also absorbed in the general results as a matter of fact, and the authors suggest some of the methods developed here would be useful under a still general setting of algebraic logic as well.