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

HTML articles powered by AMS MathViewer

- by A. Carbone and S. Semmes PDF
- Bull. Amer. Math. Soc.
**34**(1997), 131-159 Request permission

## 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.## References

- M. Ajtai,
*The complexity of the pigeonhole principle*, Proc. IEEE 29$^{\mbox {th}}$ Annual*Symp. on Foundation of Computer Science*, 1988, pp. 346–355. - M. Ajtai,
*Parity and the pigeonhole principle*, Feasible mathematics (Ithaca, NY, 1989) Progr. Comput. Sci. Appl. Logic, vol. 9, Birkhäuser Boston, Boston, MA, 1990, pp. 1–24. MR**1232921** - Paul Beame, Russell Impagliazzo, Jan Krajíček, Toniann Pitassi, Pavel Pudlák, and Alan Woods,
*Exponential lower bounds for the pigeonhole principle*, Proceedings of the 24-th Annual ACM Symposium on Theory of Computing, 1992, pp. 200–221. - T. Venkatarayudu,
*The $7$-$15$ problem*, Proc. Indian Acad. Sci., Sect. A.**9**(1939), 531. MR**0000001**, DOI 10.1090/gsm/058 - Gianluigi Bellin,
*Ramsey interpreted: a parametric version of Ramsey’s theorem*, Logic and computation (Pittsburgh, PA, 1987) Contemp. Math., vol. 106, Amer. Math. Soc., Providence, RI, 1990, pp. 17–37. MR**1057813**, DOI 10.1090/conm/106/1057813 - Evert W. Beth,
*The foundations of mathematics: A study in the philosophy of science.*, Studies in Logic and the Foundations of Mathematics, North-Holland Publishing Co., Amsterdam, 1959. MR**0118674** - Samuel R. Buss,
*Polynomial size proofs of the propositional pigeonhole principle*, J. Symbolic Logic**52**(1987), no. 4, 916–927. MR**916397**, DOI 10.2307/2273826 - Samuel R. Buss,
*The undecidability of $k$-provability*, Ann. Pure Appl. Logic**53**(1991), no. 1, 75–102. MR**1114179**, DOI 10.1016/0168-0072(91)90059-U - A. Carbone,
*On logical flow graphs*, Ph.D. thesis, Graduate School of The City University of New York, 1993. - A. Carbone,
*Some combinatorics behind proofs*, Submitted for publication, 1995. - A. Carbone,
*Interpolants, cut elimination and flow graphs for the propositional calculus*, Annals of Pure and Applied Logic (1996), To appear. - A. Carbone,
*Cycling in proofs, feasibility and no speed-up for nonstandard arithmetic*, IHES preprint, 1996. - A. Carbone,
*Proofs and groups with distorted length function*, Unpublished manuscript, 1996. - A. Carbone and S. Semmes,
*Implicit descriptions and explicit contructions: Searching for lost symmetry in combinatorial complexity*, Manuscript (in preparation), 1996. - A. Carbone and S. Semmes,
*Looking from the inside and the outside*, IHES preprint, 1996. - A. Carbone and S. Semmes,
*Propositional proofs via combinatorial geometry and the search for symmetry*, IHES preprint, 1996. - T. Venkatarayudu,
*The $7$-$15$ problem*, Proc. Indian Acad. Sci., Sect. A.**9**(1939), 531. MR**0000001**, DOI 10.1090/gsm/058 - Stephen A. Cook and Robert A. Reckhow,
*The relative efficiency of propositional proof systems*, J. Symbolic Logic**44**(1979), no. 1, 36–50. MR**523487**, DOI 10.2307/2273702 - William Craig,
*Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory*, J. Symbolic Logic**22**(1957), 269–285. MR**104565**, DOI 10.2307/2963594 - A. G. Drágalin,
*Correctness of inconsistent theories with notions of feasibility*, Computation theory (Zaborów, 1984) Lecture Notes in Comput. Sci., vol. 208, Springer, Berlin, 1985, pp. 58–79. MR**827523**, DOI 10.1007/3-540-16066-3_{7} - Harvey Friedman,
*The complexity of explicit definitions*, Advances in Math.**20**(1976), no. 1, 18–29. MR**401459**, DOI 10.1016/0001-8708(76)90167-5 - H. Furstenberg and B. Weiss,
*Topological dynamics and combinatorial number theory*, J. Analyse Math.**34**(1978), 61–85 (1979). MR**531271**, DOI 10.1007/BF02790008 - Michael R. Garey and David S. Johnson,
*Computers and intractability*, A Series of Books in the Mathematical Sciences, W. H. Freeman and Co., San Francisco, Calif., 1979. A guide to the theory of NP-completeness. MR**519066** - John B. Garnett,
*Bounded analytic functions*, Pure and Applied Mathematics, vol. 96, Academic Press, Inc. [Harcourt Brace Jovanovich, Publishers], New York-London, 1981. MR**628971** - Gerhard Gentzen,
*Untersuchungen über das logische Schließen I–II*, Math. Z.**39**(1934), 176–210, 405–431. - Gerhard Gentzen,
*The collected papers of Gerhard Gentzen*, Studies in Logic and the Foundations of Mathematics, North-Holland Publishing Co., Amsterdam-London, 1969. Edited by M. E. Szabo. MR**0262050** - Jean-Yves Girard,
*Linear logic*, Theoret. Comput. Sci.**50**(1987), no. 1, 101. MR**899269**, DOI 10.1016/0304-3975(87)90045-4 - Jean-Yves Girard,
*Proof theory and logical complexity*, Studies in Proof Theory. Monographs, vol. 1, Bibliopolis, Naples, 1987. MR**903244** - Jean-Yves Girard,
*Geometry of interaction. I. Interpretation of system $\textbf {F}$*, Logic Colloquium ’88 (Padova, 1988) Stud. Logic Found. Math., vol. 127, North-Holland, Amsterdam, 1989, pp. 221–260. MR**1015328**, DOI 10.1016/S0049-237X(08)70271-4 - Jean-Yves Girard,
*Geometry of interaction. II. Deadlock-free algorithms*, COLOG-88 (Tallinn, 1988) Lecture Notes in Comput. Sci., vol. 417, Springer, Berlin, 1990, pp. 76–93. MR**1064138**, DOI 10.1007/3-540-52335-9_{4}9 - Jean-Yves Girard,
*Towards a geometry of interaction*, Categories in computer science and logic (Boulder, CO, 1987) Contemp. Math., vol. 92, Amer. Math. Soc., Providence, RI, 1989, pp. 69–108. MR**1003197**, DOI 10.1090/conm/092/1003197 - Jean-Yves Girard,
*Geometry of interaction. III. Accommodating the additives*, Advances in linear logic (Ithaca, NY, 1993) London Math. Soc. Lecture Note Ser., vol. 222, Cambridge Univ. Press, Cambridge, 1995, pp. 329–389. MR**1356021**, DOI 10.1017/CBO9780511629150.017 - Petr Hájek and Pavel Pudlák,
*Metamathematics of first-order arithmetic*, Perspectives in Mathematical Logic, Springer-Verlag, Berlin, 1993. MR**1219738**, DOI 10.1007/978-3-662-22156-3 - Armin Haken,
*The intractability of resolution*, Theoret. Comput. Sci.**39**(1985), no. 2-3, 297–308. MR**821207**, DOI 10.1016/0304-3975(85)90144-6 - John E. Hopcroft and Jeffrey D. Ullman,
*Introduction to automata theory, languages, and computation*, Addison-Wesley Series in Computer Science, Addison-Wesley Publishing Co., Reading, Mass., 1979. MR**645539** - Ulrich Kohlenbach,
*Effective moduli from ineffective uniqueness proofs. An unwinding of de la Vallée Poussin’s proof for Chebycheff approximation*, Ann. Pure Appl. Logic**64**(1993), no. 1, 27–94. MR**1241250**, DOI 10.1016/0168-0072(93)90213-W - Ulrich Kohlenbach,
*New effective moduli of uniqueness and uniform a priori estimates for constants of strong unicity by logical analysis of known proofs in best approximation theory*, Numer. Funct. Anal. Optim.**14**(1993), no. 5-6, 581–606. MR**1248130**, DOI 10.1080/01630569308816541 - Ulrich Kohlenbach,
*Analyzing proofs in analysis*, Proceedings of the*Logic Colloquium 93*– Keele (1994). - Jan Krajíček and Pavel Pudlák,
*The number of proof lines and the size of proofs in first order logic*, Arch. Math. Logic**27**(1988), no. 1, 69–84. MR**955313**, DOI 10.1007/BF01625836 - T. Venkatarayudu,
*The $7$-$15$ problem*, Proc. Indian Acad. Sci., Sect. A.**9**(1939), 531. MR**0000001**, DOI 10.1090/gsm/058 - Georg Kreisel,
*From foundations to science: justifying and unwinding proofs*, Zb. Rad. Mat. Inst. Beograd. (N.S.)**2(10)**(1977), 63–72. MR**497872** - G. Kreisel,
*Extraction of bounds: interpreting some tricks on the trade*, University-level computer assisted instruction at Stanford: 1968–1980 (P. Suppes, ed.), Institute for Mathematical Studies in the Social Sciences, no. tome 2 (10), 1981. - G. Kreisel,
*Neglected possibilities of processing assertions and proofs mechanically: choice of problems and data*, University-level computer assisted instruction at Stanford: 1968–1980 (P. Suppes, ed.), Institute for Mathematical Studies in the Social Sciences, no. tome 2 (10), 1981. - Shôji Maehara,
*On the interpolation theorem of Craig*, Sūgaku**12**(1960/61), 235–237 (Japanese). MR**166078** - A.R. Meyer,
*A note on the length of Craig’s interpolants*, Tech. report, Laboratory for Computer Science, M.I.T., October 1980. - Daniele Mundici,
*$\textrm {NP}$ and Craig’s interpolation theorem*, Logic colloquium ’82 (Florence, 1982) Stud. Logic Found. Math., vol. 112, North-Holland, Amsterdam, 1984, pp. 345–358. MR**762116**, DOI 10.1016/S0049-237X(08)71822-6 - Daniele Mundici,
*Tautologies with a unique Craig interpolant, uniform vs. nonuniform complexity*, Ann. Pure Appl. Logic**27**(1984), no. 3, 265–273. MR**765593**, DOI 10.1016/0168-0072(84)90029-0 - Vladimir P. Orevkov,
*Lower bounds for increasing complexity of derivations after cut elimination*, Journal of Soviet Mathematics**20(4)**(1982). - V. P. Orevkov,
*Complexity of proofs and their transformations in axiomatic theories*, Translations of Mathematical Monographs, vol. 128, American Mathematical Society, Providence, RI, 1993. Translated by Alexander Bochman from the original Russian manuscript; Translation edited by David Louvish. MR**1240316**, DOI 10.1090/mmono/128 - Christos H. Papadimitriou,
*Computational complexity*, Addison-Wesley Publishing Company, Reading, MA, 1994. MR**1251285** - Rohit Parikh,
*Existence and feasibility in arithmetic*, J. Symbolic Logic**36**(1971), 494–508. MR**304152**, DOI 10.2307/2269958 - T. Venkatarayudu,
*The $7$-$15$ problem*, Proc. Indian Acad. Sci., Sect. A.**9**(1939), 531. MR**0000001**, DOI 10.1090/gsm/058 - P. Pudlák,
*The lengths of proofs*, Handbook of Proof Theory (S. Buss, ed.), North Holland, 1996. - S. Riis,
*Independence in bounded arithmetic*, Ph.D. thesis, Oxford University, 1993. - Kurt Schütte,
*Proof theory*, Grundlehren der Mathematischen Wissenschaften, Band 225, Springer-Verlag, Berlin-New York, 1977. Translated from the revised German edition by J. N. Crossley. MR**0505313** *Proof theory and constructive mathematics*, Handbook of mathematical logic, Part D, Studies in Logic and the Foundations of Math., Vol. 90, North-Holland, Amsterdam, 1977, pp. 819–1142. With contributions by C. Smoryński, Helmut Schwichtenberg, Richard Statman, Solomon Feferman, A. S. Troelstra, Michael P. Fourman, Henk Barendregt, Jeff Paris and Leo Harrington. MR**0491063**- S. Semmes,
*Metric spaces and mappings seen at many scales*, Metric Structures of Riemannian Spaces, M. Gromov et al., Birkhäuser, 1996, to appear. - Richard Statman,
*Structural complexity of proofs*, Ph.D. thesis, Stanford University, 1974. - Richard Statman,
*Bounds for proof-search and speed-up in the predicate calculus*, Ann. Math. Logic**15**(1978), no. 3, 225–287 (1979). MR**528658**, DOI 10.1016/0003-4843(78)90011-6 - R. Statman,
*Lower bounds on Herbrand’s theorem*, Proc. Amer. Math. Soc.**75**(1979), no. 1, 104–107. MR**529224**, DOI 10.1090/S0002-9939-1979-0529224-9 - Elias M. Stein,
*Harmonic analysis: real-variable methods, orthogonality, and oscillatory integrals*, Princeton Mathematical Series, vol. 43, Princeton University Press, Princeton, NJ, 1993. With the assistance of Timothy S. Murphy; Monographs in Harmonic Analysis, III. MR**1232192** - Gaisi Takeuti,
*Proof theory*, 2nd ed., Studies in Logic and the Foundations of Mathematics, vol. 81, North-Holland Publishing Co., Amsterdam, 1987. With an appendix containing contributions by Georg Kreisel, Wolfram Pohlers, Stephen G. Simpson and Solomon Feferman. MR**882549** - G. S. Ceĭtin,
*The complexity of a deduction in the propositional predicate calculus.*, Zap. Naučn. Sem. Leningrad. Otdel. Mat. Inst. Steklov. (LOMI)**8**(1968), 234–259 (Russian). MR**0280378** - B. L. van der Waerden,
*Beweis einer baudetschen vermutung*, Nieuw Archiv Wiskunde (1927), 212–216. - Jan van Leeuwen (ed.),
*Handbook of theoretical computer science. Vol. A*, Elsevier Science Publishers, B.V., Amsterdam; MIT Press, Cambridge, MA, 1990. Algorithms and complexity. MR**1127166**

## Additional Information

**A. Carbone**- 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
- Email: ale@univ-paris12.fr
**S. Semmes**- Affiliation: Department of Mathematics, Rice University, Houston, Texas 77251
- Email: semmes@rice.edu
- 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.
- © Copyright 1997 American Mathematical Society
- Journal: Bull. Amer. Math. Soc.
**34**(1997), 131-159 - MSC (1991): Primary 03F05; Secondary 68Q15
- DOI: https://doi.org/10.1090/S0273-0979-97-00715-5
- MathSciNet review: 1423203