On the content of classical propositional proofs

These are the slides accompanying the talk I gave within the Logic Group seminar at Scuola Normale Superiore in Pisa, Italy, on May 15^th, 2023. They present some unpublished work (still in progress) about a graphical proof-system for classical logic (in the style of proof-nets).

Abstract

We recall briefly the origins and significance of the problem of proof identity in classical logic, then proceed to show why extensional approaches are bound to fail and discuss an abstract method proposed in older and more recent literature to account for the intensional features of proof systems.

We introduce a graphical proof system (i.e., proofs are represented as graphs) for classical propositional logic, where the logical rule permutations of classical sequent calculus are reduced to identities and the invertibility of logical rules follows from easy and efficient constructions. The same constructions establish a direct correspondence between this system and the cut-free fragment of the sequent calculus GS4, thus providing an account of the content of GS4 derivations up to arbitrary rule permutations, in the sense specified at the beginning of the talk. We then refine the structure of our graph-based proofs in a non-trivial way, allowing us to provide an interesting cut-elimination algorithm, and show that the new system provides a rich invariant of the cut-elimination process in an augmented version of GS4.

Finally, we compare our work with previous attempts, and discuss possible applications and future developments.