Algebraic proof theory for substructural logics: cut-elimination and completions (Q409322)

The authors propose a new research project, called algebraic proof theory, which aims at identifying the fundamental connections between algebraic and proof-theoretic approaches in logic by a uniform investigation based on the ideas of proof-theoretic treatment of algebraic equations and algebraization of proof-theoretic methods, so that not only the observations already established in each area, respectively, can be made use of commonly, but also some essential characteristics behind them may be understood more clearly. Along this line, this paper investigates the connection between cut elimination and completion in the setting of substructural logics and residuated lattices. The authors first classify logical axioms (algebraic equations) over full Lambek calculus FL by a hierarchy called substructural, which is introduced in a similar way as the arithmetic according to the notion of polarity coming from proof theory of linear logic, and then show that a stronger form of cut elimination for extensions of FL and the MacNeille completion for subvarieties of pointed residuated lattices coincide with respect to the axioms up to certain (rather low) level in the hierarchy, where there are provided also some negative results to indicate limitation of cut elimination and the MacNeille completion, as well as on the expressive power of structural sequent calculus rules.