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

作者：Ciabattoni Agata; Galatos Nikolaos; Terui Kazushige^*

来源：Annals of Pure and Applied Logic, 2012, 163(3): 266-290.

DOI：10.1016/j.apal.2011.09.003

• Substructural logic
• Gentzen system
• Residuated lattices
• Cut-elimination
• Structural rule
• MacNeille 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. %26lt;br%26gt;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 N-2 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. %26lt;br%26gt;Our arguments interweave proof theory and algebra, leading to an integrated discipline which we call algebraic proof theory.

• 出版日期2012-3