Syntactic Proofs of the Analytic Cut Property

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 $\color{red}C$ is contained in $A\rightarrow(B\lor C)$ .

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 efficiently simulate 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 following observation due to Kowalski and Ono [2]:

Theorem. Let $S$ be a sequent calculus in which cut is the only non-analytic rule. Then $S$ has the ACP iff $S$ has the global subformula property.

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:

The real importance of cut-free proofs is not the elimination of cuts per se, but rather that such proofs obey the subformula principle. Raymond Smullyan, 1968.

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 “co-implication” connective $\prec$ and the following rules:

As Pinto and Uustalu observed in 2003 (quoted in [11]), the sequent $p\Rightarrow q,r\rightarrow((p\prec q)\land r)$ is provable in GBiInt using an (analytic!) cut on the formula $p\prec q$ , 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 $\delta$ , we are tempted to shift the cut upwards in $\pi$ . But doing so yields the sequent $\Ra D,E$ to which we cannot apply $(5)$ to get $\Ra\Box D,E$ :

We therefore have to come up with a new reduction step, one that makes the above cut analytic. We remark that we should not hope for a local reduction. This is because the cut on $\Box C$ is to be replaced by a cut on a formula that appears possibly deep within $\Box D$ or $E$ . But how would we choose this formula, if not by analysing how the subformulas of $\Box D$ and $E$ are used in the proof? Indeed, we will now take a global view by tracing the cut formula $\red{\Box C}$ upwards in $\pi$ until it is principal in an inference of $(5)$ :

For simplicity we assume there is just a single context formula $\color{blue}\Box F$ . It then turns out that the right move is to replace the cut on $\color{red}\Box C$ by a cut on $\color{blue}\Box F$ like this:

Here in $\pi_2^*$ , we have replaced $\color{red}\Box C$ everywhere by a formula $\color{blue}\Box F$ on the left. The upper cut $(cut'')$ is essentially a principal case reduction and has lower degree than the original $(cut)$ . More interesting is the new cut $(cut')$ on $\color{blue}\Box F$ . Is this progress? Yes! Under reasonable assumptions on the original derivation $\pi_2$ we can show:

Either $\color{blue}\Box F$ is a subformula of D, or
$\color{blue}\Box F$ is a proper subformula of $\color{red}\Box C$ .

In the first case $(cut')$ is analytic, and in the second case $(cut')$ is of smaller degree than $(cut)$ .

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 ( $\blue{\Box F}$ above) are needed for the completeness of GS5.

(show some more details)

In the general case, there will not only be one context formula $\color{blue} F$ but multiple formulas ${\color{blue} F_1},\ldots,{\color{blue} F_n}$ coming from $m$ -many ( $m\leq n$ ) different instances of $(5)$ above the cut. The solution is to systematically introduce cuts on every ${\color{blue} F_n$ , thereby creating $2^n$ 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 $\pi_2$ become non-analytic in $\pi_2^*$ . 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 $\pi_2\mapsto\pi_2^*$ is well-defined, i.e. it does not break any context restrictions of rules in $\pi_2$ . 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 partial answer: 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 $(B)$ . This can be done by a similar argument as the one sketched above [4].

[1] M. d’ Agostino and M. Mondadori, “The taming of the cut. Classical refutations with analytic cut,” Journal of Logic and Computation, vol. 4, iss. 3, p. 285–319, 1994.
[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}
}

[2] T. Kowalski and H. Ono, “Analytic cut and interpolation for bi-intuitionistic logic,” The Review of Symbolic Logic, vol. 10, iss. 2, p. 259–283, 2017.
[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}
}

[3] R. M. Smullyan, “Analytic cut,” The Journal of Symbolic Logic, vol. 33, iss. 4, p. 560–564, 1969.
[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}
}

[4] M. Takano, “Subformula property as a substitute for cut-elimination in modal propositional logics,” Mathmatica japonica, vol. 37, p. 1129–1145, 1992.
[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}
}

[5]

A. Ciabattoni, T. Lang, and R. Ramanayake, “Cut-Restriction: From Cuts to Analytic Cuts,” in 2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 2023, pp. 1-13.
[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}
}

[6] M. Ohnishi and K. Matsumoto, “Gentzen method in modal calculi,” , 1957.
[Bibtex]

@article{ohnishi1,
title={Gentzen method in modal calculi},
author={Ohnishi, Masao and Matsumoto, Kazuo},
year={1957}
}

[7] M. Ohnishi and K. Matsumoto, “Gentzen method in modal calculi. II,” , 1959.
[Bibtex]

@article{ohnishi2,
title={Gentzen method in modal calculi. II},
author={Ohnishi, Masao and Matsumoto, Kazuo},
year={1959}
}

[8] C. Rauszer and C. Rauszer, An algebraic and Kripke-style approach to a certain extension of intuitionistic logic, Państwowe Wydawnictwo Naukowe, 1980.
[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}
}

