A New Paper
It’s a new year, and it’s time for a new paper, so here is “Proof Terms for Classical Derivations” I’ve been working on these ideas for about a year, from some rough talks over most of 2016, to many conversations with my colleague Shawn as I attempted to iron out the details, to many more hours in front of whiteboards, I’ve finally got something I’m happy to show in public.
The paper still rough, but the ideas are all there, and I think the theorems are all correct. The paper is under 50 pages—but only just! It proposes a new account of proof terms for classical propositional logic. These proof terms give a new account of what it is for one sequent derivation to represent the “same underlying proof” as another. Two derivations represent the same proof if and only if they have the same proof term. In the paper I show that two derivations have the same proof term if and only if one can be permuted into the other, using a natural class of transformations of derivations. Finally, I show that cut elimination for proof terms is confluent and strongly normalising, giving a new account of what it is to evaluate a classical proof, in a way that does not collapse into triviality.
Here’s an example from the paper, of three derivations, with the same concluding proof term:
If this looks interesting to you, please take a look. I’d appreciate your feedback. Thanks!
