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: .
Most cut-elimination proofs do something like this:
- Main induction on the multiset of in a proof.
- A sub-induction on the 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 us eliminate the lower one. There are various (well-known) solutions to this problem, from Gentzen’s rule to invoking yet another induction on the ‘contraction tree’ structure, i.e. the number of .
Invertibility for propositional logic
However, one can also sometimes replace the need for (2) above by subproofs. One successful such method is known as . 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 proof size. For instance, to obtain
we replace every direct ancestor of the indicated
in
by
. The critical cases are the 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 .
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 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 formulas (see, e.g., [2]). On the other hand, Gentzen’s cut-elimination for FOL is , 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}
}
![[doi]](https://prooftheory.blog/wp-content/plugins/papercite/img/external.png)
[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}
}
![[doi]](https://prooftheory.blog/wp-content/plugins/papercite/img/external.png)
[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"
}
![[doi]](https://prooftheory.blog/wp-content/plugins/papercite/img/external.png)
[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},
}
So my first thought was the following: if something cannot be done cleanly or simply, there is usual some kind of Reverse Mathematics result lurking around the corner. It could well be that the RM result is hideous, but it may yet explain what is going on.
I think some sort of setting between usual RM and ‘bounded reverse mathematics’ would be in order. The former deals with functions that are primitive recursive upwards, whereas the latter deals with functions of polynomial growth rate. Theories for elementary functions and tetration would be the right ones, due to the known complexities of cut-elimination.
That said, I think the ‘simplicity’ I am looking for here is more about exposition, rather than computability/complexity theoretic.
I guess this is implicit in Anupam’s reply, but just to state it explicitly: cut elimination leads to a superexponential increase in proof height. I am not sure whether this computational explanation becomes more transparent if we phrase it in terms of (some version of) reverse mathematics.
On the other hand, there are several reverse mathematics results about cut elimination in infinitary proof systems. I am currently writing a post on reverse mathematics and cut elimination for omega-proofs. There is even a result that cut elimination for certain functorial systems of infinite proofs implies \Pi^1_1-comprehension (see Theorem 11.6.4 in the unpublished second volume of Girard’s book on proof theory, which is available on his website: https://girard.perso.math.cnrs.fr/Archives4.html).
Thanks for the pointers Anton, I’m looking forward to your article. One clarification: note that in propositional logic cut-elimination is not superexponential, – for instance one can simply throw away the starting proof and do proof search. In fact, now that I think about it, this is one reason why the RM setting is not appropriate here: I am only considering ‘local’ cut-elimination procedures. E.g., as far as I know, there is no known exponential-time cut-elimination procedure for intuitionistic propositional logic, despite it having exponential size cut-free proofs.
“implication is necessarily positive” -> I assume you mean negative?
Maybe a better example to illustrate your point would be the intuitionistic disjunction which is positive.
Of course! Implication is negative, sorry, corrected now. You are also right about disjunction being necessarily positive, but I like the example of implication since it seems much more profound. It is also the issue for minimal logic and, for proof search, it is also combined with the termination-issue induced by contraction.