Weakening

From Girard Reading Group

Weakening is the principle that if something holds, it doesn't stop holding when we add extra stuff. Formally, weakening tells us that if a sequent Γ ⊢ Δ is valid, so is Γ',Γ ⊢ Δ,Δ' for any Γ' and Δ'. In Gentzen's LK (the original sequent calculus for classical logic), weakening is reflected as a pair of rules

       Γ ⊢ Δ                   Γ ⊢ Δ
   ━━━━━━━━ (LW)      ━━━━━━━ (RW)
      Γ',Γ ⊢ Δ                Γ ⊢ Δ,Δ'

which weaken the sequent on the left and right. In systems such as Kleene's G3, weakening is not a rule but still admissible, built into the other rules. In intuitionistic sequent calculus, the left-weakening principle is the same but right-weakening is restricted: since the right side of a sequent can contain at most one formula, at most we can weaken Γ ⊢ ∙ to Γ ⊢ C.

The presence of arbitrary left- and right-weakening in classical sequent calculus ends up making its equational theory degenerate. Suppose we have two different proofs D1 and D2 of the sequent Γ ⊢ Δ. We build a new proof D3 of Γ ⊢ Δ as follows (this derivation is known as "Lafont's critical pair"):

        D1                   D2    
      Γ ⊢ Δ                Γ ⊢ Δ
   ━━━━━━━ (RW)     ━━━━━━━ (LW)
     Γ ⊢ Δ,C              C,Γ ⊢ Δ
 ━━━━━━━━━━━━━━━━━━━━━━━━ (cut)
                  Γ ⊢ Δ

where in the last line we applied the cut principle. Now, we want proof equality to respect cut-elimination. But to eliminate the cut in D3, we have two perfectly respectable options: reducing to either D1 or D2. Since D3 reduces to either D1 or D2 by cut-elimination, we have both D3 = D1 and D3 = D2, and finally D1 = D2 by closing under the equivalence relation.

Hence in classical sequent calculus, all proofs of a particular sequent are equal! This is disturbing from a constructive point of view, since it seems to imply that classical sequent calculus proofs have no computational content. However, there have been various proposed solutions. One way of viewing Girard's polarity is that it simply imposes a deterministic protocol for cut-elimination, based on the polarity of the cut formula. In the critical pair above, if C is positive then we always choose D1, and if it is negative we always choose D2. Then the equational theory is no longer degenerate, and we can live happily with weakening on both sides of the sequent.

References

• J-Y Girard, "A new constructive logic: Classical logic"
• V Danos, J-B Joinet, H Schellinx, "A New Deconstructive Logic: Linear Logic"
• O Laurent, "Classical isomorphisms of types"