Making proofs without Modus Ponens: An introduction to the combinatorics and complexity of cut elimination
Authors: A. Carbone and S. Semmes
Journal: Bull. Amer. Math. Soc. 34 (1997), 131-159
MSC (1991): Primary 03F05; Secondary 68Q15
MathSciNet review: 1423203
Full-text PDF Free Access
Abstract: Modus Ponens says that if you know and you know that implies , then you know . 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.
Affiliation: IHES, 35 Route de Chartres, 91440 Bures-sur-Yvette, France
Address at time of publication: Mathématiques/Informatique, Université de Paris XII, 94010 Creteil Cedex, France
Affiliation: Department of Mathematics, Rice University, Houston, Texas 77251
Received by editor(s): July 3, 1996
Received by editor(s) in revised form: December 1, 1996
Additional Notes: The first author was supported by the Lise-Meitner Stipendium # M00187-MAT (Austrian FWF) and the second author was supported by the U.S. National Science Foundation. Both authors are grateful to IHES for its hospitality.
Article copyright: © Copyright 1997 American Mathematical Society