Skip to content

The Proof Theory Blog

PA ⊢ ∀x ∃y A(x,y) ⇒ ∃t . T ⊢ ∀x A(x,t(x))

Menu
  • Home
  • About
  • Contribute
  • Resources
Menu

‘Simple’ proofs of cut-elimination: classical logic

Posted on May 7, 2020October 20, 2022 by Anupam Das

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 A with two cuts on A! 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 P^{-1}_A, P^{-1}_B and Q^{-1} are obtained from P, P and Q 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 P^{-1}_A we replace every direct ancestor of the indicated A\wedge B in P by A. 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 A\wedge B, which are \wedge\text - r, 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 \exists-r and \forall-l rules, though some variants of the techniqe exist. For instance, if there are only \exists_1-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 t_1,\dots,t_n exist by Herbrand’s thoerem and the derivations Q^{-1}_i are obtained by invertibility of \exists 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.

Almost all proofs of Herbrand’s theorem are incorrect.Matthias Baaz at Proofs, Computation, Complexity 2019.

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 \exists_1 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 \vee, \wedge 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

[1] R. McKinley, A sequent calculus demonstration of Herbrand’s theorem, 2010.
[Bibtex]
@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] [doi] 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] [doi] 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] [doi] 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},
}

8 thoughts on “‘Simple’ proofs of cut-elimination: classical logic”

  1. Pingback: Contraction on a leash - The Proof Theory Blog
  2. Sam Sanders says:
    May 28, 2020 at 9:16 pm

    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.

    Reply
    1. Anupam Das says:
      June 1, 2020 at 11:24 am

      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.

      Reply
    2. Anton Freund says:
      June 1, 2020 at 2:57 pm

      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).

      Reply
      1. Anupam Das says:
        June 3, 2020 at 9:47 am

        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.

        Reply
  3. Pingback: From cut elimination to reverse mathematics - The Proof Theory Blog
  4. Nguyễn Lê Thành Dũng says:
    June 3, 2020 at 5:16 pm

    “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.

    Reply
    1. Anupam Das says:
      June 5, 2020 at 12:59 pm

      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.

      Reply

Leave a Reply Cancel reply

Your email address will not be published. Required fields are marked *

Meta

  • Register
  • Log in
  • Entries RSS
  • Privacy Policy

Search

© 2023 The Proof Theory Blog | Powered by Minimalist Blog WordPress Theme
The Proof Theory Blog uses cookies, but you can opt-out if you wish. For further information see our privacy policy. Cookie settingsAccept
Privacy & Cookies Policy

Privacy Overview

This website uses cookies to improve your experience while you navigate through the website. Out of these cookies, the cookies that are categorized as necessary are stored on your browser as they are essential for the working of basic functionalities of the website. We also use third-party cookies that help us analyze and understand how you use this website. These cookies will be stored in your browser only with your consent. You also have the option to opt-out of these cookies. But opting out of some of these cookies may have an effect on your browsing experience.
Necessary
Always Enabled
Necessary cookies are absolutely essential for the website to function properly. This category only includes cookies that ensures basic functionalities and security features of the website. These cookies do not store any personal information.
Non-necessary
Any cookies that may not be particularly necessary for the website to function and is used specifically to collect user personal data via analytics, ads, other embedded contents are termed as non-necessary cookies. It is mandatory to procure user consent prior to running these cookies on your website.
SAVE & ACCEPT