Hostname: page-component-586b7cd67f-dsjbd Total loading time: 0 Render date: 2024-11-24T16:00:39.582Z Has data issue: false hasContentIssue false
  • English
  • Français

Which structural rules admit cut elimination? An algebraic criterion

Published online by Cambridge University Press:  12 March 2014

Kazushige Terui
Kazushige Terui*
Affiliation:
National Institute of Informatics2-1-2 Hitotsubashi, Chiyoda-Ku Tokyo 101-8430, Japan. E-mail: [email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

Consider a general class of structural inference rules such as exchange, weakening, contraction and their generalizations. Among them, some are harmless but others do harm to cut elimination. Hence it is natural to ask under which condition cut elimination is preserved when a set of structural rules is added to a structure-free logic. The aim of this work is to give such a condition by using algebraic semantics.

We consider full Lambek calculus (FL), i.e., intuitionistic logic without any structural rules, as our basic framework. Residuated lattices are the algebraic structures corresponding to FL. In this setting, we introduce a criterion, called the propagation property, that can be stated both in syntactic and algebraic terminologies. We then show that, for any set ℛ of structural rules, the cut elimination theorem holds for FL enriched with ℛ if and only if ℛ satisfies the propagation property.

As an application, we show that any set ℛ of structural rules can be “completed” into another set ℛ*, so that the cut elimination theorem holds for FL enriched with ℛ*. while the provability remains the same.

Type
Research Article
Information
The Journal of Symbolic Logic , Volume 72 , Issue 3 , September 2007 , pp. 738 - 754
Copyright
Copyright © Association for Symbolic Logic 2007

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

[1] Abrusci, V. M., Phase semantics and sequent calculus for pure noncommutative classical linear propositional logic, this Journal, vol. 56 (1991), pp. 1403–1451.Google Scholar
[2] Avron, A. and Lev, I., Canonical propositional Gentzen-type systems, IJCAR 2001 (Goré, Rajeev, Leitsch, Alexander, and Nipkow, Tobias, editors), Lecture Notes in Artificial Intelligence, vol. 2083, Springer. 2001, pp. 529–543.Google Scholar
[3] Belardinelli, F., Ono, H.. and Jipsen, P., Algebraic aspects of cut elimination, Stadia Logica, vol. 68 (2001). pp. 1–32.Google Scholar
[4] van Benthem, J., Language in Action: Categories, Lambdas and Dynamic Logic, (Studies in Logic 130), North-Holland, Amsterdam, 1991.Google Scholar
[5] Ciabattoni, A., Automated generation of analytic calculi for logics with linearity, CSL 2004 (Marcinkowski, Jerzy and Tarlecki, Andrzej, editors), Lecture Notes in Computer Science, vol. 3210, Springer, 2004, pp. 503–517.Google Scholar
[6] Ciabattoni, A. and Terui, K., Modular cut-elimination: Finding proofs or counterexamples, LPAR 2006 (Hermann, Miki and Voronkov, Andrei, editors), Lecture Notes in Artificial Intelligence, vol. 4246, Springer, 2006, pp. 135–149.Google Scholar
[7] Ciabattoni, A., Towards a semantic characterization of cut-elimination, Stadia Logica, vol. 82 (2006), pp. 95–119.Google Scholar
[8] Došen, K. and Schroeder-Heister, P. (editors), Substructural Logics, Oxford University Press, 1993.Google Scholar
[9] Girard, J.-Y., Linear logic, Theoretical Computer Science, vol. 50 (1987), pp. 1–102.CrossRefGoogle Scholar
[10] Girard, J.-Y., Linear logic: Its syntax and semantics, Advances in Linear Logic (Girard, J.-Y., Lafont, Y., and Regnier, L., editors), Cambridge University Press, 1995, pp. 1–42.CrossRefGoogle Scholar
[11] Girard, J.-Y., On the meaning of logical rules I: Syntax vs. semantics, Computational Logic (Berger, U. and Schwichtenberg, H., editors), Heidelberg Springer-Verlag, 1999, pp. 215–272.Google Scholar
[12] Hori, R., Ono, H., and Schellinx, H., Extending intuitionistic linear logic with knotted structural rules, Notre-Dame Journal of Formal Logic, vol. 35 (1994), no. 2, pp. 219–242.CrossRefGoogle Scholar
[13] Jipsen, J. and Tsinakis, C., A survey of residuated lattices, Ordered Algebraic Structures (Martinez, J., editor), Kluwer Academic Publishes, 2002, pp. 19–56.Google Scholar
[14] Kamide, N., Substructural logics with mingle. Journal of Logic, Language and Information, vol. 11 (2002), no. 2. pp. 227–249.Google Scholar
[15] Miller, D. and Pimentel, E., Using linear logic to reason about sequent systems, Tableaux 2002 (Egly, Uwe and Fermüller, Christian G., editors). Lecture Notes in Computer Science, vol. 2381, Springer, 2002, pp. 2–23.Google Scholar
[16] Ohnishi, M. and Matsumoto, K., A system for strict implication, Annals of the Japan Association for Philosophy of Science, vol. 2 (1964), pp. 183–188.CrossRefGoogle Scholar
[17] Okada, M., Phase semantics for higher order completeness, cut-elimination and normalization proofs (Extended Abstract), Electronic Notes in Theoretical Computer Science, vol.3, a Special Issue on the Linear Logic'96, Tokyo Meeting (J.-Y. Girard, M. Okada, and A. Scedrov, editors), 1996.CrossRefGoogle Scholar
[18] Okada, M., Phase semantic cut-elimination and normalization proofs of first- and higher-order linear logic, Theoretical Computer Science, vol. 227 (1999), pp. 333–396.CrossRefGoogle Scholar
[19] Okada, M., A uniform semantic proof for cut-elimination and completeness of various first and higher order logics, Theoretical Computer Science, vol. 281 (2002), pp. 471–498.CrossRefGoogle Scholar
[20] Okada, M. and Terui, K., The finite model property for various fragments of intuitionistic linear logic, this Journal, vol. 64 (1999), no. 2, pp. 790–802.Google Scholar
[21] Ono, H., Structural rules and a logical hierarchy, Mathematical Logic (Petkov, P. P., editor), Plenum Press, 1990, pp. 95–104.Google Scholar
[22] Ono, H., Semantics for substructural logics, Substructural Logics (Došen, K. and Schroeder-Heister, P., editors), Oxford University Press, 1994, pp. 259–291.Google Scholar
[23] Ono, H., Substructural logics and residuated lattices — An introduction, Trends in Logic, vol. 20 (2003), pp. 177–212.Google Scholar
[24] Restall, G., An Introduction to Substructural Logics, Routledge, London, 1999.Google Scholar
[25] Troelstra, A. S., Lectures on Linear Logic, CSLI Lecture Notes 29, Center for the Study of Language and Information, Stanford, California, 1992.Google Scholar
[26] Zamansky, A. and Avron, A., Canonical Gentzen-type calculi with (n, k)-ary quantifiers, IJCAR 2006 (Furbach, Ulrich and Shankar, Natarajan, editors), Lecture Notes in Artificial Intelligence, vol. 4130, Springer, 2006, pp. 251–265.Google Scholar
[27] Zamansky, A. and Avron, A., Cut-elimination and quantification, Studia Logica, vol. 82 (2006), pp. 157–176.CrossRefGoogle Scholar