An instance of the cut rule is called analytic if the cut formula already appears as a subformula of the lower sequent. For example, the cut
is analytic because the cut formula is contained in
.
Analytic cut can be seen as a deep inference rule. In classical and modal logic it corresponds to a case split on the truth value of a subformula of the lower sequent.
It is clear that some of the objections against the use of cuts in proof search do not apply to analytic cuts. In particular, an analytic cut does not introduce any formula into the premises that does not already appear in the conclusion. There might in fact be reasons to admit analytic cuts even if they are not strictly necessary: For example, d’Agostino and Mondadori [1] showed that LK can the truth table method only through analytic cuts.
In this blog post I want to discuss a different role of analytic cuts: Sometimes sequent calculi for non-classical logics are incomplete without cuts (i.e. cut is not admissible) but they are complete if one admits analytic cuts. This is called the analytic cut property:
Definition. A sequent calculus has the analytic cut property (ACP) if every derivable sequent has a proof whose cuts are analytic.
The ACP is intimately related to the subformula property via the 2]:
due to Kowalski and Ono [Theorem. Let
be a sequent calculus in which cut is the only non-analytic rule. Then
has the ACP iff
has the .
Thus the ACP is the strongest generalisation of cut-admissibility that still guarantees the subformula property of proofs. Smullyan’s paper [3] which coined the term “analytic cut” begins with the following remark:
Now whether one agrees with the above statement or not, it is clear that the ACP can act as a useful substitute for cut-admissibility where the latter is not possible. It is then surprising that, in comparison to cut-admissibility, the ACP has been somewhat neglected in the literature. This is in particular true when it comes to syntactic proofs of the ACP: By this I mean an algorithm that takes a proof in a calculus where cut-elimination is not possible, and successively simplifies all cuts until they are analytic. Until very recently, there seems to have been only one such result (due to Takano [4]) in the literature, dating back more than 30 years!
One might think that the argument for such a “cut-restriction” is like cut-elimination except that the analytic cuts remain. However, things are not quite that easy. In this blog post I sketch below a syntactic proof of the ACP, following the recent approach by Ciabattoni, L. and Ramanayake [5] (arxiv preprint). But before that, let us look at the two main examples.
(1) The best-known calculus that has the ACP but not cut-admissibility is the sequent calculus GS5 [6] for the modal logic S5 of equivalence relations. It extends LK by the following modal rules:
A counter-example to cut-admissibility in GS5 was presented in [7]:
Note however that this cut is analytic! And this is not a coincidence, as Takano showed the following in 1992 [4]:
Theorem. GS5 has the ACP.
Takano’s paper contains the aforementioned only syntactic proof of the ACP of which I am aware.
(2) Bi-intuitionistic logic BiInt is a conservative extension of intuitionistic logic first studied by Rauszer [8, 9]. Syntactically, its calculus GBiInt extends Maehara’s multi-succedent sequent calculus for intuitionistic logic [10] with a connective and the following rules:
As Pinto and Uustalu observed in 2003 (quoted in [11]), the sequent is provable in GBiInt using an (analytic!) cut on the formula
, but it is not provable without cuts. Using semantic methods, Kowalski and Ono confirmed in 2017 [2] that analytic cuts suffice for completeness:
Theorem. GBiInt has the ACP.
Extending Gentzen’s reduction steps
Let me now sketch a syntactic proof of the ACP, focussing on the already mentioned calculus GS5 for modal logic S5.
Although cut-elimination is ultimately not possible in GS5, some of the standard cut reductions do apply. A first naive idea for proving the ACP is therefore to apply these well-known reduction steps “as long as possible” in order to obtain an analytic proof. While this is indeed a part of the argument, it doesn’t suffice: some reduction steps fail irrespective of whether a cut is analytic or not. For example, the following cut is neither principal in GS5, nor can it be shifted upwards:
(show more details)
As the cut formula is principal in , we are tempted to shift the cut upwards in
. But doing so yields the sequent
to which we cannot apply
to get
:
We therefore have to come up with a new reduction step, one that is to be replaced by a cut on a formula that appears possibly deep within
or
. But how would we choose this formula, if not by analysing how the subformulas of
and
are used in the proof? Indeed, we will now take a global view by tracing the cut formula
upwards in
until it is principal in an inference of
:
For simplicity we assume there is just a single context formula . It then turns out that the right move is to replace the cut on
by a cut on
like this:
Here in , we have replaced
everywhere by a formula
on the left. The upper cut
is essentially a principal case reduction and has lower degree than the original
. More interesting is the new cut
on
. Is this progress? Yes! Under on the original derivation
we can show:
- Either
is a subformula of D, or
is a proper subformula of
.
In the first case is analytic, and in the second case
is of smaller degree than
.
This is the key idea behind the new reduction step. It can be extended to an algorithm that restricts all cuts to analytic ones, starting from the uppermost non-analytic cut in a proof. One useful information from the syntactic proof is that only cuts on boxed subformulas ( above) are needed for the completeness of GS5.
(show some more details)
- In the general case, there will not only be one context formula
but multiple formulas
coming from
-many (
) different instances of
above the cut. The solution is to systematically introduce cuts on every
, thereby creating
branches.
- To deal with contraction, the formal argument deals with multicuts instead of cuts on single formulas.
- It can happen that pre-existing analytic cuts in
become non-analytic in
. These will have to be revisited by the algorithm at a later stage. This makes the dynamics of the reduction process quite complex.
Generalising the argument
The above argument for GS5 can be written down abstractly such that it applies to all sequent calculi satisfying certain syntactic restrictions [5]. Informally they can be subsumed as follows: Whenever a standard reduction is not possible in the calculus, then the substitution is well-defined, i.e. it does not break any context restrictions of rules in
. In this way one can obtain a uniform proof of the ACP for both GS5 and GBiInt and some related calculi. This shows that GS5 and GBiInt have the ACP “for the same reason”. For illustration, here is the analogous reduction step for GBiInt:
Some questions around calculi with analytic cuts
We have seen that S5 and BiInt have sequent calculi that are complete if one admits analytic cuts. It is well-known that there are also cutfree calculi for both logics, specifically a hypersequent calculus for S5 [12, 13, 14] and a nested sequent calculus for BiInt [11]. It is then a natural question how sequent calculi with analytic cuts compare to such cutfree extensions of sequent calculi. This question could be answered in different ways.
Scope. Which logics can (or cannot) be captured by a sequent calculus with the ACP? How does this class compare with logics that can be captured by various cutfree hypersequents / nested sequents / deep inference?
Applicability: How useful are sequent calculi with the ACP for proving properties (e.g. decidability, interpolation, finite model property) of a logic? As a first remark, some simple decidability arguments for sequent calculi make use of the subformula property rather than cut-elimination, and therefore go through unchanged in the presence of analytic cuts. For a nontrivial result, [2] derives Craig interpolation of BiInt from the ACP following Maehara’s syntactic method [15]. The same result was later derived from cut-admissibility in the nested sequent calculus [16].
Proof complexity. If a logic admits both a sequent calculus with the ACP and a cutfree extension of the sequent calculus like the hypersequent calculus, how are the proofs in both systems related? Are there efficient translations between both calculi? Here is a
: Cutfree LK cannot p-simulate LK + analytic cuts, and this failure will usually be inherited by extensions of LK: E.g., cutfree hypersequent proofs for S5 cannot p-simulate GS5-proofs with analytic cuts. On the other hand, there might still be a class of modal formulas on which the hypersequent calculus performs better.Further remarks
A different syntactic approach. At least for GS5 and GBiInt there is an alternative syntactic method for proving the ACP. This proceeds by showing that cutfree hypersequent proofs (for S5) or cutfree nested sequent proofs (for BiInt) can be “projected” onto sequent proofs via analytic cuts. A proof sketch for GS5 is in [17]. The method is simpler than what has been described above, but it presupposes cut-elimination in the hypersequent and nested calculus. It is also worth mentioning that the projection leads to an exponential increase in proof size.
Semantics Proofs of the ACP. We mentioned that there is almost no literature on syntactic proofs of the ACP. For semantic proofs, the situation is better understood. Recall that by the result from [2] it suffices to show the subformula property to obtain the ACP. Moreover, the subformula property can be proved by an adaption of a Lindenbaum-style model construction [18, 2].
Modal logic B. Another example for a sequent calculus that is complete with analytic cuts but does not admit cut-elimination is the the sequent calculus GKB for the modal logic of symmetric frames. GKB features the rule
which is itself a potential source of non-analyticity. Therefore, in order to obtain the subformula property one needs to restrict not only the cut rule but also instances of . This can be done by a similar argument as the one sketched above [4].
[Bibtex]
@article{agostino,
title={The taming of the cut. Classical refutations with analytic cut},
author={Agostino, Marcello d' and Mondadori, Marco},
journal={Journal of Logic and Computation},
volume={4},
number={3},
pages={285--319},
year={1994},
publisher={Oxford University Press}
}
[Bibtex]
@article{kowalskiono,
title={Analytic cut and interpolation for bi-intuitionistic logic},
author={Kowalski, Tomasz and Ono, Hiroakira},
journal={The Review of Symbolic Logic},
volume={10},
number={2},
pages={259--283},
year={2017},
publisher={Cambridge University Press}
}
[Bibtex]
@article{smullyan,
title={Analytic cut},
author={Smullyan, Raymond M},
journal={The Journal of Symbolic Logic},
volume={33},
number={4},
pages={560--564},
year={1969},
publisher={Cambridge University Press}
}
[Bibtex]
@article{takano,
title={Subformula property as a substitute for cut-elimination in modal propositional logics},
author={Takano, Mitio},
journal={Mathmatica japonica},
volume={37},
pages={1129--1145},
year={1992}
}
![[doi]](https://prooftheory.blog/wp-content/plugins/papercite/img/external.png)
[Bibtex]
@INPROCEEDINGS{lics23,
author={Ciabattoni, Agata and Lang, Timo and Ramanayake, Revantha},
booktitle={2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)},
title={Cut-Restriction: From Cuts to Analytic Cuts},
year={2023},
volume={},
number={},
pages={1-13},
doi={10.1109/LICS56636.2023.10175785}
}
[Bibtex]
@article{ohnishi1,
title={Gentzen method in modal calculi},
author={Ohnishi, Masao and Matsumoto, Kazuo},
year={1957}
}
[Bibtex]
@article{ohnishi2,
title={Gentzen method in modal calculi. II},
author={Ohnishi, Masao and Matsumoto, Kazuo},
year={1959}
}
[Bibtex]
@book{rauszer1,
title={An algebraic and Kripke-style approach to a certain extension of intuitionistic logic},
author={Rauszer, Cecylia and Rauszer, C},
year={1980},
publisher={Pa{\'n}stwowe Wydawnictwo Naukowe}
}
[Bibtex]
@article{rauszer2,
title={A formalization of the propositional calculus of HB logic},
author={Rauszer, Cecylia},
journal={Studia Logica: An International Journal for Symbolic Logic},
volume={33},
number={1},
pages={23--34},
year={1974},
publisher={JSTOR}
}
[Bibtex]
@article{maehara,
title={Eine Darstellung der intuitionistischen Logik in der klassischen},
author={Maehara, Sh{\^o}ji},
journal={Nagoya mathematical journal},
volume={7},
pages={45--64},
year={1954},
publisher={Cambridge University Press}
}
[Bibtex]
@inproceedings{goree,
title={A cut-free sequent calculus for bi-intuitionistic logic},
author={Buisman, Linda and Gor{\'e}, Rajeev},
booktitle={Automated Reasoning with Analytic Tableaux and Related Methods: 16th International Conference, TABLEAUX 2007, Aix en Provence, France, July 3-6, 2007. Proceedings 16},
pages={90--106},
year={2007},
organization={Springer}
}
[Bibtex]
@article{mints,
title={Some calculi of modal logic},
author={Mints, Grigorii Efroimovich},
journal={Trudy Matematicheskogo Instituta imeni VA Steklova},
volume={98},
pages={88--111},
year={1968},
publisher={Russian Academy of Sciences, Steklov Mathematical Institute of Russian~…}
}
[Bibtex]
@article{pottinger,
title={Uniform, cut-free formulations of T, S4 and S5},
author={Pottinger, Garrel},
journal={Journal of Symbolic Logic},
volume={48},
number={3},
pages={900},
year={1983}
}
[Bibtex]
@book{avron,
title={The method of hypersequents in the proof theory of propositional non-classical logics},
author={Avron, Arnon},
year={1996},
publisher={Citeseer}
}
[Bibtex]
@article{maeharaInter,
title={On the interpolation theorem of Craig},
author={Maehara, Shoji},
journal={Sugaku},
volume={12},
number={4},
pages={235--237},
year={1960}
}


[Bibtex]
@inproceedings{lyon,
title={Syntactic Interpolation for Tense Logics and Bi-Intuitionistic Logic via Nested Sequents},
author={Lyon, Tim and Gor{\'e}, Rajeev},
booktitle={28th
EACSL
Annual Conference on Computer Science Logic, CSL 2020},
pages={1--16},
year={2020},
organization={Schloss Dagstuhl-Leibniz-Zentrum f{\"u}r Informatik}
}
[Bibtex]
@article{jsl,
title={Bounded-analytic sequent calculi and embeddings for hypersequent logics},
author={Ciabattoni, Agata and Lang, Timo and Ramanayake, Revantha},
journal={The Journal of Symbolic Logic},
volume={86},
number={2},
pages={635--668},
year={2021},
publisher={Cambridge University Press}
}
[Bibtex]
@inproceedings{onosurvey,
title={Semantical approach to cut elimination and subformula property in modal logic},
author={Ono, Hiroakira},
booktitle={Structural Analysis of Non-Classical Logics: The Proceedings of the Second Taiwan Philosophical Logic Colloquium},
pages={1--15},
year={2016},
organization={Springer}
}