Skip to main content
Log in

Matrix identities and the pigeonhole principle

  • Published:
Archive for Mathematical Logic Aims and scope Submit manuscript

Abstract.

We show that short bounded-depth Frege proofs of matrix identities, such as PQ=IQP=I (over the field of two elements), imply short bounded-depth Frege proofs of the pigeonhole principle. Since the latter principle is known to require exponential-size bounded-depth Frege proofs, it follows that the propositional version of the matrix principle also requires bounded-depth Frege proofs of exponential size.

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

Access this article

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  1. Miklós Ajtai.: The complexity of the pigeonhole principle. In Proceedings of the 29th Annual IEEE Symposium on the Foundations of Computer Science. 346–355 (1988)

  2. Paul Beame, Russell Impagliazzo, Jan Krajícek, Toniann Pitassi, Pavel Pudlák, Alan Woods.: Exponential lower bounds for the pigeonhole principle. In Proceedings of the 24th Annual ACM Symposium on theory of computing. 200–220 (1992)

  3. Peter Clote, Evangelos Kranakis.: Boolean Functions and Computation Models. Springer-Verlag, 2002

  4. Stephen~A. Cook, Michael Soltys.: The proof complexity of linear algebra. In Seventeenth Annual IEEE Symposium on Logic in Computer Science (LICS 2002). 2002

  5. Jan Krajícek, Pavel Pudlák, Alan Woods.: Exponential lower bound to the size of bounded depth Frege proofs of the pigeonhole principle. Random Structures and Algorithms. 7, 15–39 (1995)

    MathSciNet  Google Scholar 

  6. Toniann Pitassi, Paul Beame, Russell: Impagliazzo. Exponential lower bounds for the pigeonhole principle. Computational Complexity. 3, 97–140 (1993)

    Google Scholar 

  7. Michael Soltys.: The Complexity of Derivations of Matrix Identities. PhD thesis, University of Toronto, 2001

  8. Michael Soltys.: Extended Frege and Gaussian elimination. Bulletin of the Section of Logic, Polish Academy of Sciences. 31~(4), 189–206 (2002)

  9. Alasdair Urquhart, Xudong Fu.: Simplified lower bounds for propositional proofs.Notre Dame Journal of Formal Logic. 37, 523–544 (1996)

    Article  MathSciNet  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Corresponding author

Correspondence to Michael Soltys.

Rights and permissions

Reprints and permissions

About this article

Cite this article

Soltys, M., Urquhart, A. Matrix identities and the pigeonhole principle. Arch. Math. Logic 43, 351–357 (2004). https://doi.org/10.1007/s00153-003-0205-z

Download citation

  • Received:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s00153-003-0205-z

Keywords

Navigation