Making Proofs without Modus Ponens: an introduction to the combinatorics and complexity of cut elimination TeX Export

@article{carb:maki97, abstract = {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.}, author = {Semmes, S. and Carbone, A.}, citeulike-article-id = {131913}, citeulike-linkout-0 = {http://www.ams.org/bull/1997-34-02/S0273-0979-97-00715-5/S0273-0979-97-00715-5.pdf}, journal = {Bulletin of the American Mathematical Society}, keywords = {combinatorics, complexity, cut\_elimination, logic, pnc, prooftheory, sequent}, month = {April}, pages = {131--159}, posted-at = {2005-03-18 08:31:31}, priority = {0}, title = {Making Proofs without Modus Ponens: an introduction to the combinatorics and complexity of cut elimination}, url = {http://www.ams.org/bull/1997-34-02/S0273-0979-97-00715-5/S0273-0979-97-00715-5.pdf}, volume = {34}, year = {1997} }

TY - JOUR ID - carb:maki97 L3 - citeulike-article-id:131913 N2 - 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. JF - Bulletin of the American Mathematical Society EP - 159 TI - Making Proofs without Modus Ponens: an introduction to the combinatorics and complexity of cut elimination VL - 34 SP - 131 KW - combinatorics KW - complexity KW - cut_elimination KW - logic KW - pnc KW - prooftheory KW - sequent AU - Semmes, S AU - Carbone, A PY - 1997/April// UR - http://www.ams.org/bull/1997-34-02/S0273-0979-97-00715-5/S0273-0979-97-00715-5.pdf ER -