Cycling in proofs and feasibility

Carbone, A.

doi:10.1090/S0002-9947-99-02300-4

Cycling in proofs and feasibility
HTML articles powered by AMS MathViewer

by A. Carbone PDF

Trans. Amer. Math. Soc. 352 (2000), 2049-2075 Request permission

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

P. Bernays. Sur le platonisme dans les mathématiques. L’Enseignement Mathématique, 34:52–69, 1935.
George Boolos, Don’t eliminate cut, J. Philos. Logic 13 (1984), no. 4, 373–378. MR 765992, DOI 10.1007/BF00247711
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. Dissertation, Graduate School of The City University of New York, May 1993.
A. Carbone, Interpolants, cut elimination and flow graphs for the propositional calculus, Ann. Pure Appl. Logic 83 (1997), no. 3, 249–299. MR 1434359, DOI 10.1016/S0168-0072(96)00019-X
A. Carbone. Turning cycles into spirals. Annals of Pure and Applied Logic, 96:57–73, 1997.
A. Carbone. Proofs and Groups with distorted Length Function. Manuscript, 1996.
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).
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, DOI 10.1090/S0273-0979-97-00715-5
A. Carbone and S. Semmes. Geometry, Symmetry and Implicit Representations of Combinatorial Structures. Book in preparation, 1997.
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}
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.
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.
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
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
R. O. Gandy, Limitations to mathematical knowledge, Logic Colloquium ’80 (Prague, 1980) Studies in Logic and the Foundations of Mathematics, vol. 108, North-Holland, Amsterdam-New York, 1982, pp. 129–146. MR 673789
Jean-Yves Girard, Proof theory and logical complexity, Studies in Proof Theory. Monographs, vol. 1, Bibliopolis, Naples, 1987. MR 903244
Jean-Yves Girard, Linear logic, Theoret. Comput. Sci. 50 (1987), no. 1, 101. MR 899269, DOI 10.1016/0304-3975(87)90045-4
S.C. Kleene. Introduction to Metamathematics, volume 1 of Bibliotheca Mathematica, Monographs on Pure and Applied Mathematics. Groningen, Walters-Noordhoff, 1988.
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
G. Mannoury. Methodologisches und Philosophisches zur Elementar-Mathematik. Visser, Haarlem, 1909.
Edward Nelson, Predicative arithmetic, Mathematical Notes, vol. 32, Princeton University Press, Princeton, NJ, 1986. MR 869999, DOI 10.1515/9781400858927
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
V. P. Orevkov. Lower Bounds for increasing complexity of derivations after cut elimination. Journal of Soviet Mathematics, 20(4), 1982.
Rohit Parikh, Existence and feasibility in arithmetic, J. Symbolic Logic 36 (1971), 494–508. MR 304152, DOI 10.2307/2269958
R. Parikh. The problem of vague predicates. In Language, Logic and Method, R.S. Cohen and M.W. Wartofsky, editors, pages 241–261. 1983.
H. Poincaré. The Foundations of Science. Science Press, 1913.
V.Yu. Sazonov. On feasible numbers. In Proceedings of The Kleene’s Conference on Mathematical Logic, Varna, 1990.
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
Gaisi Takeuti, Proof theory, Studies in Logic and the Foundations of Mathematics, Vol. 81, North-Holland Publishing Co., Amsterdam-Oxford; American Elsevier Publishing Co., Inc., New York, 1975. MR 0536648
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.
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
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
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