Algebraic proof theory for substructural logics: Cut-elimination and completions |
| |
Authors: | Agata Ciabattoni |
| |
Affiliation: | a Department of Computer Languages, Vienna University of Technology, Favoritenstrasse 9-11, 1040 Wien, Austriab Department of Mathematics, University of Denver, 2360 S. Gaylord St., Denver, CO 80208, USAc Research Institute for Mathematical Sciences, Kyoto University, Kitashirakawa Oiwakecho, Sakyo-ku, Kyoto 606-8502, Japan |
| |
Abstract: | 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 N2 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. |
| |
Keywords: | 03B47 06F05 03G10 08B15 |
本文献已被 ScienceDirect 等数据库收录! |
|