‘Simple’ proofs of cut-elimination II: intuitionistic logic

Cut-elimination for intuitionistic logic has particular significance to proof theorists due to the constructive nature of the logic. Cut-free proofs give rise to significant computational information, including interpolants of implications and, in the case of predicate logic, witnesses of existentials. Moreover, the process of cut-elimination can itself be viewed as a computational process thanks to the Curry-Howard correspondence. This post is a continuation of this one, investigating ‘simpler’ proofs of cut-elimination in special cases. One particular criterion for simplicity here is computational complexity, but I am also interested by expositional simplicity.

Hauptsatz: cut-elimination or cut-admissibility?

As for classical logic before, we should distinguish two problems, that could equally interpret Gentzen’s ‘Hauptsatz’The following terminological distinction of 'cut-admissibility' and 'cut-elimination' seems to be common in many proof theory communities, but it should not be taken as standard.:

1. Every theorem has a cut-free proof (cut-admissibility).
2. Every proof can be ‘locally’ transformed into one of the same theorem without cuts (cut-elimination).

Somewhat ironically, the usual statements (e.g. the one on Wikipedia) of the Hauptsatz correspond to cut-admissibility, while the usual understanding of the Hauptsatz among (at least structural) proof theorists is that of cut-elimination. In this post I am more interested in cut-elimination, but let us at least mention some basic properties of cut-free LJ proofs for intuitionistic propositional logic (IPL).

Proposition 1 (Folklore). For any theorem of IPL, we can compute a cut-free LJ proof of A in exponential time and polynomial spaceWe may admit exponential growth rate functions in polynomial space by adpoting a machine model with polynomially bounded work tape and write-only output type. in .

This result is widely known, and appears in several guises in the literature (see [1] for a recent survey of related results). It is a special case of the fact that any ‘well-behaved’ analytic sequent system admitting structural rules contraction and weakening has the above property, thanks to a simple loop checking argument.

Many important consequences of the Hauptsatz in fact require only this weaker statement of cut-admissibility. For example:

Theorem 2 (Craig interpolation). If IPL , where all propositional variables are indicated and disjoint, then there is a formula , with all propositional variables indicated, (the interpolant), such that IPL and IPL .

However, Proposition 1 above is not really a ‘cut-elimination’ theorem per se, since it merely asserts cut-free completeness of LJ. In particular, it does not allow us to distinguish proofs by their normal forms under some reduction process.

Curry-Howard: cut-elimination vs normalisation

For many structural proof theorists, cut-elimination for IPL is identified with the normalisation of simply typedStrictly speaking, this is only for the implication-only fragment. Conjunction is easily admitted by product types and pairs, while disjunction is admitted by sum types and a form of case distinction. -terms. The latter is known to have a non-elementary lower bound since we can type functions of arbitrary elementary growth rate. In fact we have a much stronger result from [2]:

Theorem 3 (Statman ’79). Deciding whether two simply typed -terms reduce to the same normal form is not elementary recursive.

Via the Curry-Howard correspondence, we may view this result as a lower bound on deciding proof equivalence for intuitionistic logic, but I will leave the discussion of this to another day.

However, Statman’s result does not imply any lower bounds on the complexity of cut-elimination for LJ, since normalisation of -terms constitutes just one particular strategy for cut-elimination. Note in particular, that both Proposition 1 and Theorem 3 are perfectly consistent with each other.

On the other hand, more efficient (yet local) cut-elimination strategies may induce alternative notions of computation-as-normalisation, which could lead to other interesting term calculi and type systems for the Curry-Howard-oriented proof theorist.

Semi-invertibility and elementary cut-elimination

The fact that elementary cut-elimination is possible in LJ seems to be folklore (though I will cite some particular results in a moment). All arguments I am aware of use a form of ‘semi-invertibility’. Recall from last time that invertibility of rules in LK allowed us to normalise proofs in exponential time. For intuitionistic logic, the same trick works for cuts on conjunctions , but we have only invertibility on one side for disjunction and implication . As I mentioned last time, this sort of one-sided invertibility is well-understood under the guise of focussing, where connectives of a logic are organised based on whether their introduction rules are invertible on the left (positive) or invertible or the right (negative) (see [3]).

Semi-invertibility can still be used to drive a more efficient cut-elimination argument, e.g. via the following reduction:

Here is obtained from by replacing every immediate ancestor of the indicated by , and adding to the antecedent of all affected sequents. Any affected -r steps may be safely deleted.

However note that the –-cut in the RHS above is of the same logical complexity as the cut in the LHS, in contrast with ‘full inversion’ reductions for propositional LK. Termination is still guaranteed by the fact that the –-cut roots a smaller subproof but, along with the necessity of commutative casesA commutative case (as opposed to a 'key' case) is a cut-reduction that permutes the cut over a step that is principal on a side formula, not the cut-formula., there are many more technicalities involved to organise the reductions into a cut-elimination procedure of demonstrably elementary complexity.

The first result I am aware of that established elementary bounds on the complexity of cut-elimination for IPL is Hudelmaier’s work [4]. Inspired by the proof-search-oriented calculus G4ip for IPL, Hudelmaier devised inversion rules by employing a modest form of deep inference, inspecting the antecedent of implications. G4ip is significant enough to merit a post of its own, so I will avoid discussing it here and refer only to [1] for further details. More pertinent is (a simplified statement of) Hudelmaier’s main result:

