Cut-Restriction: From Cuts to Analytic Cuts

Cut-elimination is the bedrock of proof theory with a multitude of applications from computational interpretations to proof analysis. It is also the starting point for important metatheoretical investigations into decidability, complexity, disjunction property, interpolation, and more. Unfortunately cut-elimination does not hold for the sequent calculi of most non-classical logics. It is well-known that the key to applications is the subformula property (a typical consequence of cut-elimination) rather than cut-elimination itself. With this in mind, we introduce cutrestriction, a procedure to restrict arbitrary cuts to analytic cuts (when elimination is not possible). The algorithm applies to all sequent calculi satisfying language-independent and simple-tocheck conditions, and it is obtained by adapting age-old cutelimination. Our work encompasses existing results in a uniform way, subsumes Gentzen's cut-elimination, and establishes new analytic cut properties.

• We introduce the first proof transformation reducing arbitrary cuts to analytic cuts that applies to a large class of propositional sequent calculi. In doing so, we extend Gentzen's age-old transformations.

• We provide easy-to-check sufficient conditions on the sequent calculus for analytic cut property.

Cut-restriction needs a novel idea: At first sight it might seem reasonable to assume that cut restriction follows from some slight adaptation of cut-elimination. We illustrate using the case of S5 that this is not the case. The following presumes some knowledge of cut-elimination; the reader unfamiliar with this terminology is referred to Section II. First consider the cut below that is well-known [11] to be not eliminable in S5: ¬p ⇒ ¬p (¬r) ⇒ ¬ ¬p, ¬p (5) ⇒ ¬ ¬p, ¬p p ⇒ p (¬l) ¬p, p ⇒ (T ) ¬p, p ⇒ cut p ⇒ ¬ ¬p