Remote Access Transactions of the American Mathematical Society
Green Open Access

Transactions of the American Mathematical Society

ISSN 1088-6850(online) ISSN 0002-9947(print)



Cycling in proofs and feasibility

Author: A. Carbone
Journal: Trans. Amer. Math. Soc. 352 (2000), 2049-2075
MSC (1991): Primary 03F07, 03F20, 03F05, 03H15, 68R10
Published electronically: September 8, 1999
MathSciNet review: 1603882
Full-text PDF Free Access

Abstract | References | Similar Articles | Additional Information

Abstract: There is a common perception by which small numbers are considered more concrete and large numbers more abstract. A mathematical formalization of this idea was introduced by Parikh (1971) through an inconsistent theory of feasible numbers in which addition and multiplication are as usual but for which some very large number is defined to be not feasible. Parikh shows that sufficiently short proofs in this theory can only prove true statements of arithmetic. We pursue these topics in light of logical flow graphs of proofs (Buss, 1991) and show that Parikh's lower bound for concrete consistency reflects the presence of cycles in the logical graphs of short proofs of feasibility of large numbers. We discuss two concrete constructions which show the bound to be optimal and bring out the dynamical aspect of formal proofs. For this paper the concept of feasible numbers has two roles, as an idea with its own life and as a vehicle for exploring general principles on the dynamics and geometry of proofs. Cycles can be seen as a measure of how complicated a proof can be. We prove that short proofs must have cycles.

