Sequent calculi with restricted cuts for non-classical logics
The primary motivation for cut-elimination is that it leads to a proof calculus with the subformula property. Such a proof calculus has a restricted proof search space and this is a powerful aid for investigating the properties of the logic. Unfortunately, many substructural and modal logics of interest lack a sequent calculus that supports cut-elimination. The overwhelming response since the 1960s has been to generalise the sequent calculus in a bid to regain cut-elimination. The price is that these generalised formalisms are more complicated to reason about and implement.
There is an alternative: remain with the sequent calculus by accepting weaker (but still meaningful) versions of the subformula property. We will discuss how cut-free hypersequent proofs can be transformed into sequent calculus proofs in a controlled way [1]. Combined with the quite general methodology [2] for transforming Hilbert axiomatic extensions into cut-free hypersequent calculi, this leads to an algorithm taking a Hilbert axiomatic extension to a sequent calculus with a weak subformula property.
Can we avoid this detour through the hypersequent calculus? This goes to the heart of a new programme called cut-restriction that aims to adapt Gentzen’s celebrated cut-elimination argument systematically so that cut-formulas are restricted (when elimination is not possible). We will present the early results in this programme: from arbitrary cuts to analytic cuts in the sequent calculi for bi-intuitionistic logic and S5 via a uniform cut-restriction argument (the results themselves are well-known).
Based on joint work with Agata Ciabattoni (TU Wien) and Timo Lang (UCL).
References
- [1]
- Agata Ciabattoni and Timo Lang and Revantha Ramanayake, Bounded-analytic Sequent Calculi and Embeddings for Hypersequent Logics, Journal of Symbolic Logic, vol. 86 (2021), no. 2, pp. 635–668.
- [2]
- A. Ciabattoni and N. Galatos and K. Terui, From axioms to analytic rules in nonclassical logics, Proceedings of the Twenty-Third Annual IEEE Symposium on Logic in Computer Science (LICS) Pittsburgh, PA, USA, IEEE Computer Society, 2008, pp. 229–240.
This document was translated from LATEX by HEVEA.