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.GS5has 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.GBiInthas 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 *local* reduction. This is because the cut on 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}
}
```

[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}
}
```

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 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 has the global subformula property, then all cuts in such a proof are analytic by assumption.

What am I missing?

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.

Ah, I had not appreciated the difference between ‘locally analytic cut’ and ‘globally analytic cut’ here. Thanks for clarifying.