Lecture Notes on Cut Elimination
Frank Pfenning · 2012
After presenting an interpretation of linear propositions in the sequent calculus as session types, we now return to studying properties of the sequent calculus itself in order to better understand how to search for proofs. The central theorem here is cut elimination: any provable sequent has a proof without using the cut rule. This will have many consequences. To appreciate the import of the theorem, consider the rule of cut.