Proposition 4 (Hudelmaier ’92). Any proof of LJ may be transformed by a sequence of local reductions into a cut-free one of the same conclusion of sizeIt should be mentioned that Hudelmaier argues with 'length' than size, by which he means the length of the longest branch of a proof. He obtains a triple-exponential bound on this parameter, which implies the quadruple-exponential bound so stated, but I have not attempted to optimise this. .

Recently Baaz and Fermüller obtained elementary bounds on cut-elimination for some nontrivial fragments of predicate LJ [5]. Along the way, they formalised a semi-invertibility argument for cut-elimination in propositional LJ, improving Hudelmaier’s result:

Proposition 5 (Baaz & Fermüller ’15). Any proof of LJ may be transformed by a sequence of local reductions into a cut-free one of the same conclusion of sizeAgain, Baaz and Fermüller work in terms of 'height', and state a double-exponential bound in this parameter .

As far as I know, this triple-exponential bound is the best known on cut-elimination for LJ. However, recalling Proposition 1, note that we now have a curious (and to me surprising) gap between the bounds on the size of cut-free proofs and on the complexity of cut-elimination.

Closing the gap?

It astounds me that Proposition 1 is so easy to establish, while Propositions 4 and 5 above seem non-optimal yet already require much more work. In classical logic, as mentioned in the previous post, exponential-time cut-elimination is readily established, thanks to a full invertibility argument. It is not clear to me whether exponential-time cut-elimination requires, in some formal sense, invertible rules for all connectives, or if there is another way. Put more succinctly:

Question. Is cut-elimination for LJ possible in exponential time?

In fact, as far as I know, there is not even a double-exponential-time procedure known! It would not surprise me if someone has worked this out on the back of a cigarette packet, or if there is some hidden literature reference to this effect. If anyone knows anything more about this, please do get in touch or leave a comment below!

References

[1] R. Dyckhoff, “Intuitionistic Decision Procedures Since Gentzen,” in Advances in Proof Theory, R. Kahle, T. Strahm, and T. Studer, Eds., Cham: Springer International Publishing, 2016, p. 245–267.
[Bibtex]

@Inbook{Dyc16:ipl-decision-procedures,
author="Dyckhoff, Roy",
editor="Kahle, Reinhard
and Strahm, Thomas
and Studer, Thomas",
title="Intuitionistic Decision Procedures Since Gentzen",
bookTitle="Advances in Proof Theory",
year="2016",
publisher="Springer International Publishing",
address="Cham",
pages="245--267",
isbn="978-3-319-29198-7",
doi="10.1007/978-3-319-29198-7_6",
url="https://doi.org/10.1007/978-3-319-29198-7_6"
}

[2] R. Statman, “The Typed -Calculus is not Elementary Recursive,” Theor. Comput. Sci., vol. 9, p. 73–81, 1979.
[Bibtex]

@article{Sta79:stlc-non-elementary,
author = {Richard Statman},
title = {The Typed -Calculus is not Elementary Recursive},
journal = {Theor. Comput. Sci.},
volume = {9},
pages = {73--81},
year = {1979},
url = {https://doi.org/10.1016/0304-3975(79)90007-0},
doi = {10.1016/0304-3975(79)90007-0},
}

[3] J. Andreoli, “Logic Programming with Focusing Proofs in Linear Logic,” J. Log. Comput., 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 = {J. Log. Comput.},
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},
}

[4] J. Hudelmaier, “Bounds for cut elimination in intuitionistic propositional logic,” Arch. Math. Log., vol. 31, iss. 5, p. 331–353, 1992.
[Bibtex]

@article{Hud92:bounds-cut-elim-lj,
author = {J{\"{o}}rg Hudelmaier},
title = {Bounds for cut elimination in intuitionistic propositional logic},
journal = {Arch. Math. Log.},
volume = {31},
number = {5},
pages = {331--353},
year = {1992},
url = {https://doi.org/10.1007/BF01627506},
doi = {10.1007/BF01627506},
}

[5] M. Baaz and C. G. Fermüller, “Elementary Elimination of Prenex Cuts in Disjunction-free Intuitionistic Logic,” in 24th EACSL Annual Conference on Computer Science Logic (CSL 2015), Dagstuhl, Germany, 2015, p. 94–109.
[Bibtex]

@inproceedings{BaaFer15:elementary-cut-elim-lj,
author =  {Matthias Baaz and Christian G. Ferm{\"u}ller},
title =  {{Elementary Elimination of Prenex Cuts in Disjunction-free Intuitionistic Logic}},
booktitle =  {24th EACSL Annual Conference on Computer Science Logic (CSL 2015)},
pages =  {94--109},
series =  {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN =  {978-3-939897-90-3},
ISSN =  {1868-8969},
year =  {2015},
volume =  {41},
editor =  {Stephan Kreutzer},
publisher =  {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
address =  {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2015/5409},
URN = {urn:nbn:de:0030-drops-54097},
doi = {10.4230/LIPIcs.CSL.2015.94},
annote =  {Keywords: Cut-elimination, sequent calculus, intuitionistic logic}
}