Abstract
We introduce necessary and sufficient conditions for a (single-conclusion) sequent calculus to admit (reductive) cut-elimination. Our conditions are formulated both syntactically and semantically.
Similar content being viewed by others
References
Abrusci, V. M., ‘Non-commutative intuitionistic linear Propositional logic’, Zeit-schrift fur Mathematische Logik und Grundlagen der Mathematik 36: 297–318, 1990.
Avron, A., and I. Lev, ‘Canonical Propositional Gentzen-Type Systems’, Proceedings of IJCAR'01, vol. 2083 LNCS, 2001, pp. 529–543.
Belardinelli, F., H. Ono, and P. Jipsen, ‘Algebraic aspects of cut elimination’, Studia Logica 68: 1–32, 2001.
Belnap, N. D., Jr., ‘Display Logic’, Journal of Philosophical Logic, 11(4):375–417, 1982.
Buss, S., ‘An Introduction to Proof Theory’, Handbook of Proof Theory, Elsevier Science, 1998, pp. 1–78.
Ciabattoni, A., ‘Automated Generation of Analytic Calculi for Logics with Linearity’, Proceedings of CSL'04, vol. 3210 LNCS, 2004, pp. 503–517.
Gentzen, G., ‘Untersuchungenüber das Logische Schliessen’, Math. Zeitschrift 39: 176–210, 405–431, 1935.
Girard, J.-Y., ‘Three valued logics and cut-elimination: the actual meaning of Takeuti's conjecture’, Dissertationes Mathematicae 136: 1–49, 1976.
Girard, J.-Y., Proof Theory and Logical Complexity, Bibliopolis, 1987.
Girard, J.-Y., Y. Lafont, and P. Taylor, Proofs and Types, Cambridge University Press, 1989.
Girard, J.-Y., ‘On the meaning of logical rules I: syntax vs. semantics’, in U. Berger and H. Schwichtenberg, (eds.), Computational Logic, Heidelberg Springer-Verlag, 1999, pp. 215–272.
Hori, R., H. Ono, and H. Schellinx, ‘Extending intuitionistic linear logic with knotted structural rules’, Notre Dame Journal of Formal Logic 35(2):219–242, 1994.
Miller, D., and E. Pimentel, ‘Using Linear Logic to reason about sequent systems’, Proceedings of Tableaux'02, vol. 2381 LNCS, 2002, pp. 2–23.
Okada, M., ‘Phase semantics for higher order completeness, cut-elimination and normalization proofs (extended abstract)’, in J.-Y. Girard, M. Okada, and A. Scedrov, (eds.), ENTCS (Electronic Notes in Theoretical Computer Science) vol.3: A Special Issue on the Linear Logic 96, Tokyo Meeting, Elsevier-ENTCS, 1996.
Okada, M., ‘Phase semantic cut-elimination and normalization proofs of first- and higher-order linear logic’, Theoretical Computer Science 227: 333–396, 1999.
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.
Ono, H., ‘Semantics for substructural logics’, in K. Dosen and P. Schroder-Heister, (eds.), Substructural logics, Oxford University Press, 1994, pp. 259–291.
Prijatelj, A., ‘Bounded Contraction and Gentzen style Formulation of Lukasiewicz Logics’, Studia Logica 57: 437–456, 1996.
Restall, G., An Introduction to Substructural Logics, Routledge, London, 1999.
Schwichtenberg, H., and A. S. Troelstra, Basic Proof Theory (2nd Edition). Cambridge Tracts in Theoretical Computer Science, Cambridge University Press, 2000.
Terui, K., ‘Which Structural Rules Admit Cut Elimination? — An Algebraic Criterion’, Submitted. Available at research.nii.ac.jp/~terui/cut.pdf.
Troelstra, A. S., Lectures on Linear Logic, CSLI Lecture Notes 29, Center for the Study of Language and Information, Stanford, California, 1992.
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
About this article
Cite this article
Ciabattoni, A., Terui, K. Towards a Semantic Characterization of Cut-Elimination. Stud Logica 82, 95–119 (2006). https://doi.org/10.1007/s11225-006-6607-2
Issue Date:
DOI: https://doi.org/10.1007/s11225-006-6607-2