Making Proofs without Modus Ponens: An Introduction to the Combinatorics andComplexity of Cut Elimination

摘要

Modus Ponens says that if you know A and you know that A implies B then you knowB. 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 logic as 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.