A theory of cut-restriction: first steps

TL;DR

This paper introduces a novel approach called cut-restriction, which adapts traditional cut-elimination to restrict cut-formulas in cases where elimination isn't possible, focusing on analytic cuts in specific logics.

Contribution

It pioneers a theory of cut-restriction by adapting cut-elimination to handle analytic cuts in complex sequent calculi, expanding proof-theoretic techniques.

Findings

Applied to bi-intuitionistic logic and S5 sequent calculi

Demonstrated the feasibility of cut-restriction in non-eliminable cases

Laid groundwork for further development of cut-restriction theory

Abstract

Cut-elimination is the bedrock of proof theory. It is the algorithm that eliminates cuts from a sequent calculus proof that leads to cut-free calculi and applications. Cut-elimination applies to many logics irrespective of their semantics. Such is its influence that whenever cut-elimination is not provable in a sequent calculus the invariable response has been a move to a richer proof system to regain it. In this paper we investigate a radically different approach to the latter: adapting age-old cut-elimination to restrict the shape of the cut-formulas when elimination is not possible. We tackle the "first level" above cut-free: analytic cuts. Our methodology is applied to the sequent calculi for bi-intuitionistic logic and S5 where analytic cuts are already known to be required. This marks the first steps in a theory of cut-restriction.