References [Enhancements On Off] (What's this?)

  • 1. P. Bernays. Sur le platonisme dans les mathématiques. L'Enseignement Mathématique, 34:52-69, 1935.
  • 2. George Boolos, Don’t eliminate cut, J. Philos. Logic 13 (1984), no. 4, 373–378. MR 765992,
  • 3. Samuel R. Buss, The undecidability of 𝑘-provability, Ann. Pure Appl. Logic 53 (1991), no. 1, 75–102. MR 1114179,
  • 4. A. Carbone. On Logical Flow Graphs. Ph.D. Dissertation, Graduate School of The City University of New York, May 1993.
  • 5. A. Carbone, Interpolants, cut elimination and flow graphs for the propositional calculus, Ann. Pure Appl. Logic 83 (1997), no. 3, 249–299. MR 1434359,
  • 6. A. Carbone. Turning cycles into spirals. Annals of Pure and Applied Logic, 96:57-73, 1997.
  • 7. A. Carbone. Proofs and Groups with distorted Length Function. Manuscript, 1996.
  • 8. A. Carbone and S. Semmes. Looking from the inside and from the outside. I.H.E.S. preprint M/96/44, 1996 (Bures-sur-Yvette, France).
  • 9. A. Carbone and S. Semmes, Making proofs without modus ponens: an introduction to the combinatorics and complexity of cut elimination, Bull. Amer. Math. Soc. (N.S.) 34 (1997), no. 2, 131–159. MR 1423203,
  • 10. A. Carbone and S. Semmes. Geometry, Symmetry and Implicit Representations of Combinatorial Structures. Book in preparation, 1997.
  • 11. 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,
  • 12. M.E. Dummett. Wang's paradox. In Truth and Other Enigmas, pages 248-268. Harvard University Press, Cambridge, 1978. Also appeared in Synthèse 30:301-324, 1975.
  • 13. M.E. Dummett. Wittgenstein's philosophy of mathematics. In Truth and Other Enigmas, pages 166-185. Harvard University Press, Cambridge, 1978. Also appeared in The Philosophical Review, Cornell University, 1959.
  • 14. A. S. Ésénine-Volpine, Le programme ultra-intuitionniste des fondements des mathématiques., Infinitistic Methods (Proc. Sympos. Foundations of Math., Warsaw, 1959) Pergamon, Oxford; Państwowe Wydawnictwo Naukowe, Warsaw, 1961, pp. 201–223 (French). MR 0147389
  • 15. A. S. Yessenin-Volpin, The ultra-intuitionistic criticism and the antitraditional program for foundations of mathematics, Intuitionism and proof theory (Proc. Conf., Buffalo, N.Y., 1968) North-Holland, Amsterdam, 1970, pp. 3–45. MR 0295876
  • 16. R. O. Gandy, Limitations to mathematical knowledge, Logic Colloquium ’80 (Prague, 1980) Stud. Logic Foundations Math., vol. 108, North-Holland, Amsterdam-New York, 1982, pp. 129–146. MR 673789
  • 17. Jean-Yves Girard, Proof theory and logical complexity, Studies in Proof Theory. Monographs, vol. 1, Bibliopolis, Naples, 1987. MR 903244
  • 18. Jean-Yves Girard, Linear logic, Theoret. Comput. Sci. 50 (1987), no. 1, 101. MR 899269,
  • 19. S.C. Kleene. Introduction to Metamathematics, volume 1 of Bibliotheca Mathematica, Monographs on Pure and Applied Mathematics. Groningen, Walters-Noordhoff, 1988.
  • 20. G. Kreisel, Axiomatizations of nonstandard analysis that are conservative extensions of formal systems for classical standard analysis, Applications of Model Theory to Algebra, Analysis, and Probability (Internat. Sympos., Pasadena, Calif., 1967) Holt, Rinehart and Winston, New York, 1969, pp. 93–106. MR 0238686
  • 21. G. Mannoury. Methodologisches und Philosophisches zur Elementar-Mathematik. Visser, Haarlem, 1909.
  • 22. Edward Nelson, Predicative arithmetic, Mathematical Notes, vol. 32, Princeton University Press, Princeton, NJ, 1986. MR 869999
  • 23. Rohit Parikh, A conservation result, Applications of Model Theory to Algebra, Analysis, and Probability (Internat. Sympos., Pasadena, Calif., 1967) Holt, Rinehart and Winston, New York, 1969, pp. 107–108. MR 0234831
  • 24. V. P. Orevkov. Lower Bounds for increasing complexity of derivations after cut elimination. Journal of Soviet Mathematics, 20(4), 1982.
  • 25. Rohit Parikh, Existence and feasibility in arithmetic, J. Symbolic Logic 36 (1971), 494–508. MR 0304152,
  • 26. R. Parikh. The problem of vague predicates. In Language, Logic and Method, R.S. Cohen and M.W. Wartofsky, editors, pages 241-261. 1983.
  • 27. H. Poincaré. The Foundations of Science. Science Press, 1913.
  • 28. V.Yu. Sazonov. On feasible numbers. In Proceedings of The Kleene's Conference on Mathematical Logic, Varna, 1990.
  • 29. 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,
  • 30. Gaisi Takeuti, Proof theory, North-Holland Publishing Co., Amsterdam-Oxford; American Elsevier Publishing Co., Inc., New York, 1975. Studies in Logic and the Foundations of Mathematics, Vol. 81. MR 0536648
    G. Takeuti, \cyr Teoriya dokazatel′stv., Izdat. “Mir”, Moscow, 1978 (Russian). Translated from the English by T. K. Soholev; Edited by S. I. Adjan. MR 0536649
  • 31. A.S. Troelstra. Remarks on intuitionism and the philosophy of mathematics (revised version). In Proceedings of the Congresso Internazionale ``Nuovi Problemi della Logica e della Filosofia della Scienza'', Viareggio 8-13 January, 1990.
  • 32. 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
  • 33. Petr Vopěnka, Mathematics in the alternative set theory, BSB B. G. Teubner Verlagsgesellschaft, Leipzig, 1979. Teubner-Texte zur Mathematik. [Teubner Texts in Mathematics]; With German, French and Russian summaries. MR 581368
  • 34. Ludwig Wittgenstein, Remarks on the foundations of mathematics, Revised edition, MIT Press, Cambridge, Mass.-London, 1978. Edited by G. H. von Wright, R. Rhees and G. E. M. Anscombe; Translated from the German by G. E. M. Anscombe. MR 519516

Similar Articles

Retrieve articles in Transactions of the American Mathematical Society with MSC (1991): 03F07, 03F20, 03F05, 03H15, 68R10

Retrieve articles in all journals with MSC (1991): 03F07, 03F20, 03F05, 03H15, 68R10

Additional Information

A. Carbone
Affiliation: Math\a’ematiques/Informatique, Universit\a’e de Paris XII, 61 Avenue du G\a’en\a’eral de Gaulle, 94010 Cr\a’eteil Cedex, France

Keywords: Feasible numbers, cut elimination, cycles in proofs, structure of proofs, complexity of proofs.
Received by editor(s): June 13, 1997
Received by editor(s) in revised form: January 21, 1998
Published electronically: September 8, 1999
Additional Notes: Partially supported by the Lise-Meitner Stipendium # M00187-MAT (Austrian FWF)
Article copyright: © Copyright 2000 American Mathematical Society