Remote Access Bulletin of the American Mathematical Society

Bulletin of the American Mathematical Society

ISSN 1088-9485(online) ISSN 0273-0979(print)



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 | References | Similar Articles | Additional Information

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 [Enhancements On Off] (What's this?)

  • 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.
  • P. Beame, R. Impagliazzo, J. Krajíček, T. Pitassi, and P. Pudlák, Lower bounds on Hilbert’s nullstellensatz and propositional proofs, Proceedings of the London Mathematical Society (3) 73 (1996), 1–26.
  • 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
  • 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 Company, 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
  • Samuel R. Buss, The undecidability of $k$-provability, Ann. Pure Appl. Logic 53 (1991), no. 1, 75–102. MR 1114179, DOI
  • 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.
  • P. Clote and J. Krajíček, Open problems, Arithmetic, Proof Theory and Computational Complexity (Peter Clote and Jan Krajíček, eds.), Oxford University Press, 1993, pp. 1–19.
  • 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
  • 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
  • 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
  • Harvey Friedman, The complexity of explicit definitions, Advances in Math. 20 (1976), no. 1, 18–29. MR 401459, DOI
  • H. Furstenberg and B. Weiss, Topological dynamics and combinatorial number theory, J. Analyse Math. 34 (1978), 61–85 (1979). MR 531271, DOI
  • Michael R. Garey and David S. Johnson, Computers and intractability, W. H. Freeman and Co., San Francisco, Calif., 1979. A guide to the theory of NP-completeness; A Series of Books in the Mathematical Sciences. 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
  • 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 ${\bf F}$, Logic Colloquium ’88 (Padova, 1988) Stud. Logic Found. Math., vol. 127, North-Holland, Amsterdam, 1989, pp. 221–260. MR 1015328, DOI
  • 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
  • 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
  • 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
  • Petr Hájek and Pavel Pudlák, Metamathematics of first-order arithmetic, Perspectives in Mathematical Logic, Springer-Verlag, Berlin, 1993. MR 1219738
  • Armin Haken, The intractability of resolution, Theoret. Comput. Sci. 39 (1985), no. 2-3, 297–308. MR 821207, DOI
  • John E. Hopcroft and Jeffrey D. Ullman, Introduction to automata theory, languages, and computation, Addison-Wesley Publishing Co., Reading, Mass., 1979. Addison-Wesley Series in Computer Science. 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
  • 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
  • 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
  • J. Krajíček, Bounded arithmetic, propositional logic and complexity theory, Cambridge University Press, 1995.
  • 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, ${\rm 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
  • 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
  • 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
  • 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
  • Pavel Pudlák, Ramsey’s theorem in bounded arithmetic, Computer Science Logic, LNCS, vol. 533, Springer-Verlag, 1991, pp. 308–317.
  • 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, Springer-Verlag, Berlin-New York, 1977. Translated from the revised German edition by J. N. Crossley; Grundlehren der Mathematischen Wissenschaften, Band 225. MR 0505313
  • Proof theory and constructive mathematics, Handbook of mathematical logic, Part D, North-Holland, Amsterdam, 1977, pp. 819–1142. Studies in Logic and the Foundations of Math., Vol. 90. 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
  • R. Statman, Lower bounds on Herbrand’s theorem, Proc. Amer. Math. Soc. 75 (1979), no. 1, 104–107. MR 529224, DOI
  • 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

Similar Articles

Retrieve articles in Bulletin of the American Mathematical Society with MSC (1991): 03F05, 68Q15

Retrieve articles in all journals with MSC (1991): 03F05, 68Q15

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

S. Semmes
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