[9] C. Rauszer, “A formalization of the propositional calculus of HB logic,” Studia Logica: An International Journal for Symbolic Logic, vol. 33, iss. 1, p. 23–34, 1974.
[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}
}

[10] S. Maehara, “Eine Darstellung der intuitionistischen Logik in der klassischen,” Nagoya mathematical journal, vol. 7, p. 45–64, 1954.
[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}
}

[11] L. Buisman and R. Goré, “A cut-free sequent calculus for bi-intuitionistic logic,” in Automated Reasoning with Analytic Tableaux and Related Methods: 16th International Conference, TABLEAUX 2007, Aix en Provence, France, July 3-6, 2007. Proceedings 16, 2007, p. 90–106.
[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}
}

[12] G. E. Mints, “Some calculi of modal logic,” Trudy Matematicheskogo Instituta imeni VA Steklova, vol. 98, p. 88–111, 1968.
[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~…}
}

[13] G. Pottinger, “Uniform, cut-free formulations of T, S4 and S5,” Journal of Symbolic Logic, vol. 48, iss. 3, p. 900, 1983.
[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}
}

[14] A. Avron, The method of hypersequents in the proof theory of propositional non-classical logics, Citeseer, 1996.
[Bibtex]

@book{avron,
title={The method of hypersequents in the proof theory of propositional non-classical logics},
author={Avron, Arnon},
year={1996},
publisher={Citeseer}
}

[15] S. Maehara, “On the interpolation theorem of Craig,” Sugaku, vol. 12, iss. 4, p. 235–237, 1960.
[Bibtex]

@article{maeharaInter,
title={On the interpolation theorem of Craig},
author={Maehara, Shoji},
journal={Sugaku},
volume={12},
number={4},
pages={235--237},
year={1960}
}

[16] T. Lyon and R. Goré, “Syntactic Interpolation for Tense Logics and Bi-Intuitionistic Logic via Nested Sequents,” in 28th $\{$ EACSL $\}$ Annual Conference on Computer Science Logic, CSL 2020, 2020, p. 1–16.
[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}
}

[17] A. Ciabattoni, T. Lang, and R. Ramanayake, “Bounded-analytic sequent calculi and embeddings for hypersequent logics,” The Journal of Symbolic Logic, vol. 86, iss. 2, p. 635–668, 2021.
[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}
}

[18] H. Ono, “Semantical approach to cut elimination and subformula property in modal logic,” in Structural Analysis of Non-Classical Logics: The Proceedings of the Second Taiwan Philosophical Logic Colloquium, 2016, p. 1–15.
[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}
}

3 thoughts on “Syntactic Proofs of the Analytic Cut Property”

Anupam Das says:
October 12, 2023 at 6:05 pm
Hi Timo, thanks for the illuminating post. I am not sure I see why the first Theorem you stated, due to Kowalski and Ono, has a nontrivial direction (as the tooltip suggests).
– if $S$ has the ACP then each formula occurring in a proof is a subformula of the conclusion or a cut formula, and so is again a subformula of the conclusion if all cuts are analytic.
– if $S$ has the global subformula property, then all cuts in such a proof are analytic by assumption.
What am I missing?
Timo Lang says:
October 13, 2023 at 9:08 am
Hi Anupam!
Thank you for this question. Short answer: The global subformula property states that formulas in the proof are subformulas of the endsequent. This does not imply that locally, every formula occurrence is a subformula of the sequent immediately below it. In particular it does not imply that all cuts in such a proof are analytic.
For the longer answer, let me repeat and introduce some terminology first. We say that a proof has the local (resp. global) subformula property if every formula occurrence in it is a subformula of the sequent immediately below it (resp. a subformula of the endsequent). A sequent calculus has the local (resp. global) subformula property if every valid sequent has a proof with the local (resp. global) subformula property.
Clearly the local property implies the global one, both at the level of proofs and (therefore) at the level of sequent calculi. The converse direction *fails* at the level of proofs: A proof can have the global subformula property without having the local one. E.g. think of a proof that, reading bottom-up, first weakens a formula and then reintroduces it via cut.
At the level of sequent caluli, however, the global=>local direction *does* hold. This is the nontrivial part shown by Ono and Kowalski. You can find the argument in Lemma 4.6 of their paper: it is elegant and not hard.
1. Anupam Das says:
  October 16, 2023 at 4:09 pm
  Ah, I had not appreciated the difference between ‘locally analytic cut’ and ‘globally analytic cut’ here. Thanks for clarifying.

Extending Gentzen’s reduction steps

Generalising the argument

Some questions around calculi with analytic cuts

Further remarks

3 thoughts on “Syntactic Proofs of the Analytic Cut Property”

Leave a Reply Cancel reply