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

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. G. Boolos. Don't eliminate cut. Journal of Philosophical Logic, 13:373-378, 1984. MR 85i:03029
  • 3. S. Buss. The undecidability of $k$-provability. Annals of Pure and Applied Logic, 53:72-102, 1991. MR 92g:03071
  • 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. In Annals of Pure and Applied Logic, 83:249-299, 1997. MR 98i:03073
  • 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. In Bulletin of the American Mathematical Society, 34:131-159, 1997. MR 98c:03112
  • 10. A. Carbone and S. Semmes. Geometry, Symmetry and Implicit Representations of Combinatorial Structures. Book in preparation, 1997.
  • 11. A.G. Dragalin. Correctness of inconsistent theories with notion of feasibility. In LNCS 208, pages 58-79. Springer Verlag, 1985. MR 87e:03150
  • 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. Esenin-Volpin. Le programme ultra-intuitionniste des fondements des mathématiques. In Infinitistic Methods, Proceedings of the Symposium on the Foundations of Mathematics, pages 201-223. PWN. Warsaw, 1961. MR 26:4905
  • 15. A.S. Esenin-Volpin. The ultra-intuitionistic criticism and the antitraditional program for foundations of mathematics. In A. Kino, J. Myhill, and R.E. Vesley, editors, Intuitionism and Proof Theory, pages 3-45. North-Holland, 1970. MR 45:4938
  • 16. R.O. Gandy. Limitation to mathematical knowledge. In D. van Dalen, D. Lascar, and J. Smiley, editors, Logic Colloquium 80, pages 129-146. North-Holland Publishing Company, 1982. MR 84d:00010
  • 17. J.Y. Girard. Proof Theory and Logical Complexity, volume 1 of Studies in Proof Theory, Monographs. Bibliopolis, 1987. MR 89a:03113
  • 18. J.Y. Girard. Linear Logic. Theoretical Computer Science, 50:1-102, 1987. MR 89m:03057
  • 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. In Application of Model Theory, W.A.J. Luxemburg, editor, pages 93-106. Holt, Rinehart and Winston, New York, 1969. MR 39:50
  • 21. G. Mannoury. Methodologisches und Philosophisches zur Elementar-Mathematik. Visser, Haarlem, 1909.
  • 22. E. Nelson. Predicative Arithmetic. Princeton University Press, Princeton, New Jersey, 1986. MR 88c:03061
  • 23. R. Parikh. A conservation result. In W.A.J. Luxemburg, editor, Application of Model Theory, pages 107-108. Holt, Rinehart and Winston, New York, 1969. MR 38:3145
  • 24. V. P. Orevkov. Lower Bounds for increasing complexity of derivations after cut elimination. Journal of Soviet Mathematics, 20(4), 1982.
  • 25. R. Parikh. Existence and feasibility in arithmetic. Journal of Symbolic Logic, 36:494-508, 1971. MR 46:3287
  • 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. R. Statman. Bounds for proof-search and speed-up in predicate calculus. In Annals of Mathematical Logic, 15:225-287. 1978. MR 81c:03049
  • 30. G. Takeuti. Proof Theory, volume 81 of Studies in Logic and the Foundations of Mathematics. North Holland, 1975. MR 58:27366a
  • 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. Tseitin. The complexity of a deduction in the propositional predicate calculus. In Zap. Nauchn. Sem. Leningrad Otd. Mat. Inst. Akad. Nauk SSSR, 8:234-259. 1968. MR 43:6098
  • 33. P. Vopenka. Mathematics in the Alternative Set Theory. Teubner, Leipzig, 1979. MR 83f:03051
  • 34. L. Wittgenstein. In Remarks on the Foundations of Mathematics. R. Rhees, G.H. von Wright and G.E.M. Anscombe, editors, The MIT Press, Cambridge, 1978. Revised Version. MR 80f:00009

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

American Mathematical Society