Non-trivial invariants of rule permutation and cut-elimination in classical sequent calculus

These are the slides accompanying the talk I gave at the Logic Colloquium (ASL European Summer Meeting) 2023 in Milan, Italy. The content of the talk originated from some unpublished notes. I paste below for historical purposes the abstract that was accepted by the program committee:

Abstract

Cut-elimination procedures in classical sequent calculus are notoriously non-deterministic and non-confluent, both in the original formulation by Gentzen and in later reformulations. It is natural to ask whether those instances of non-confluence are superficial in nature, i.e. whether distinct normal forms of the same derivation are in fact correlated in a non-trivial way. A famous counter-example by Lafont purports to show that the answer is negative, that is, any notion of proof equivalence compatible with classical cut-elimination must be a trivial one that identifies all proofs of the same sequent. A long standing open question has been whether it is possible to work around Lafont’s example by natural and non-trivial adjustments of the calculus and/or of cut-reduction steps, without resorting to symmetry-breaking techniques like polarization or embeddings into intuitionistic or linear logic.

Working within the propositional fragment of GS4 — i.e. the one-sided variant of Kleene’s context-sharing style sequent system G4 — where parallel rule applications permute freely, we show that the graph induced by axiom rules linking dual atom occurrences is preserved under arbitrary rule permutations in cut-free proofs. We then refine the notion of axiom-induced graph so as to extend the result to proofs with cuts. Finally, we exploit rule permutations to define a global normalization procedure that preserves axiom-induced graphs, thus yielding a non-trivial invariant of cut-elimination in GS4.

We conclude by discussing briefly the possibility of extending the result to context-splitting style systems and first-order logic.