|
Cycling in proofs and feasibility
Author(s):
A.
Carbone
Journal:
Trans. Amer. Math. Soc.
352
(2000),
2049-2075.
MSC (1991):
Primary 03F07, 03F20, 03F05, 03H15, 68R10
Posted:
September 8, 1999
MathSciNet review:
1603882
Retrieve article in:
PDF
This article is available free of charge
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:
- 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
 -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'{e}matiques/Informatique, Universit\a'{e} de Paris XII, 61 Avenue du G\a'{e}n\a'{e}ral de Gaulle, 94010 Cr\a'{e}teil Cedex, France
Email:
ale@gauss.math.jussieu.fr, ale@univ-paris12.fr
DOI:
10.1090/S0002-9947-99-02300-4
PII:
S 0002-9947(99)02300-4
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
Posted:
September 8, 1999
Additional Notes:
Partially supported by the Lise-Meitner Stipendium # M00187-MAT (Austrian FWF)
Copyright of article:
Copyright
2000,
American Mathematical Society
|
