On the semantics of proofs in classical sequent calculus

TL;DR

This paper investigates invariants of cut-reduction in classical sequent calculus, introducing a graph-based approach within GS4 to understand and normalize proof transformations.

Contribution

It develops a graph-based invariant in GS4, extending it to derivations with cuts, and introduces a new proof system with simplified rule permutations.

Findings

Graph induced by axioms is preserved under rule permutations

Refined axiom-induced graphs are preserved during cut-elimination

New proof system simplifies rule permutations to identities

Abstract

We discuss the problem of finding non-trivial invariants of non-deterministic, symmetric cut-reduction procedures in the classical sequent calculus. We come to the conclusion that (an enriched version of) the propositional fragment of GS4 -- i.e. the one-sided variant of Kleene's context-sharing style sequent system G4, where independent rule applications permute freely -- is an ideal framework in which to attack the problem. We show that the graph induced by axiom rules linking dual atom occurrences is preserved under arbitrary rule permutations in the cut-free fragment of GS4. We then refine the notion of axiom-induced graph so as to extend the result to derivations with cuts, and we exploit the invertibility of logical rules to define a global normalisation procedure that preserves the refined axiom-induced graphs, thus yielding a non-trivial invariant of cut-elimination in GS4. Finally, we build upon the result to devise a new proof system for classical propositional logic, where the rule permutations of GS4 reduce to identities.