Contraction on a leash - The Proof Theory Blog

The contraction rule (c) (discussed also in this blog post) is a familiar obstacle to anyone aiming to use the sequent calculus to establish a property of the underlying logic.

$\inferrule*[right=(c)]{X,A,A\Rightarrow B}{X,A\Rightarrow B}$

Simply stated the issue is that the premise of the rule is more complicated (contains more content) than its conclusion, and hence proof search (the repeated application of rules upwards from conclusion to premises) does not terminate.

In this post, I will discuss Curry’s lemma which captures how the contraction rule can be tamed by internalising a limited amount of contraction into the other sequent calculus rules. If you want to have a concrete calculus in mind, take the (cut free) intuitionistic calculus $\text{LJ}$ or the commutative Full Lambek calculus with contraction $\text{FL}_{ec}$ (see here for the rules). A sequent has the form $X \Rightarrow A$ where the antecedent $X$ is a multiset of formulas.

In fact, when all the rules are context-sharing (additive), it is possible that contraction is tameable in the strongest possible way, by deleting the contraction rule and proving that the contraction rule is height-preserving admissible. This means that given a derivation of $X,A,A\Rightarrow B$ there is a derivation of $X,A\Rightarrow B$ of no greater height. The argument is an induction on the height of a derivation of $X,A,A\Rightarrow B$ . From a procedural viewpoint the contraction rule is repeatedly permuted with the rule above it until it reaches the leaves of the derivation tree where it is finally eliminated.

Unfortunately such a permutation is not possible when (c) is below a context-splitting (multiplicative) rule. For example, consider the following instance of the ( $\otimes$ R) rule where the antecedent context $X,Y,A,A$ is split into $X,A$ in the left premise and $Y,A$ in the right premise.

$\mprset{fraction={\cdot\cdots\cdot}}\inferrule*[left=(c)]{\mprset{fraction={---}} \inferrule*[left=($\otimes$R)]{X,A\Rightarrow C\\Y,A\Rightarrow D}{X,Y,A,A\Rightarrow C\otimes D}}{X,Y,A\Rightarrow C\otimes D}$

The issue is that the contraction rule cannot be applied in either premise of ( $\otimes$ R) because at least two copies of $A$ in the antecedent are required for this.

One way of getting around this is to internalise the contraction rule into every other rule in the sequent calculus. Let $s \rightsquigarrow^{c} s_{1}$ denote that sequent $s_{1}$ can obtained from sequent s by applying some number of contraction rules. Now let us replace the rule ( $\otimes$ R) with the following.

$\inferrule*[right={$X,Y\Rightarrow C\otimes D \rightsquigarrow^{c} Z\Rightarrow C\otimes D$}]{X\Rightarrow C\\Y\Rightarrow D}{Z\Rightarrow C\otimes D}$

Of course, this is nothing more than a change of notation. In particular, for a given $Z \Rightarrow C\otimes D$ there are in general an unlimited number of premises $X\Rightarrow C$ and and $Y\Rightarrow D$ such that $X,Y \Rightarrow C\otimes D$ contracts to $Z\Rightarrow C\otimes D$ (and this was the issue in the first place).

What we want to do therefore is to restrict the number of contraction rules that can be performed i.e. replacing $\rightsquigarrow^{c}$ with $\rightsquigarrow^{c}_{N}$ for some fixed $N$ , where $X \Rightarrow A \rightsquigarrow^{c}_{N} Y \Rightarrow A$ means that $Y\Rightarrow A$ is obtained from $X\Rightarrow A$ by applying some number of contraction rules such that a formula in $X$ occurs at most $N$ fewer times in $Y$ . For example, $p^{3},q^{2}\Rightarrow r \rightsquigarrow^{c}_{2} p^{2},q\Rightarrow r$ and $p^{3},q^{2}\Rightarrow r \rightsquigarrow^{c}_{2} p,q\Rightarrow r$ (but not $p^{3},q^{2}\Rightarrow r \rightsquigarrow^{c}_{2} p\Rightarrow r$ since the contraction rule cannot make the $q$ disappear).

So what value of $N$ should we use?

Consider the conclusion $X,Y \Rightarrow C\otimes D$ of an instance of ( $\otimes$ R). If there were three occurrences of $A$ in $X,Y$ then there would be two occurrences in $X$ (say): apply (c) on the left premise (this is the permutation) to get $X\setminus \{A\}$ and then by ( $\otimes$ R) we get $X,Y\setminus\{A\} \Rightarrow C\otimes D$ . It follows that the only case that requires internalised contraction is when there are just two occurrences of $A$ in $X,Y$ . Since the lowest value that can be achieved via contraction is a single occurrence of $A$ it follows that $\rightsquigarrow^{c}_{1}$ suffices (internalising more contraction would obviously be okay as well).

