Proof Complexity

  • Pavel Pudlák
Part of the Springer Monographs in Mathematics book series (SMM)


The first section deals with classical results in proof theory and the lengths of proofs in first-order logic. We explain cut-elimination, Herbrand’s Theorem and ordinal analysis of first order theories. We present bounds on the increase of lengths of proofs in cut-elimination and some other speed-up results. The next two sections are about mainstream results in proof complexity. We explain how first-order theories are associated with complexity classes. Further, we show how these theories are associated with propositional proof systems. Feasible incompleteness, the topic treated in the last section, refers to results and conjectures that talk about the feasible versions of classical incompleteness theorems.


Polynomial Time Boolean Function Turing Machine Proof System Search Problem 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. 29.
    Bonet, M.L., Pitassi, T., Raz, R.: On interpolation and automatization for Frege systems. SIAM J. Comput. 29(6), 1939–1967 (2000) MathSciNetzbMATHCrossRefGoogle Scholar
  2. 34.
    Buss, S.R.: Bounded Arithmetic. Bibliopolis, Naples (1986) zbMATHGoogle Scholar
  3. 35.
    Buss, S.R., Krajíček, J.: An application of boolean complexity to separation problems in bounded arithmetic. Proc. Lond. Math. Soc. 69(3), 1–21 (1994) zbMATHCrossRefGoogle Scholar
  4. 42.
    Church, A.: A set of postulates for the foundation of logic (1). Ann. Math. 33, 346–366 (1932) MathSciNetCrossRefGoogle Scholar
  5. 45.
    Chvátal, V.: Edmonds polytops and a hierarchy of combinatorial problems. Discrete Math. 4, 305–337 (1973) MathSciNetzbMATHCrossRefGoogle Scholar
  6. 49.
    Cook, S.A.: Feasibly constructive proofs and the propositional calculus. In: Proc. Seventh Annual ACM Symposium on Theory of Computing, pp. 83–97. ACM, New York (1975) CrossRefGoogle Scholar
  7. 51.
    Cook, S.A., Reckhow, R.A.: The relative efficiency of propositional proof systems. J. Symb. Log. 44(1), 36–50 (1979) MathSciNetzbMATHCrossRefGoogle Scholar
  8. 53.
    Craig, W.: Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory. J. Symb. Log. 22(3), 269–285 (1957) MathSciNetzbMATHCrossRefGoogle Scholar
  9. 81.
    Friedman, H.: On the consistency, completeness and correctness. Unpublished typescript (1979) Google Scholar
  10. 89.
    Gentzen, G.: Untersuchungen über das logische Schließen I. Math. Z. 39(2), 176–210 (1934) MathSciNetGoogle Scholar
  11. 90.
    Gentzen, G.: Untersuchungen über das logische Schließen II. Math. Z. 39(3), 405–431 (1935) MathSciNetCrossRefGoogle Scholar
  12. 94.
    Glaßer, C., Selman A, A., Sengupta, S., Zhang, L.: Disjoint NP-pairs. SIAM J. Comput. 33(6), 1369–1416 (2004) MathSciNetzbMATHCrossRefGoogle Scholar
  13. 104.
    Gomory, R.E.: Outline of an algorithm for integer solutions to linear programs. Bull. Am. Math. Soc. 64, 275–278 (1958) MathSciNetzbMATHCrossRefGoogle Scholar
  14. 115.
    Håstad, J.: Almost optimal lower bounds for small depth circuits. In: Micali, S. (ed.) Randomness and Computation, Advances in Computing Research, vol. 5, pp. 143–170. JAI Press, London (1989) Google Scholar
  15. 121.
    Herbrand, J.: Recherches sur la theorie de la demonstration. Travaux de la Societe des Sciences et des Lettres de Varsovie, Class III, Sciences Mathematiques et Physiques 33, 33–160 (1930) Google Scholar
  16. 134.
    Hrubeš, P.: A lower bound for intuitionistic logic. Ann. Pure Appl. Log. 146, 72–90 (2007) zbMATHCrossRefGoogle Scholar
  17. 135.
    Impagliazzo, R.: A personal view of average-case complexity. In: 10th Annual Structure in Complexity Theory Conference (SCT’95), pp. 134–147 (1995) Google Scholar
  18. 140.
    Jeřábek, E.: The strength of sharply bounded induction. Math. Log. Q. 52(6), 613–624 (2006) MathSciNetzbMATHCrossRefGoogle Scholar
  19. 144.
    Johnson, D., Papadimitriou, C., Yannakakis, M.: How easy is local search? J. Comput. Syst. Sci. 37, 79–100 (1988) MathSciNetzbMATHCrossRefGoogle Scholar
  20. 162.
    Krajíček, J.: Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic. J. Symb. Log. 62(2), 457–486 (1997) zbMATHCrossRefGoogle Scholar
  21. 164.
    Krajíček, J., Pudlák, P.: Propositional proof systems, the consistency of first order theories and the complexity of computations. J. Symb. Log. 54(3), 1063–1079 (1989) zbMATHCrossRefGoogle Scholar
  22. 166.
    Krajíček, J., Pudlák, P.: Some consequences of cryptographical conjectures for \(S_{2}^{1}\) and EF. In: Leivant, D. (ed.) Logic and Computational Complexity, (Proceedings of Meeting Held in Indianapolis 1994). LNCS, vol. 960, pp. 210–220. Springer, Berlin (1995) Google Scholar
  23. 167.
    Krajíček, J., Pudlák, P., Takeuti, G.: Bounded arithmetic and polynomial hierarchy. Ann. Pure Appl. Log. 52, 143–154 (1991) zbMATHCrossRefGoogle Scholar
  24. 187.
    Luckhardt, H.: Herbrand-Analysen Zweier Beweise Des Satzes von Roth: Polynomiale Anzahlschranken. J. Symb. Log. 54(1) (1989) Google Scholar
  25. 194.
    Matoušek, J.: A combinatorial proof of Kneser’s conjecture. Combinatorica 2(1), 163–170 (2004) CrossRefGoogle Scholar
  26. 200.
    Mostowski, A.: Sentences Undecidable in Formalized Arithmetic: An Exposition of the Theory of Kurt Gödel. Studies in Logic. North-Holland, Amsterdam (1952) zbMATHGoogle Scholar
  27. 211.
    Parikh, R.: Existence and feasibility in arithmetic. J. Symb. Log. 36(3), 494–508 (1971) MathSciNetzbMATHCrossRefGoogle Scholar
  28. 215.
    Paris, J., Wilkie, A.: Δ 0 sets and induction. In: Proc. Jadswin Logic Conference (Poland), pp. 237–248. Leeds University Press, Leeds (1981) Google Scholar
  29. 223.
    Pudlák, P.: On the length of proofs of finitistic consistency statements in first order theories. In: Logic Colloquium, vol. 84, pp. 165–196. North-Holland, Amsterdam (1986) CrossRefGoogle Scholar
  30. 224.
    Pudlák, P.: Improved bounds to the length of proofs of finitistic consistency statements. In: Contemporary Mathematics, vol. 65, pp. 309–331. Am. Math. Soc., Providence (1987) Google Scholar
  31. 225.
    Pudlák, P.: Lower bounds for resolution and cutting planes proofs and monotone computations. J. Symb. Log. 62(3), 981–998 (1997) zbMATHCrossRefGoogle Scholar
  32. 233.
    Quine, W.V.: Mathematical Logic. Norton, New York (1940) Google Scholar
  33. 241.
    Razborov, A.: Unprovability of lower bounds on the circuit size in certain fragments of bounded arithmetic. Izv. Math. 59(1), 201–224 (1995) MathSciNetCrossRefGoogle Scholar
  34. 242.
    Razborov, A.: Bounded arithmetic and lower bounds in Boolean complexity. In: Clote, P., Remmel, J. (eds.) Feasible Mathematics II, pp. 344–386. Birkhauser, Basel (1995) CrossRefGoogle Scholar
  35. 258.
    Schütte, K.: Bewiestheorie. Springer, Berlin (1960) Google Scholar
  36. 272.
    Smith, R.L.: The consistency strengths of some finite forms of the Higman and Kruskal theorems. In: Harrington, L.A., et al. (eds.) Harvey’s Friedman Research on the Foundations of Mathematics, pp. 119–136. North-Holland, Amsterdam (1985) CrossRefGoogle Scholar
  37. 284.
    Statman, R.: Proof-search and speed-up in the predicate calculus. Ann. Math. Log. 15, 225–287 (1978) MathSciNetzbMATHCrossRefGoogle Scholar

Copyright information

© Springer International Publishing Switzerland 2013

Authors and Affiliations

  • Pavel Pudlák
    • 1
  1. 1.ASCRPragueCzech Republic

Personalised recommendations