‘Simple’ proofs of cut-elimination: classical logic

In the last couple years, I have taught cut-elimination several times to research-level students (ESSLLI ’18, LSS ’18, and to PhD students at the University of Birmingham). Every time I am left squirming when I have to deal with the monster in the closet: contractionContraction allows us to merge copies of the same formula on the same side of a sequent..

Most cut-elimination proofs do something like this:

1. Main induction on the multiset of cut degreesThe degree of a cut is the number of connectives in its cut formula. in a proof.
2. A sub-induction on the height'Height' is a bit of a misnomer here, since the simplest working measure is usually 'size'. of a proof.

Most cut-reduction steps play well with these measures, but the contraction step a priori is particularly nasty:

This step will be a known foe to many proof theorists, replacing a cut on with two cuts on ! This actually increases the measure (1) above, and appealing to (2) to eliminate the upper cut of the RHS does not helpHeight below a cut is not preserved by cut-reduction. Indeed, the step above creates many contraction steps below the two cuts. us eliminate the lower one. There are various (well-known) solutions to this problem, from Gentzen’s mixThe mix rule is a generalisation of the usual cut that combines it with contractions on the cut formula. Specifically, it may infer a sequent Γ → Δ from sequents Γ → Δ,A,…,A and A,…,A,Γ → Δ. rule to invoking yet another induction on the ‘contraction tree’ structure, i.e. the number of direct ancestorsA direct ancestor of a formula C, morally speaking, is any higher occurrence of C that 'comes from' the indicated one, bottom-up. This can, of course, be made formal, but the full definition is much more tedious than the idea behind it..

Invertibility for propositional logic

However, one can also sometimes replace the need for (2) above by globally modifyingTechnically, these are also proved by an induction on height, but such lemmas serve a different purpose than in usual cut-elimination. subproofs. One successful such method is known as invertibilityAn inference rule is invertible if the validity of its conclusion implies the validity of its premisses. (It is the converse of soundness).. For classical propositional logic, this allows us to sidestep the contraction issue altogether, e.g. with the following reduction:

Here, the derivations , and are obtained from , and respectively without increasingTechnically, it matters precisely which set of rules we fix, but in any case there is a natural notion of size that does not increase. proof size. For instance, to obtain we replace every direct ancestor of the indicated in by . The critical cases are the originsAn origin of A is a direct ancestor that is principal, i.e. it concludes an inference step that decomposes it, bottom-up. of , which are , weakening or initial steps, and these may be duly repaired in situ. In this way, we elegantly achieve exponential-time cut-elimination, by an induction on the sum of cut-degrees in a proof, rather than the multiset as in (1) above. In contrast, Gentzen’s procedure is non-elementaryThe complexity of Gentzen's procedure is, by the 'Curry-Howard' correspondence, correlated to the normalisation of simply typed lambda terms, which includes arbitrary towers of 2s..

A problem with the quantifiers

However, the tradeoff is that the invertibility technique does not scale well at all. Even first-order classical logic (FOL) proves problematic, since we cannot in general ‘invert’ the -r and -l rules, though some variants of the techniqe exist. For instance, if there are only -cutsThese are cuts on formulas of the form ∃x∃y…∃z A, where A is quantifier-free. then we may appeal to Herbrand’s theorem to apply the invertibility technique:

Here the terms exist by Herbrand’s thoerem and the derivations are obtained by invertibility of on the LHS. Indeed, more general forms of Herbrand’s theorem can give more general versions of cut-elimination, though the statements of the invertibility lemmas does get increasingly complex. See, for instance [1] for a formal (and correct) account of Herbrand’s theorem in its full generality.

While historically it is not a problem to rely on Herbrand’s theorem to prove cut-elimination, the former predatingHerbrand published his result in 1930 and Gentzen his in 1934. Of course, they may have obtained the results beforehand, but we can at least suppose that Herbrand's result is independent. the latter, it does not seem like a satisfactory solution. Beyond the complications of scaling to more quantifier-ly complex formulas, the size of Herbrand disjuncts is well-known to be non-recursive, even for formulas (see, e.g., [2]). On the other hand, Gentzen’s cut-elimination for FOL is superexponentialI don't like this terminology since it does not seem precise. 'Super' just means above, but does not quantify how much above. I prefer 'tetration', which is also used but much less common in proof theory circles., so this time the invertibility technique is actually worse in terms of complexity!

