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

Carbone, A.; Semmes, S.

doi:10.1090/S0273-0979-97-00715-5

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