Abstract.
We show that short bounded-depth Frege proofs of matrix identities, such as PQ=I⊃QP=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.
Similar content being viewed by others
References
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)
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)
Peter Clote, Evangelos Kranakis.: Boolean Functions and Computation Models. Springer-Verlag, 2002
Stephen~A. Cook, Michael Soltys.: The proof complexity of linear algebra. In Seventeenth Annual IEEE Symposium on Logic in Computer Science (LICS 2002). 2002
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)
Toniann Pitassi, Paul Beame, Russell: Impagliazzo. Exponential lower bounds for the pigeonhole principle. Computational Complexity. 3, 97–140 (1993)
Michael Soltys.: The Complexity of Derivations of Matrix Identities. PhD thesis, University of Toronto, 2001
Michael Soltys.: Extended Frege and Gaussian elimination. Bulletin of the Section of Logic, Polish Academy of Sciences. 31~(4), 189–206 (2002)
Alasdair Urquhart, Xudong Fu.: Simplified lower bounds for propositional proofs.Notre Dame Journal of Formal Logic. 37, 523–544 (1996)
Author information
Authors and Affiliations
Corresponding author
Rights 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
Received:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s00153-003-0205-z