×

Algebraic proof theory for substructural logics: cut-elimination and completions. (English) Zbl 1245.03026

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.

MSC:

03B47 Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics)
03F05 Cut-elimination and normal-form theorems
03G25 Other algebras related to logic

Software:

SQEMA
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Andreoli, J.-M., Logic programming with focusing proofs in linear logic, Journal of Logic and Computation, 2, 3, 297-347 (1992) · Zbl 0764.03020
[2] Avron, A., Hypersequents, logical consequence and intermediate logics for concurrency, Annals of Mathematics and Artificial Intelligence, 4, 225-248 (1991) · Zbl 0865.03042
[3] Avron, A.; Lahav, O., Kripke semantics for basic sequent systems, (Proceedings of Tableaux 2011. Proceedings of Tableaux 2011, LNCS, vol. 6793 (2011)), 43-57 · Zbl 1333.03236
[4] Avron, A.; Zamansky, A., Non-deterministic Semantics for Logical Systems, Handbook of Philosophical Logic, 227-304 (2011)
[5] Banaschewski, B., Hüllensysteme und Erweiterungen von Quasi-Ordnungen, Zeitschrift fur Mathematische Logik und Grundlagen der Mathematik, 2, 35-46 (1956)
[6] Belardinelli, F.; Jipsen, P.; Ono, H., Algebraic aspects of cut-elimination, Studia Logica, 77, 2, 09-240 (2004) · Zbl 1064.03014
[7] Bergman, G., Specially ordered groups, Communications in Algebra, 12, 19-20, 2315-2333 (1984) · Zbl 0506.06006
[8] Bezhanishvili, G.; Harding, J., MacNeille completions of Heyting algebras, The Houston Journal of Math., 30, 4, 937-952 (2004) · Zbl 1066.06005
[9] Buss, S., (An Introduction to Proof Theory. An Introduction to Proof Theory, Handbook of Proof Theory (1998), Elsevier Science), 1-78 · Zbl 0912.03024
[10] Funayama, N., On the completion by cuts of distributive lattices, Proceedings of the Imperial Academy, Tokyo, 20, 1-2 (1944) · Zbl 0063.01484
[11] A. Ciabattoni, N. Galatos, K. Terui, MacNeille Completions of FL-algebras, Algebra Universalis (in press).; A. Ciabattoni, N. Galatos, K. Terui, MacNeille Completions of FL-algebras, Algebra Universalis (in press). · Zbl 1259.03086
[12] Ciabattoni, A.; Galatos, N.; Terui, K., From axioms to analytic rules in nonclassical logics, Proceedings of LICS 2008, 229-240 (2008)
[13] Ciabattoni, A.; Strassburger, L.; Terui, K., Expanding the realm of systematic proof theory, (Proceedings of CSL 2009. Proceedings of CSL 2009, LNCS, vol. 5771 (2009)), 163-178 · Zbl 1257.03084
[14] Ciabattoni, A.; Terui, K., Towards a semantic characterization of cut-elimination, Studia Logica, 82, 1, 95-119 (2006) · Zbl 1105.03057
[15] Conradie, W.; Goranko, V.; Vakarelov, D., Algorithmic correspondence and completeness in modal logic I: the core algorithm SQEMA, Logical Methods in Computer Science, 2, 1:5 (2006) · Zbl 1126.03018
[16] Conradie, W.; Palmigiano, A., Algorithmic correspondence and canonicity for distributive modal logic, Annals of Pure and Applied Logic, 163, 3, 338-376 (2012) · Zbl 1255.03030
[17] Gehrke, M.; Harding, J.; Venema, Y., MacNeille completions and canonical extensions, Transactions of the American Mathematical Society, 358, 573-590 (2006) · Zbl 1083.06009
[18] Galatos, N., Minimal varieties of residuated lattices, Algebra Universalis, 52, 2, 215-239 (2005) · Zbl 1082.06011
[19] N. Galatos, P. Jipsen, Residuated frames with applications to decidability, Transactions of the AMS (in press).; N. Galatos, P. Jipsen, Residuated frames with applications to decidability, Transactions of the AMS (in press). · Zbl 1285.03077
[20] Galatos, N.; Jipsen, P.; Kowalski, T.; Ono, H., Residuated Lattices: an algebraic glimpse at substructural logics, (Studies in Logics and the Foundations of Mathematics (2007), Elsevier) · Zbl 1171.03001
[21] Galatos, N.; Ono, H., Algebraization, parameterized local deduction theorem and interpolation for substructural logics over \(FL\), Studia Logica, 83, 279-308 (2006) · Zbl 1105.03021
[22] Galatos, N.; Ono, H., Cut-elimination and strong separation for substructural logics: an algebraic approach, Annals of Pure and Applied Logic, 161, 9, 1097-1133 (2010) · Zbl 1245.03027
[23] Galatos, N.; Raftery, J., Adding involution to residuated structures, Studia Logica, 77, 2, 181-207 (2004) · Zbl 1062.03059
[24] Harding, J., Completions of ordered algebraic structures: a survey, (Ono; etal., Proceedings of the International Workshop on Interval/Probabilistic Uncertainty and Non-classical Logics. Proceedings of the International Workshop on Interval/Probabilistic Uncertainty and Non-classical Logics, Advances in Soft Computing, vol. 46 (2008), Springer), 231-244 · Zbl 1151.06012
[25] Hori, R.; Ono, H.; Schellinx, H., Extending intuitionistic linear logic with knotted structural rules, Notre Dame Journal of Formal Logic, 35, 2, 219-242 (1994) · Zbl 0812.03008
[26] Jipsen, P.; Tsinakis, C., A survey of residuated lattices, (Martinez, J., Ordered Algebraic Structures (2002), Kluwer Academic Publishers: Kluwer Academic Publishers Dordrecht), 19-56 · Zbl 1070.06005
[27] Jónsson, B.; Tarski, A., Boolean algebras with operators I, American Journal of Math., 73, 891-939 (1951) · Zbl 0045.31505
[28] Jónsson, B.; Tarski, A., Boolean algebras with operators II, American Journal of Math., 74, 127-162 (1952) · Zbl 0045.31601
[29] MacNeille, H. M., Partially ordered sets, Transactions of the American Mathematical Society, 42, 416-460 (1937) · Zbl 0017.33904
[30] Okada, M.; Terui, K., The finite model property for various fragments of intuitionistic linear logic, Journal of Symbolic Logic, 64, 2, 790-802 (1999) · Zbl 0930.03021
[31] Okada, M., Phase semantic cut-elimination and normalization proofs of first- and higher-order linear logic, Theoretical Computer Science, 227, 333-396 (1999) · Zbl 0951.03058
[32] Okada, M., A uniform semantic proof for cut-elimination and completeness of various first and higher order logics, Theoretical Computer Science, 281, 471-498 (2002) · Zbl 1048.03042
[33] Ono, H., Semantics for substructural logics, (Došen, K.; Schröder-Heister, P., Substructural Logics (1994), Oxford University), 259-291 · Zbl 0941.03522
[34] Ono, H., Proof theoretic methods for nonclassical logic — an introduction, (Takahashi, M.; Okada, M.; Dezani-Ciancaglini, M., Theories of Types and Proofs (MSJ Memoir 2) (1998), Mathematical Society of Japan), 207-254 · Zbl 0947.03073
[35] Raftery, J. G., Correspondences between Gentzen and Hilbert systems, Journal of Symbolic Logic, 71, 3, 903-957 (2006) · Zbl 1115.03095
[36] Restall, G., An Introduction to Substructural Logics (1999), Routledge: Routledge London · Zbl 1028.03018
[37] Schmidt, J., Zur Kennzeichnung der Dedekind-MacNeilleschen Hülle einer geordneten Menge, Archiv der Mathematik, 7, 241-249 (1956) · Zbl 0073.03801
[38] Schütte, K., Ein System des Verknüpfenden Schliessens, Archiv fur Mathematische Logik und Grundlagenforschung, 2, 55-67 (1956) · Zbl 0071.00802
[39] Suzuki, T., Canonicity results of substructural and lattice-based logics, Review of Symbolic Logic, 4, 1, 1-42 (2011) · Zbl 1229.03023
[40] Terui, K., Which structural rules admit cut elimination? — an algebraic criterion, Journal of Symbolic Logic, 72, 3, 738-754 (2007) · Zbl 1128.03048
[41] Theunissen, M.; Venema, Y., Macneille completions of lattice expansions, Algebra Universalis, 57, 143-193 (2007) · Zbl 1133.06005
[42] Troelstra, A. S.; Schwichtenberg, H., (Basic Proof Theory. Basic Proof Theory, Cambridge Tracts in Theoretical Computer Science (2000), Cambridge University Press)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.