On the lengths of proofs of consistency

a survey of results
  • Pavel Pudlák
Part of the Collegium Logicum book series (COLLLOGICUM, volume 2)


This article is essentially a part of my thesis for the degree DrSc (Doctor of Sciences). Therefore it mainly surveys my articles [42, 43, 44, 29, 30, 45, 23], and it is structured according to the requirements for such theses. I made only minor changes in the original text and added a few further references. Since Gödel’s main achievement concerns the problem of consistency and some of the problems that I am going to describe had been considered by him, I think that it is appropriate to publish this article in Gödel Society.


Turing Machine Complexity Theory Propositional Calculus Proof System Peano Arithmetic 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Miklos Ajtai. The complexity of the pigeonhole principle. In Proceedings of the 29th Annual IEEE Symposium on Foundations of Computer Science, pages 346–355, 1988.Google Scholar
  2. 2.
    Miklos Ajtai. The independence of the modulo p counting principles. In Proc. 26th ACM Symp. on Theory of Computing,pages 402–411, 1994.Google Scholar
  3. 3.
    Mathias Baaz and Pavel Pudlák. Kreisel’s conjecture for Lat. In Peter Clote and Jan Krajícek, editors, Arithmetic Proof Theory and Computational Complexity, pages 30–39. Oxford Univ. Press, 1993.Google Scholar
  4. 4.
    Paul Beame, Russell Impagliazzo, Jan Krajícek, Toniann Pitassi, Pavel Pudlák, and Alan Woods. Exponential lower bounds for the pigeonhole principle. In Proceedings of the 24th Annual ACM Symposium on Theory of Computing, pages 200–221, 1992.Google Scholar
  5. 5.
    A. Bezboruah and J. Shepherdson. Gödel’s second incompleteness theorem for Q. J. Symbolic Logic, pages 503–512, 1976.Google Scholar
  6. 6.
    Samuel R. Buss. Bounded Arithmetic. Bibliopolis, 1986. Revision of 1985 Princeton University Ph.D. thesis.Google Scholar
  7. 7.
    Samuel R. Buss and Aleksandar Ignjatović. Unprovability of consistency statements in fragments of bounded arithmetic. In preparation, 1993.Google Scholar
  8. 8.
    R. Carnap. Logische Syntax der Sprache. Springer-Verlag, 1934.MATHGoogle Scholar
  9. 9.
    Stephen A. Cook. Feasibly constructive proofs and the propositional calculus. In Proceedings of the 7th Annual ACM Symposium on Theory of Computing,pages 83–97, 1975.Google Scholar
  10. 10.
    Martin Dowd. Propositional Representation of Arithmetic Proofs. PhD thesis, University of Toronto, 1979.Google Scholar
  11. 11.
    A.G. Dragalin. Correctness of inconsistent theories with notions of feasibility. volume 108 of Lecture Notes in Comp. Sci.,pages 58–79, 1985.Google Scholar
  12. 12.
    A. Esenine-Volpin. Le programme ultra-intuitionniste des fondements des mathematiques. In Infinitistic Methods, Proceedings of the Symposium on Foundations of Mathematics, pages 201–223. PWN, Warsaw, 1961.Google Scholar
  13. 13.
    J. Ferrante and Ch. W. Rackoff. The Computational Complexity of Logical Theories. LNM 718. Springer-Verlag, 1979.MATHGoogle Scholar
  14. 14.
    H. Friedman. On the consistency, completeness, and correctness problems. Ohio State Univ., unpublished, 1979.Google Scholar
  15. 15.
    H. Friedman. Translatability and relative consistency II. Ohio State Univ., unpublished, 1979.Google Scholar
  16. 16.
    Yu.V. Gavrilenko. Monotone theories of feasible numbers. Doklady Akademii Nauk SSSR, 276(1):18–22, 1984.MathSciNetGoogle Scholar
  17. 17.
    Gerhard Gentzen. Die Widerspruchsfreiheit der reinen Zahlentheorie. Mathematische Annalen, 112:493–565, 1936. English translation in Gerhard Gentzen, Collected Papers of Gerhard Gentzen, Editted by M. E. Szabo, North-Holland, 1969, pp. 132–213.Google Scholar
  18. 18.
    Gerhard Gentzen. Collected Papers of Gerhard Gentzen. North-Holland, 1969. Editted by M. E. Szabo.Google Scholar
  19. 19.
    K. Gödel. Uber formal unentscheidbare Sätze der Principia Mathematica und vewandter Systeme I. Monatshefte Math. Phys., 38:173–198, 1931.CrossRefGoogle Scholar
  20. 20.
    K. Gödel. Uber die Länge von Beweisen. Ergebnisse eines Mathematischen Kolloquiums,pages 23–24, 1936. English translation in Kurt Gödel: Collected Works, Volume 1, pages 396–399, Oxford University Press, 1986.Google Scholar
  21. 21.
    P. Hájek. On interpretability in set theories II. Commentatione Math. Univ. Carol., 13:445–455, 1972.MATHGoogle Scholar
  22. 22.
    Petr Häjek. On a new notion of partial conservativity. In Logic Colloquium ‘83, pages 217–232. Springer-Verlag, 1983.Google Scholar
  23. 23.
    Petr Häjek, Franco Montagna, and Pavel Pudlák. Abbreviating proofs using meta-mathematical rules. In Peter Clote and Jan Krajícek, editors, Arithmetic Proof Theory and Computational Complexity, pages 197–221. Oxford Univ. Press, 1993.Google Scholar
  24. 24.
    Petr Häjek and Pavel Pudlák. Metamathematics of First-order Arithmetic. Springer-Verlag, 1993.Google Scholar
  25. 25.
    D. Hilbert. Die Grundlagen der Mathematik, volume 5 of Hamburger Mathematische Einzelschriften. Teubner, 1934. A lecture presented in Hamburg in July 1927.Google Scholar
  26. 26.
    A. Ignjatovié. Fragments of First and Second Order Arithmetic and Length of Proofs. PhD thesis, University of California at Berkeley, 1990.Google Scholar
  27. 27.
    Jan Krajíček. A note on proofs of falsehood. Archiv f. Math. Logic u. Grundlagen d. Math., 26:169–179, 1987.MATHGoogle Scholar
  28. 28.
    Jan Krajíček. Lower bounds to the size of constant-depth propositional proofs. Journal of Symbolic Logic, 59(1):73–86, 1994.MathSciNetCrossRefMATHGoogle Scholar
  29. 29.
    Jan Krajícek and Pavel Pudlâk. On the structure of initial segments of models of arithmetic. Archive for Mathematical Logic, 28:91–98, 1989.MathSciNetCrossRefMATHGoogle Scholar
  30. 30.
    Jan Krajícek and Pavel Pudlâk. Propositional proof systems, the consistency of first-order theories and the complexity of computations. Journal of Symbolic Logic, 54:1063–1079, 1989.MathSciNetCrossRefMATHGoogle Scholar
  31. 31.
    Jan Krajícek and Pavel Pudlâk. Quantified propositional calculi and fragments of bounded arithmetic. Zeitschrift für Mathematische Logik and Grundlagen der Mathematik,36:29–46, 1990.CrossRefMATHGoogle Scholar
  32. 32.
    Jan Krajícek, Pavel Pudlâk, and Gaisi Takeuti. Bounded arithmetic and the polynomial hierarchy. Annals of Pure and Applied Logic, 52:143–154, 1991.MathSciNetCrossRefMATHGoogle Scholar
  33. 33.
    Jan Krajíček and Gaisi Takeuti. On induction-free provability. Annals of Math. and Artificial Intelligence, 6:107–126, 1992.CrossRefMATHGoogle Scholar
  34. 34.
    R. Montague. Theories incomparable with respect to relative interpretability. Journal of Symbolic Logic, 27:195–211, 1962.MathSciNetCrossRefGoogle Scholar
  35. 35.
    V. P. Orevkov. Correctness of short proofs in theory with notions of feasibility. volume 417 of Lecture Notes in Comp. Sci.,pages 242–245, 1990.Google Scholar
  36. 36.
    S. Orey. Relative interpretations. Journal of Symbolic Logic, 24:281–282, 1959.Google Scholar
  37. 37.
    S. Orey. Relative interpretations. Zeitschrift für Mathematische Logik and Grundlagen der Mathematik, 7:146–153, 1961.MathSciNetCrossRefMATHGoogle Scholar
  38. 38.
    R. Parikh. Existence and feasibility in arithmetic. J. Symbolic Logic, 36:494–508, 1971.MathSciNetCrossRefMATHGoogle Scholar
  39. 39.
    J. B. Paris and C. Dimitracopoulos. Truth definitions for formulas. In Logic et algoritmic, L ‘enscignment Mathematique No 30, pages 318–329, 1982.Google Scholar
  40. 40.
    J. B. Paris and C. Dimitracopoulos. A note on the undefinability of cuts. J. Symbolic Logic, 48:564–569, 1983.MathSciNetCrossRefMATHGoogle Scholar
  41. 41.
    J.B. Paris and L. Harrington. A mathematical incompleteness in Peano Arithmetic. In Handbook of Mathematical Logic, pages 1133–1142. North-Holland, 1977.Google Scholar
  42. 42.
    Pavel Pudlák. Cuts, consistency statements and interpretation. Journal of Symbolic Logic, 50:423–441, 1985.MathSciNetCrossRefMATHGoogle Scholar
  43. 43.
    Pavel Pudlák. On the lengths of proofs of finitistic consistency statements in first order theories. In Logic Colloquium ‘84, pages 165–196. North-Holland, 1986.Google Scholar
  44. 44.
    Pavel Pudlák. Improved bounds to the lengths of proofs of finitistic consistency statements. In Logic and Combinatorics, volume 65 of Contemporary Mathematics, pages 309–331. American Mathematical Society, 1987.Google Scholar
  45. 45.
    Pavel Pudlák. A note on bounded arithmetic. Fundamenta Mathematicae, 136:85–89, 1990.MathSciNetMATHGoogle Scholar
  46. 46.
    C. Smoriński. Nonstandard models and related developments. In Harvey Fried-man’s Research on the Foundations of Mathematics, pages 179–229. North Holland, 1985.Google Scholar
  47. 47.
    R.M. Solovay. Injecting inconsistencies into models of PA. Annals of Pure and Applied Logic, 44:101–132, 1989.MathSciNetCrossRefGoogle Scholar
  48. 48.
    R.M. Solovay. Upper bounds on the speedup of GB over ZF. preprint, 1990.Google Scholar
  49. 49.
    R. Statman. Proof search and speed-up in the predicate calculus. Ann. Math. Logic, 15:225–287, 1978.MathSciNetCrossRefMATHGoogle Scholar
  50. 50.
    V. Švejdar. Modal analysis of generalized Rosser sentences. Journ. of Symb. Logic, 48:986–999, 1983.CrossRefMATHGoogle Scholar
  51. 51.
    G. Takeuti. Some relations among systems for bounded arithmetic. Annals of Pure and Applied Logic, 39:75–104, 1988.MathSciNetCrossRefMATHGoogle Scholar
  52. 52.
    O.V. Verbitsky. Optimal algorithms for coNP-sets and the problem EXP=?NEXP. Matematicheskie zametki, 50(2):37–46, 1991. Eglish translation in: Math. Notes 50,1–2, (1991), pp. 798–801.Google Scholar
  53. 53.
    L.Ch. Verbrugge. Efficient Mathematics. PhD thesis, Universiteit van Amsterdam, 1993.Google Scholar
  54. 54.
    A. Visser. The unprovability of small consistency. Archive for Math. Logic, 32:275–298, 1993.MathSciNetCrossRefMATHGoogle Scholar
  55. 55.
    A. Wilkie. On sentences interpretable in systems of arithmetic. In Logic Colloquium ‘84, pages 329–342. North-Holland, 1986.Google Scholar
  56. 56.
    A.J. Wilkie and J.B. Paris. On the schema of induction for bounded arithmetical formulas. Annals of Pure and Applied Logic, 35:261–302, 1987.MathSciNetCrossRefMATHGoogle Scholar

Copyright information

© Springer-Verlag/Wien 1996

Authors and Affiliations

  • Pavel Pudlák
    • 1
  1. 1.Mathematical InstituteAcademy of SciencesPragueCzech Republic

Personalised recommendations