‘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: contraction.

Most cut-elimination proofs do something like this:

1. Main induction on the multiset of cut degrees in a proof.
2. A sub-induction on the height 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 help us eliminate the lower one. There are various (well-known) solutions to this problem, from Gentzen’s mix rule to invoking yet another induction on the ‘contraction tree’ structure, i.e. the number of direct ancestors.

Invertibility for propositional logic

However, one can also sometimes replace the need for (2) above by globally modifying subproofs. One successful such method is known as invertibility. 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 increasing proof size. For instance, to obtain we replace every direct ancestor of the indicated in by . The critical cases are the origins 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-elementary.

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 -cuts 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 predating 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 superexponential, 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},
}