Hostname: page-component-77c78cf97d-tlp4c Total loading time: 0 Render date: 2026-04-29T00:50:07.256Z Has data issue: false hasContentIssue false
  • English
  • Français

Lower bounds to the size of constant-depth propositional proofs

Published online by Cambridge University Press:  12 March 2014

Jan Krajíček
Jan Krajíček*
Affiliation:
Mathematical Institute, Academy of Sciences, Žitná 25, Praha 1, 11567 Czech Republic, E-mail:krajicek@earn.cvut.cz
Get access Rights & Permissions [Opens in a new window]

Abstract

LK is a natural modification of Gentzen sequent calculus for propositional logic with connectives ¬ and ∧,∨ (both of bounded arity). Then for every d ≥ 0 and n ≥ 2, there is a set of depth d sequents of total size O(n3+d) which are refutable in LK by depth d + 1 proof of size exp(O(log2n)) but such that every depth d refutation must have the size at least exp(nΩ(1)). The sets express a weaker form of the pigeonhole principle.

Keywords

Lengths of proofspropositional calculusFrege systemspigeonhole principle

Information

Type
Research Article
Information
The Journal of Symbolic Logic , Volume 59 , Issue 1 , March 1994 , pp. 73 - 86
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.)

Article purchase

Temporarily unavailable

References

[1]Ajtai, M., The complexity of the pigeonhole principle, Proceedings of the 29th IEEE annual symposium on foundations of computer science, IEEE Computer Society Press, Washington, D.C., 1988, pp. 346–355.Google Scholar
[2]Ajtai, M., Parity and the pigeonhole principle, Feasible mathematics (Buss, S. R. and Scott, P. J., editors), Birkhäuser, Basel and Boston, 1990, pp. 1–24.Google Scholar
[3]Beame, P., Impagliazzo, R., and Pitassi, T., Exponential lower bounds for the pigeonhole principle, University of Toronto, TR 257/91, 1991.Google Scholar
[4]Bellantoni, S., Pitassi, T., and Urquhart, A., Approximation and small depth Frege proofs, Society for Industrial and Applied Mathematics Journal of Computing, vol. 21 (1992), pp. 1161–1179.Google Scholar
[5]Buss, S. R., Axiomatizations and conservation results for fragments of bounded arithmetic, Logic and computation (Sieg, Wilfred, editor), Contemporary Mathematics, vol. 106, American Mathematical Society, Providence, Rhode Island, 1990, pp. 57–84.CrossRefGoogle Scholar
[6]Buss, S. R. and Turán, G., Resolution proofs of generalized pigeonhole principles, Theoretical Computer Science, vol. 62 (1988), pp. 311–317.CrossRefGoogle Scholar
[7]Cejtin, G. C., On the complexity of the derivations in prepositional calculus, Studies in mathematics and mathematical logic, Part II (Silsenko, A. O., editor), 1968, pp. 115–125.Google Scholar
[8]Cook, S. A. and Reckhow, A. R., The relative efficiency of prepositional proof systems, this Journal, vol. 44 (1979), pp. 36–50.Google Scholar
[9]Craig, W., Three uses of the Herbrand-Gentzen theorem relating model theory and proof theory, this Journal, vol. 22 (1957), pp. 269–285.Google Scholar
[10]Haken, A., The intractability of resolution, Theoretical Computer Science, vol. 39 (1985), pp. 297–308.CrossRefGoogle Scholar
[11]Hastad, J., Almost optimal lower bounds for small depth circuits, Advances in Computer Research, vol. 5, JAI Press, 1989, pp. 143–170.Google Scholar
[12]Krajíček, J., Fragments of bounded arithmetic and bounded query classes, Transactions of the American Mathematical Society, vol. 338 (1993), pp. 587–598.CrossRefGoogle Scholar
[13]Krajíček, J., No counter-example interpretation and interactive computation, Logic from computer science (Moschovakis, Y. N., editor), Mathematical Sciences Research Institute Publications, vol. 21, Mathematical Science Research Institute, Berkeley, California, 1992, pp. 287–293.CrossRefGoogle Scholar
[14]Krajíček, J. and Pudlák, P., Prepositional proof systems, the consistency offirst-order theories and the complexity of computations, this Journal, vol. 54 (1989), pp. 1063–1079.Google Scholar
[15]Krajíček, J., Pudlák, P. and Woods, A., Exponential lower bound to the size of bounded depth Frege proofs of the pigeonhole principle, submitted.Google Scholar
[16]Paris, J. and Wilkie, A., Counting problems in bounded arithmetic, Methods in mathematical logic, Lecture Notes in Mathematics, vol. 1130, Springer-Verlag, Berlin and New York, 1985, pp. 317–340.CrossRefGoogle Scholar
[17]Paris, J., Wilkie, A., and Woods, A., Provability of the pigeonhole principle and the existence of infinitely many primes, this Journal, vol. 53 (1988), pp. 1235–1244.Google Scholar
[18]Sipser, M., Borel sets and circuit complexity, Proceedings of the 15th annual Association for Computing Machinery symposium on the theory of computing, Association for Computing machinery, New York, 1983, pp. 61–69.Google Scholar
[19]Smolensky, R., Algebraic methods in the theory of lower bounds for Boolean circuit complexity, Proceedings of the 19th annual Association for Computing Machinery symposium on the theory of computing, Association for Computing Machinery, New York, 1987, pp. 77–82.Google Scholar
[20]Spira, P. M., On time-hardward complexity of tradeoffs for Boolean functions, Proceedings of the 4th Hawaii Symposium on system sciences, Western Periodicals Co., North Hollywood, California, 1971, pp. 525–527.Google Scholar
[21]Statman, R., Proof search and speed-up in the predicate calculus, Annals of Mathematical Logic, vol. 15 (1978), pp. 225–287.CrossRefGoogle Scholar
[22]Tait, W. W., Normal derivability in classical logic, The syntax and semantics of infinitary languages (Barwise, J., editor), Springer-Verlag, New York, 1968, pp. 204–236.CrossRefGoogle Scholar
[23]Takeuti, G., Proof theory, North-Holland, Amsterdam, 1975.Google Scholar
[24]Toda, S., On the computational power of P P and ⊕ pr. Proceedings of the 30th IEEE annual symposium on foundations of computer science, IEEE Computer Society Press, Washington, D. C, 1989, pp. 514–519.CrossRefGoogle Scholar
[25]Yao, A., Separating the polynomial-time hierarchy by oracles, Proceedings of the 26th IEEE annual symposium on foundations of computer science, IEEE Computer Society Press, Washington, D.C., 1985, pp. 1–10.Google Scholar