Making proofs without Modus Ponens: An introduction to the combinatorics and complexity of cut elimination

Alessandra Carbone, S. Semmes

This paper is intended to provide an introduction to cut elimination which is accessible to a broad mathematical audience. Gentzen's cut elimination theorem is not as well known as…