Algebraic proof theory for substructural logics: Cut-elimination and completions

We carry out a unified investigation of two prominent topics in proof theory and order algebra: cut-elimination and completion, in the setting of substructural logics and residuated lattices.We introduce the substructural hierarchy — a new classification of logical axioms (algebraic equations) over full Lambek calculus FL, and show that a stronger form of cut-elimination for extensions of FL and the MacNeille completion for subvarieties of pointed residuated lattices coincide up to the level N2N2 in the hierarchy. Negative results, which indicate limitations of cut-elimination and the MacNeille completion, as well as of the expressive power of structural sequent calculus rules, are also provided.Our arguments interweave proof theory and algebra, leading to an integrated discipline which we call algebraic proof theory.

► Hierarchical classification of axioms for substructural logics and identities for residuated lattices.
► Tight connection between cut elimination (proof theory) and closure under MacNeille completions (order algebra) at low levels in the substructural hierarchy.
► Uniform algebraic proof of cut elimination and closure under completions for a large class of sequent calculi and varieties of residuated lattices.
► Expressive power of structural rules in sequent calculi identified.