$\inferrule*[right={$X,Y\Rightarrow C\otimes D \rightsquigarrow^{c}_{1} Z\Rightarrow C\otimes D$}]{X\Rightarrow C\\Y\Rightarrow D}{Z\Rightarrow C\otimes D}$

Let us consider how this plays out on another rule.

$\inferrule*[left=($\rightarrow$)]{X\Rightarrow C\\D,Y\Rightarrow B}{X,Y,C\rightarrow D\Rightarrow B}$

If there were four or more occurrences of a formula in $X,Y,C\rightarrow D$ then we could permute (c) into the premises and then apply $(\rightarrow L)$ , to obtain the situation where three occurrences occur. However if only three occurrences of $C\rightarrow D$ occur in $X,Y,C\rightarrow D$ , then it is possible that both $X$ and $Y$ contain a single copy of $C\rightarrow D$ so we cannot permute. We need to internalise some contraction to handle this case: since the lowest that we need to go is a single occurrence of a formula, a reduction by at most two formulas i.e. $\rightsquigarrow^{c}_{2}$ suffices. Therefore we arrive at the following rule.

$\inferrule*[left=($\rightarrow$), right={$X,Y,C\rightarrow D \Rightarrow B \rightsquigarrow^{c}_{2} Z \Rightarrow B$}]{X\Rightarrow C\\D,Y\Rightarrow B}{Z\Rightarrow B}$

By choosing an amount of internal contraction that is enough for every rule in the calculus (for a rule schema whose conclusion antecedent is a list of length $k$ it suffices to use $\rightsquigarrow^{c}_{k-1}$ ) we obtain

Curry’s lemma. There is an $N>0$ such that the sequent calculus obtained by replacing the conclusion $s$ of each rule schema with $s'$ with the side condition $s\rightsquigarrow^{c}_{N} s'$ has height-preserving contraction.

The attribution is due to Theorem 3 in Curry’s book [1] where a proof of height-preserving admissibility of contraction is given for propositional intuitionistic and classical sequent calculi by amending the rules so that the conclusion of each internalised a fixed amount of contraction. If too much contraction was applied, the situation could be rectified using the weakening rule. Since a substructural logic might lack weakening, it is necessary to internalise a variable amount of contraction (the “at most” in the definition of $\rightsquigarrow^{c}_{N}$ ).

Kripke made crucial use of this lemma in his proof [2] of the decidability of implicational fragment of $\text{FL}_{ec}$ (the argument extends easily to the full calculus). Kripke’s argument requires the use of minimal derivations i.e. derivations whose every subderivation has minimum height. In such a derivation, no sequent on a branch is contractible to an earlier sequent on that branch as Curry’s lemma would imply then the violation of minimality. This meant that non-decreasing sequences of sequents could be disregarded from proof search. There is another crucial ingredient to his argument establishing the finiteness of proof search that I do not discuss here: an infinite sequence of sequents built from a fixed finite set of formulas such that no element is contractible to any other element does not exist (Kripke’s lemma). See Restall [3] for an exposition.

In a future post I will discuss how Curry’s lemma can be extended to hypersequent calculi to establish height-preserving admissibility of internal contraction (c) and external contraction (EC).

References

[1] H. B. Curry, A Theory of Formal Deducibility, Notre Dame, Ind.: University of Notre Dame, 1950.
[Bibtex]

@book{Cur50,
Author = {Curry, Haskell B.},
Pages = {ix+126},
Publisher = {Notre Dame, Ind.: University of Notre Dame},
Title = {A Theory of Formal Deducibility},
Year = {1950}}

[2] S. Kripke, “The problem of entailment (abstract),” J. of Symbolic Logic, vol. 24, p. 324, 1959.
[Bibtex]

@article{Kri59,
Author = {S. Kripke},
Journal = {J. of Symbolic Logic},
Pages = {324},
Title = {The problem of entailment (abstract)},
Volume = {24},
Year = {1959}}

[3] G. Restall, An Introduction to Substructural Logics, London: Routledge, 1999.
[Bibtex]

@book{Res99,
Address = {London},
Author = {G. Restall},
Publisher = {Routledge},
Title = {An Introduction to Substructural Logics},
Topic = {substructural-logics;},
Year = {1999}}

Thank you very much for the two interesting posts on the role of contraction in cut elimination! I wanted to share a completely different experience from my own research (ordinal analysis of relatively strong theories), in which I use cut elimination a lot but do not need to deal with contraction at all. The reason is that I usually consider sequents as finite sets (rather than multisets or sequences) of formulas, so that there is simply no place for structural rules. Of course, this is not appropriate for all applications: When you are interested in computational complexity, then it may be crucial to keep the contraction rule and analyse it in detail. On the other hand, there is no need to worry about contraction when you use cut elimination in an ordinal analysis of, say, Peano arithetic. The general point that I want to make is:

