Skip to main content
SpringerLink
Log in

On Frege and Extended Frege Proof Systems

  • Conference paper
Feasible Mathematics II

Part of the book series: Progress in Computer Science and Applied Logic ((PCS,volume 13))

Abstract

We propose a framework for proving lower bounds to the size of EF-proofs (equivalently, to the number of proof-steps in F-proofs) in terms of boolean valuations. The concept is motivated by properties of propositional provability in models of bounded arithmetic and it is a finitisation of a particular forcing construction explained also in the paper. It reduces the question of proving a lower bound to the question of constructing a partial boolean algebra and a map of formulas into that algebra with particular properties. We show that in principle one can obtain via this method optimal lower bounds (up to a polynomial increase).

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. M. Ajtai: “\(\Sigma_1^1\)-formulae in finite structures”, Annals of Pure and Applied Logic, 24, (1983), pp. 1 – 48.

    Article  Google Scholar 

  2. M. Ajtai: “The complexity of the pigeonhole principle”, in: Proc. IEEE 29th Annual Symp. on Foundation of Computer Science, (1988), pp. 346–355.

    Google Scholar 

  3. T. Arai: “Frege system, ALOGTIMEand bounded arithmetic”, unpublished manuscript, (1993).

    Google Scholar 

  4. J.A. Bondy: “Induced subsets”, J.Combinatorial Theory (B), 12, (1972), pp. 201 – 202.

    Article  Google Scholar 

  5. M. L. Bonet: “Number of symbols in Frege proofs with and without the deduction rule”, in: Arithmetic, Proof Theory and Computational Complexity, eds.P. Clote and J. Krajíček, Oxford Press, (1993), pp.61– 95.

    Google Scholar 

  6. M.L. Bonet, S.R. Buss and T. Pitassi: “Are there hard examples for Frege systems?”, this volume.

    Google Scholar 

  7. S.R. Buss: Bounded Arithmetic, Bibliopolis, Naples,(1986).

    Google Scholar 

  8. S.R. Buss: “The propositional pigeonhole principle has polynomial size Frege proofs”, J. Symbolic Logic 52, (1987), pp. 916 – 927.

    Article  Google Scholar 

  9. S.R. Buss: “Propositional consistency proofs”, Annals of Pure and Applied Logic, 52, (1991), pp. 3 – 29.

    Article  Google Scholar 

  10. S.R. Buss, J. Krajíček and G. Takeuti: “On provably total functions in bounded arithmetic theories R i3 , U i2 and V i2 ”,in: Arithmetic, Proof Theory and Computational Complexity, eds.P. Clote and J. Krajíček, Oxford Press, (1993), pp. 116 – 161.

    Google Scholar 

  11. S.R. Buss and G. Turán: “Resolution proofs of generalized pigeonhole principle”, Theoretical Computer Science, 62, (1988), pp. 311 – 317.

    Article  Google Scholar 

  12. P. Clote: “ALOGTIME and a conjecture of S.A. Cook”, Annals of Mathematics and Artificial Inteligence, 6, (1992), pp. 57 – 106.

    Article  Google Scholar 

  13. P. Clote: “On polynomial size Frege proofs of certain combinatorial principles”, in: Arithmetic, Proof Theory and Computational Complexity, eds.P. Clote and J. Krajíček, Oxford Press, (1993), pp. 162 – 184.

    Google Scholar 

  14. P. Clote and J. Krajíček: “Open problems”, in: Arithmetic, Proof Theory and Computational Complexity, eds.P. Clote and J. Krajíček, Oxford Press, (1993), pp. 1 – 19.

    Google Scholar 

  15. P. Clote and G. Takeuti: “Bounded arithmetic for NC, ALogTIME, Land NL”, Annals of Pure and Applied Logic 56, (1992), pp. 73 – 117.

    Article  Google Scholar 

  16. S.A. Cook: “Feasibly constructive proofs and the propositional calculus”, in: Proc. 7th Annual ACM Symp. on Theory of Computing, (1975), pp. 83–97.

    Google Scholar 

  17. S.A. Cook and A.R. Reckhow: “The relative efficiency of propositions! proof systems”, J. Symbolic Logic 44 (1), (1979), pp. 36 – 50.

    Article  Google Scholar 

  18. W. Cook, C. R. Coullard and G. Turan: “On the complexity of cutting plane proofs”, Discrete Applied Mathematics, 18, (1987). pp. 25 – 38.

    Article  Google Scholar 

  19. M. Dowd: “Model-theoretic aspects of P ≠ NP”, unpublished manuscript, (1985).

    Google Scholar 

  20. M. Furst, J.B.Saxe and M. Sipser: “Parity, circuits and the polynomial-time hierarchy”, Math. Systems Theory, 17, (1984), pp. 13 – 27.

    Article  Google Scholar 

  21. A. Goerdt: “Cutting plane versus Frege proof systems”, in: Computer Science Logic, eds. E. Börger et. al., LN in Computer Science 533, Springer Verlag, pp.174–194, (1991).

    Google Scholar 

  22. A. Haken: “The intractability of resolution”, Theoretical Computer Science 39, (1985), pp. 297 – 308.

    Article  Google Scholar 

  23. J. Krajíček: “On the number of steps in proofs”, Annals of Pure and Applied Logic 41, (1989), pp. 153 – 178.

    Article  Google Scholar 

  24. J. Krajíček: “Speed-up for propositional Frege systems via generalizations of proofs”, Commentationes Mathematicae Universitas Carolinae 30 (1), (1989), pp. 137 – 140.

    Google Scholar 

  25. J. Krajíček: “Exponentiation and second-order bounded arithmetic”, Annals of Pure and Applied Logic 48, (1990), pp. 261 – 276

    Article  Google Scholar 

  26. J. Krajíček: “Lower bounds to the size of constant-depth propositional proofs”, Journal of Symbolic Logic, 59 (1), (1994), pp. 73 – 86.

    Article  Google Scholar 

  27. J. Krajčcek: Bounded arithmetic, propositional logic and complexity theory, a book prepared for the Cambridge University Press, (1993), 401 p.

    Google Scholar 

  28. J. Krajíček and P. Pudlák: “Propositional proof systems, the consistency of first order theories and the complexity of computations”, J. Symbolic Logic 54 (3), (1989), pp. 1063 – 1079

    Article  Google Scholar 

  29. J. Krajíček and P. Pudlák: “Quantified propositional calculi and fragments of bounded arithmetic”, Zeitschrift f. Mathematikal Logik u. Grundlagen d. Mathematik 36, (1990), pp. 29 – 46.

    Google Scholar 

  30. J. Krajíček and P. Pudlák: “Propositional provability in models of weak arithmetic”, in:Computer Science Logic, eds. E. Boerger, H. Kleine-Bunning and M.M. Richter, Springer-Verlag, (1990), pp. 193 – 210.

    Google Scholar 

  31. J. Krajíček and P. Pudlák and A. Woods: “Exponential lower bound to the size of bounded depth Frege proofs of the pigeonhole principle”, submitted.

    Google Scholar 

  32. J. Krajíček and G. Takeuti: “On bounded \(\Sigma_1^1\)-polynomial induction”, in: Feasible Mathematics, eds. S.R. Buss and P.J. Scott, Birkhauser, (1990), pp. 259 – 280.

    Chapter  Google Scholar 

  33. L. Lovász: “Communication complexity: a survey”, in: Paths, Flows and VLSI Layout, eds. Korte, Lovász, Promer, Schrijver, Springer-Verlag, (1990), pp. 325 – 266.

    Google Scholar 

  34. K. Mehlhorn and F. M. Schmidt: “Las Vegas is better than determinism in VLSI and distributed computing”, 14th Annual ACM Symp. on Th. of Computing, (1982), pp. 330 – 337.

    Google Scholar 

  35. R. Parikh: “Some results on the length of proofs”, Transactions of the A.M.S., 177, (1973), pp. 29 – 36.

    Article  Google Scholar 

  36. T. Pitassi, P. Beame and R. Impagliazzo: “Exponential lower bounds for the pigeonhole principle”, Computational Complexity, 3, (1993), pp. 97 – 308.

    Article  Google Scholar 

  37. J. Paris and A. Wilkie: “Counting problems in bounded arithmetic”, in: Methods in Mathematical Logic, LNM 1130, Springer (1985), pp. 317–340.

    Chapter  Google Scholar 

  38. A.A. Razborov: “An Equivalence between second order bounded domain bounded arithmetic and first order bounded arithmetic”, in: Arithmetic, Proof Theory and Computational Complexity, eds. P. Clote and J. Krajíček, Oxford Univ. Press, (1993), pp. 247 – 277.

    Google Scholar 

  39. R.A.Reckhow: “On the lengths of proofs in the prepositional calculus”, PhD.Thesis, Dept. of CS, University of Toronto, (1976).

    Google Scholar 

  40. P.M. Spira: “On time-hardware complexity of tradeoffs for Boolean functions”, in: Proc. 4th Hawaii Symp. System Sciences, Western Periodicals Co., North Hollywood (1971), pp. 525 – 527.

    Google Scholar 

  41. G. Takeuti: “RSUV Isomorphism”, in: Arithmetic, Proof Theory and Computational Complexity, eds. P. Clote and J. Krajíček, Oxford Univ. Press, (1993), pp. 364 – 386.

    Google Scholar 

  42. G. Takeuti and W.M. Zaring: Axiomatic Set Theory, Springer-Verlag, (1973), 238 p.

    Google Scholar 

  43. G. C. Tseitin: “On the complexity of derivations in propositional calculus”, in: Studies in mathematics and mathematical logic, Part II, ed. A.O.Slisenko, (1968), pp. 115 – 125.

    Google Scholar 

  44. G.C. Tseitin and A.A. Choubarian: “On some bounds to the lengths of logical proofs in classical propositional calculus” (Russian), Trudy Vyčisl Centra AN Arm SSR i Erevanskovo Univ. 8, (1975), 57 – 64.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Mathematical Institut, Academy of Sciences, Žitna 25, Praha 1, 115 67, Czech Republic

    Jan Krajíček

Authors
  1. Jan Krajíček
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science, Boston College, 02167, Chestnut Hill, MA, USA

    Peter Clote

  2. Department of Mathematics, University of California, 92093, San Diego La Jolla, CA, USA

    Jeffrey B. Remmel

Rights and permissions

Reprints and permissions

Copyright information

© 1995 Birkhäuser Boston

About this paper

Cite this paper

Krajíček, J. (1995). On Frege and Extended Frege Proof Systems. In: Clote, P., Remmel, J.B. (eds) Feasible Mathematics II. Progress in Computer Science and Applied Logic, vol 13. Birkhäuser Boston. https://doi.org/10.1007/978-1-4612-2566-9_10

Download citation

  • DOI: https://doi.org/10.1007/978-1-4612-2566-9_10

  • Publisher Name: Birkhäuser Boston

  • Print ISBN: 978-1-4612-7582-4

  • Online ISBN: 978-1-4612-2566-9

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation