Making proofs without Modus Ponens: An introduction to the combinatorics and complexity of cut elimination
Alessandra Carbone, Stephen Semmes · Bulletin of the American Mathematical Society · 1997
Modus Ponens says that if you know $A$ and you know that $A$ implies $B$, then you know $B$. This is a basic rule that we take for granted and use repeatedly, but there is a gem of a theorem in logic by Gentzen to the effect that it is not needed in some logical systems. It is fun to say, “You can make proofs without lemmas” to mathematicians and watch how they react, but our true intention here is to let go of logic as a reflection of reasoning and move towards combinatorial aspects. Proofs contain basic problems of algorithmic complexity within their framework, and there is strong geometric and dynamical flavor inside them.