Abstract
This paper is part of a general project of developing a systematic and algebraic proof theory for nonclassical logics. Generalizing our previous work on intuitionistic-substructural axioms and single-conclusion (hyper)sequent calculi, we define a hierarchy on Hilbert axioms in the language of classical linear logic without exponentials. We then give a systematic procedure to transform axioms up to the level \({\mathcal P}_3'\) of the hierarchy into inference rules in multiple-conclusion (hyper)sequent calculi, which enjoy cut-elimination under a certain condition. This allows a systematic treatment of logics which could not be dealt with in the previous approach. Our method also works as a heuristic principle for finding appropriate rules for axioms located at levels higher than \({\mathcal P}_3'\). The case study of Abelian and Łukasiewicz logic is outlined.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Andreoli, J.-M.: Logic programming with focusing proofs in linear logic. Journal of Logic and Computation 2(3), 297–347 (1992)
Avron, A.: Hypersequents, logical consequence and intermediate logics for concurrency. Ann. Math. Artif. Intell. 4, 225–248 (1991)
Ciabattoni, A., Galatos, N., Terui, K.: Algebraic proof theory for substructural logics: Cut-elimination and completions (2008) (submitted)
Ciabattoni, A., Galatos, N., Terui, K.: From axioms to analytic rules in nonclassical logics. In: LICS, pp. 229–240 (2008)
Gispert, J., Torrens, A.: Axiomatic extensions of IMT3 logic. Studia Logica 81(3), 311–324 (2005)
Houston, R.: Finite products are biproducts in a compact closed category. Journal of Pure and Applied Algebra 212(2) (2008)
Kracht, M.: Power and weakness of the modal display calculus. In: Proof theory of modal logic, pp. 93–121. Kluwer, Dordrecht (1996)
Lamarche, F.: On the algebra of structural contexts. Accepted at Mathematical Structures in Computer Science (2001)
Lamarche, F., Retoré, C.: Proof nets for the Lambek-calculus — an overview. In: Abrusci, V.M., Casadio, C. (eds.) Proceedings of the Third Roma Workshop Proofs and Linguistic Categories, pp. 241–262. CLUEB, Bologna (1996)
Lamarche, F., Straßburger, L.: From proof nets to the free *-autonomous category. Logical Methods in Computer Science 2(4:3), 1–44 (2006)
Litak, T., Kowalski, T.: Completions of GBL algebras: negative results. Algebra Universalis 58, 373–384 (2008)
Metcalfe, G.: A sequent calculus for constructive logic with strong negation as a substructural logic. To appear in Bulletin of the Section of Logic
Metcalfe, G.: Proof theory for Casari’s comparative logics. J. Log. Comput. 16(4), 405–422 (2006)
Metcalfe, G., Olivetti, N., Gabbay, D.M.: Sequent and hypersequent calculi for Abelian and Łukasiewicz logics. ACM Trans. Comput. Log. 6(3), 578–613 (2005)
Meyer, R., Slaney, J.: Abelien logic (from A to Z). In: Paraconsistent Logic: Essays on the Inconsistent, pp. 245–288 (1989)
Meyer, R., Slaney, J.: Still adorable, Paraconsistency: The Logical Way to the Inconsistent. In: Proceedings of the world congress on paraconsistency held in Sao Paulo, pp. 241–260 (2002)
Miller, D.: Forum: A multiple-conclusion specification logic. Theoretical Computer Science 165, 201–232 (1996)
Kowalski, T., Galatos, N., Jipsen, P., Ono, H.: Residuated Lattices: an algebraic glimpse at substructural logics. Elsevier, Amsterdam (2007)
Negri, S.: Proof analysis in modal logics. Journal of Philosophical Logic 34(5-6), 507–544 (2005)
Sambin, G., Battilotti, G., Faggian, C.: Basic logic: Reflection, symmetry, visibility. J. Symb. Log. 65(3), 979–1013 (2000)
Schellinx, H.: Some syntactical observations on linear logic. Journal of Logic and Computation 1(4), 537–559 (1991)
Shirahata, M.: A sequent calculus for compact closed categories. Unpublished (2000)
Szabo, M.E.: Polycategories. Comm. Alg. 3, 663–689 (1975)
Terui, K.: Which structural rules admit cut elimination? An algebraic criterion. Journal of Symbolic Logic 72(3), 738–754 (2007)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ciabattoni, A., Straßburger, L., Terui, K. (2009). Expanding the Realm of Systematic Proof Theory. In: Grädel, E., Kahle, R. (eds) Computer Science Logic. CSL 2009. Lecture Notes in Computer Science, vol 5771. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-04027-6_14
Download citation
DOI: https://doi.org/10.1007/978-3-642-04027-6_14
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-04026-9
Online ISBN: 978-3-642-04027-6
eBook Packages: Computer ScienceComputer Science (R0)