Due to these complications, it is more common to combine the invertibility reduction for propositional cuts with a more classical treatment of quantifier cuts (via mix or contraction trees etc.). For instance, this is essentially how the cut-elimination proof in the Handbook of Proof Theory proceeds [3].

Beyond classical logic…

The problems for the invertibility technique become even worse for other logics, due to the general lack of invertible rules. In focussing parlance, this is due to the fact that logics generally comprise of negative connectives (whose right introduction rules are invertible) and positive connectives (whose left introduction rules are invertible). Classical logic has the property that its propositional connectives can both be negatively polarised. This is obviously not the case for intuitionistic logic (implication is necessarily positive negative) and, more generally, linear logic (each connective has exactly one polarity) [4]. In these cases, Gentzen’s procedure remains the only general one, as far as I know. However, in some follow up posts, I want to examine some of the work done on alternative cut-elimination procedures for non-classical logics, with the case of intuitionistic logic being of particular interest.

References

@misc{McK10:herbrand-sequent,
title={A sequent calculus demonstration of {H}erbrand's theorem},
author={Richard McKinley},
year={2010},
eprint={1007.3414},
archivePrefix={arXiv},
note={\url{https://arxiv.org/abs/1007.3414}},
primaryClass={math.LO}
}

[2] S. R. Buss, “On Herbrand’s Theorem,” in Logical and Computational Complexity. Selected Papers. Logic and Computational Complexity, International Workshop LCC ’94, Indianapolis, Indiana, USA, 13-16 October 1994, 1994, p. 195–209.
[Bibtex]

@inproceedings{Bus94:on-herbrand,
author = {Samuel R. Buss},
editor = {Daniel Leivant},
title = {On Herbrand's Theorem},
booktitle = {Logical and Computational Complexity. Selected Papers. Logic and Computational
Complexity, International Workshop {LCC} '94, Indianapolis, Indiana,
USA, 13-16 October 1994},
series = {Lecture Notes in Computer Science},
volume = {960},
pages = {195--209},
publisher = {Springer},
year = {1994},
url = {https://doi.org/10.1007/3-540-60178-3\_85},
doi = {10.1007/3-540-60178-3\_85},
timestamp = {Tue, 14 May 2019 10:00:54 +0200},
biburl = {https://dblp.org/rec/conf/lcc/Buss94.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}

[3] S. R. Buss, “Chapter I – An Introduction to Proof Theory,” in Handbook of Proof Theory, S. R. Buss, Ed., Elsevier, 1998, vol. 137, pp. 1-78.
[Bibtex]

@incollection{Bus98:intro-to-pt:handbook,
title = "Chapter I - An Introduction to Proof Theory",
editor = "Samuel R. Buss",
series = "Studies in Logic and the Foundations of Mathematics",
publisher = "Elsevier",
volume = "137",
pages = "1 - 78",
year = "1998",
booktitle = "Handbook of Proof Theory",
issn = "0049-237X",
doi = "https://doi.org/10.1016/S0049-237X(98)80016-5",
url = "http://www.sciencedirect.com/science/article/pii/S0049237X98800165",
author = "Samuel R. Buss"
}

[4] J. Andreoli, “Logic Programming with Focusing Proofs in Linear Logic,” Journal of Logic and Computation, vol. 2, iss. 3, p. 297–347, 1992.
[Bibtex]

@article{And92:focussing,
author = {Jean-Marc Andreoli},
title = {Logic Programming with Focusing Proofs in Linear Logic},
journal = {Journal of {L}ogic and {C}omputation},
volume = {2},
number = {3},
pages = {297--347},
year = {1992},
url = {https://doi.org/10.1093/logcom/2.3.297},
doi = {10.1093/logcom/2.3.297},
}