Hostname: page-component-586b7cd67f-2plfb Total loading time: 0 Render date: 2024-12-01T07:03:34.886Z Has data issue: false hasContentIssue false
  • English
  • Français

On Gödel's theorems on lengths of proofs I: Number of lines and speedup for arithmetics

Published online by Cambridge University Press:  12 March 2014

Samuel R. Buss
Samuel R. Buss*
Affiliation:
Department of Mathematics, University of California, San Diego, La Jolla, California 92093-0112, E-mail: [email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

This paper discusses lower bounds for proof length, especially as measured by number of steps (inferences). We give the first publicly known proof of Gödel's claim that there is superrecursive (in fact, unbounded) proof speedup of (i + l)st-order arithmetic over ith-order arithmetic, where arithmetic is formalized in Hilbert-style calculi with + and • as function symbols or with the language of PRA. The same results are established for any weakly schematic formalization of higher-order logic: this allows all tautologies as axioms and allows all generalizations of axioms as axioms.

Our first proof of Gödel's claim is based on self-referential sentences: we give a second proof that avoids the use of self-reference based loosely on a method of Statman.

Type
Survey/expository paper
Information
The Journal of Symbolic Logic , Volume 59 , Issue 3 , September 1994 , pp. 737 - 756
Copyright
Copyright © Association for Symbolic Logic 1994

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

REFERENCES

[1]Buss, S. R., On Gödels theorems on lengths of proofs II: Lower bounds for recognizing k symbolprovability, in preparation.Google Scholar
[2]Buss, S. R., Bounded arithmetic, Bibliopolis, Naples, 1986: revision of Ph.D. Thesis, Princeton University, Princeton, New Jersey, 1985.Google Scholar
[3]Ehrenfeucht, A. and Mycielski, J., Abbreviating proofs by adding new axioms, Bulletin of the American Mathematical Societyg, vol. 77 (1971), pp. 366–367.Google Scholar
[4]Enderton, H., A mathematical introduction to logic, Academic Press, New York, 1972.Google Scholar
[5]Farmer, W. M., A unification-theoretic method for investigating the k-provability problem, Annals of Pure and Applied Logic, vol. 51 (1991), pp. 173–214.CrossRefGoogle Scholar
[6]Gödel, K., Über die Länge von Beweisen, Ergebnisse eines Mathematischen Kolloquiums, (1936), pp. 23–24: English translation, Kurt Gödel: Collected Works, volume 1, Oxford University Press. London and New York, 1986, pp. 396–399.Google Scholar
[7]Krajíček, J., On the number of steps in proofs, Annals of Pure and Applied Logic, vol. 41 (1989), pp. 153–178.Google Scholar
[8]Krajíčekand, J.Pudlák, P., The number of proof lines and the size of proofs in first-order logic, Archive for Mathematical Logic, vol. 27 (1988), pp. 69–84.Google Scholar
[9]Kreisel, G. and Wang, H., Some applications of formalized consistency proofs, Fundamenta Mathematicae, vol. 42 (1955), pp. 101–110.CrossRefGoogle Scholar
[10]Mostowski, A., Sentences undecidable in formalized arithmetic: an exposition of the theory of Kurt Gödel, North-Holland, Amsterdam, 1952.Google Scholar
[11]Parikh, R. J., Some results on the lengths of proofs, Transactions of the American Mathematical Society, vol. 177 (1973), pp. 29–36.CrossRefGoogle Scholar
[12]Parikh, R. J., Introductory note to 1936 (a), Kurt Gödel, Collected Works, volume 1, Oxford University Press, London and New York, 1986, pp. 394–397.Google Scholar
[13]Pudlák, P., On the lengths of proofs of finitistic consistency statements in first-order theories, Logic Colloquium ‘84 (1986), North-Holland, Amsterdam, pp. 165–196.Google Scholar
[14]Pudlák, P., Improved bounds to the lengths of proofs of finitistic consistency statements, Logic and Combinatorics, Contemporary Mathematics, vol. 65, American Mathematical Society, Providence, Rhode Island, 1987, pp. 309–331.Google Scholar
[15]Statman, R., Speed-up by theories with infinite models, Proceedings of the American Mathematical Society, vol. 81 (1981), pp. 465–469.CrossRefGoogle Scholar
[16]Takeuti, G., Proof theory, 2nd edition North-Holland, Amsterdam, 1987.Google Scholar
[17]Wilkie, A. J. and Paris, J. B., On the scheme of induction for bounded arithmetic formulas, Annals of Pure and Applied Logic, vol. 35 (1987), pp. 261–302.CrossRefGoogle Scholar