* Cut elimination can be very simple and transparent! *

In the following, I will mention some simplifications that justify this claim. All these simplifications are applied in the paper “Notation systems for infinitary derivations” by Wilfried Buchholz (Arch. Math. Logic 30 (1991), no. 5-6, 277–296). The sequent calculus in this paper does only have four rules (plus a “trivial” repetition rule, see Definition 2.1), and there is an extremely rigorous treatment of cut elimination in about two pages (admittedly with very condensed notation). Let me now state the promised simplifications:

(1) If your application does not depend on a fine analysis of structural rules, consider sequents as sets (rather than multisets or sequences) of formulas, as mentioned above.
(2) If your application is concerned with classical logic, use Tait-style sequent calculus. In this variant, the negation symbol is only allowed in front of atomic formulas, and complex formulas are negated with the help of de Morgan’s rules. As a consequence, there is no need to distinguish between antecedent and consequent: a sequent will simply be a single set of formulas. The advantage is that your sequent calculus will have far fewer rules, so that there are no lengthy case distinctions.
(3) If you consider infinite proof trees with the omega rule, there is no need for free variables (since a universal formula is derived from its infinitely many closed instances). Hence it is not necessary to worry about variable conditions or substitution. Also, one can then consider universal (existential) formulas as infinite conjunctions (disjunctions), which will further reduce the number of rules.

3 thoughts on “Contraction on a leash”

Anton Freund says:

May 31, 2020 at 8:52 am

Thank you very much for the two interesting posts on the role of contraction in cut elimination! I wanted to share a completely different experience from my own research (ordinal analysis of relatively strong theories), in which I use cut elimination a lot but do not need to deal with contraction at all. The reason is that I usually consider sequents as finite sets (rather than multisets or sequences) of formulas, so that there is simply no place for structural rules. Of course, this is not appropriate for all applications: When you are interested in computational complexity, then it may be crucial to keep the contraction rule and analyse it in detail. On the other hand, there is no need to worry about contraction when you use cut elimination in an ordinal analysis of, say, Peano arithetic. The general point that I want to make is:

* Cut elimination can be very simple and transparent! *

In the following, I will mention some simplifications that justify this claim. All these simplifications are applied in the paper “Notation systems for infinitary derivations” by Wilfried Buchholz (Arch. Math. Logic 30 (1991), no. 5-6, 277–296). The sequent calculus in this paper does only have four rules (plus a “trivial” repetition rule, see Definition 2.1), and there is an extremely rigorous treatment of cut elimination in about two pages (admittedly with very condensed notation). Let me now state the promised simplifications:

(1) If your application does not depend on a fine analysis of structural rules, consider sequents as sets (rather than multisets or sequences) of formulas, as mentioned above.
(2) If your application is concerned with classical logic, use Tait-style sequent calculus. In this variant, the negation symbol is only allowed in front of atomic formulas, and complex formulas are negated with the help of de Morgan’s rules. As a consequence, there is no need to distinguish between antecedent and consequent: a sequent will simply be a single set of formulas. The advantage is that your sequent calculus will have far fewer rules, so that there are no lengthy case distinctions.
(3) If you consider infinite proof trees with the omega rule, there is no need for free variables (since a universal formula is derived from its infinitely many closed instances). Hence it is not necessary to worry about variable conditions or substitution. Also, one can then consider universal (existential) formulas as infinite conjunctions (disjunctions), which will further reduce the number of rules.

1. Anupam Das says:
  
  June 3, 2020 at 10:12 am
  
  I think Rev answered your points well in his response but just to add my take: I do agree that, for classical logic, there are very elegant and succinct ways to argue about cut-elimination. However, many situations in ‘structural’ proof theory fall out of the scope of (1), since they do depend on structural rules, (2), since they might not admit a De Morgan duality, and (3) since we often deal in a purely propositional setting.
  
Revantha Ramanayake says:

June 2, 2020 at 11:12 am

l agree with the spirit of using the simplest formalism that works. In particular, where viable, sets instead of multisets, and one-sided sequents do simplify the cut-elimination argument.

Thus, although Curry proved the lemma now bearing his name in the setting of intuitionistic logic, its real value is in the context of substructural logics lacking weakening. In this context, one needs to keep track of the multiplicity of formulas and hence it is not possible to use sequents built from sets.

Note also that the purpose of internalising contraction in the way described in the article is to eliminate the unrestricted use of the contraction rule (rather than to aid the cut-elimination argument). This restricts the proof search and that is helpful for establishing properties of the underlying logic (for example, its decidability).

References

3 thoughts on “Contraction on a leash”

Leave a Reply Cancel reply