{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,2]],"date-time":"2026-03-02T09:45:55Z","timestamp":1772444755937,"version":"3.50.1"},"reference-count":25,"publisher":"Cambridge University Press (CUP)","issue":"1","license":[{"start":{"date-parts":[[2014,3,12]],"date-time":"2014-03-12T00:00:00Z","timestamp":1394582400000},"content-version":"unspecified","delay-in-days":7316,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. symb. log."],"published-print":{"date-parts":[[1994,3]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p><jats:bold>LK<\/jats:bold> is a natural modification of Gentzen sequent calculus for propositional logic with connectives \u00ac and \u2227,\u2228 (both of bounded arity). Then for every <jats:italic>d<\/jats:italic> \u2265 0 and <jats:italic>n<\/jats:italic> \u2265 2, there is a set <jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"gif\" xlink:type=\"simple\" xlink:href=\"S0022481200020235_inline1\"\/> of depth <jats:italic>d<\/jats:italic> sequents of total size <jats:italic>O<\/jats:italic>(<jats:italic>n<\/jats:italic><jats:sup>3+<jats:italic>d<\/jats:italic><\/jats:sup>) which are refutable in LK by depth <jats:italic>d<\/jats:italic> + 1 proof of size exp(<jats:italic>O<\/jats:italic>(log<jats:sup>2<\/jats:sup><jats:italic>n<\/jats:italic>)) but such that every depth <jats:italic>d<\/jats:italic> refutation must have the size at least exp(<jats:italic>n<\/jats:italic><jats:sup>\u03a9(1)<\/jats:sup>). The sets <jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"gif\" xlink:type=\"simple\" xlink:href=\"S0022481200020235_inline1\"\/> express a weaker form of the pigeonhole principle.<\/jats:p>","DOI":"10.2307\/2275250","type":"journal-article","created":{"date-parts":[[2006,5,6]],"date-time":"2006-05-06T22:51:08Z","timestamp":1146955868000},"page":"73-86","source":"Crossref","is-referenced-by-count":88,"title":["Lower bounds to the size of constant-depth propositional proofs"],"prefix":"10.1017","volume":"59","author":[{"given":"Jan","family":"Kraj\u00ed\u010dek","sequence":"first","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2014,3,12]]},"reference":[{"key":"S0022481200020235_ref023","volume-title":"Proof theory","author":"Takeuti","year":"1975"},{"key":"S0022481200020235_ref021","doi-asserted-by":"publisher","DOI":"10.1016\/0003-4843(78)90011-6"},{"key":"S0022481200020235_ref020","first-page":"525","volume-title":"Proceedings of the 4th Hawaii Symposium on system sciences","author":"Spira","year":"1971"},{"key":"S0022481200020235_ref018","first-page":"61","volume-title":"Proceedings of the 15th annual Association for Computing Machinery symposium on the theory of computing","author":"Sipser","year":"1983"},{"key":"S0022481200020235_ref014","first-page":"1063","volume":"54","author":"Kraj\u00ed\u010dek","year":"1989","journal-title":"Prepositional proof systems, the consistency offirst-order theories and the complexity of computations"},{"key":"S0022481200020235_ref010","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(85)90144-6"},{"key":"S0022481200020235_ref008","first-page":"36","volume":"44","author":"Cook","year":"1979","journal-title":"The relative efficiency of prepositional proof systems"},{"key":"S0022481200020235_ref007","first-page":"115","volume-title":"Studies in mathematics and mathematical logic, Part II","author":"Cejtin","year":"1968"},{"key":"S0022481200020235_ref006","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(88)90072-2"},{"key":"S0022481200020235_ref004","first-page":"1161","article-title":"Approximation and small depth Frege proofs","volume":"21","author":"Bellantoni","year":"1992","journal-title":"Society for Industrial and Applied Mathematics Journal of Computing"},{"key":"S0022481200020235_ref024","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1989.63527"},{"key":"S0022481200020235_ref019","first-page":"77","volume-title":"Proceedings of the 19th annual Association for Computing Machinery symposium on the theory of computing","author":"Smolensky","year":"1987"},{"key":"S0022481200020235_ref002","first-page":"1","volume-title":"Feasible mathematics","author":"Ajtai","year":"1990"},{"key":"S0022481200020235_ref009","first-page":"269","volume":"22","author":"Craig","year":"1957","journal-title":"Three uses of the Herbrand-Gentzen theorem relating model theory and proof theory"},{"key":"S0022481200020235_ref016","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0075316"},{"key":"S0022481200020235_ref011","first-page":"143","volume-title":"Advances in Computer Research","volume":"5","author":"Hastad","year":"1989"},{"key":"S0022481200020235_ref013","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-2822-6_11"},{"key":"S0022481200020235_ref015","unstructured":"Kraj\u00ed\u010dek J. , Pudl\u00e1k P. and Woods A. , Exponential lower bound to the size of bounded depth Frege proofs of the pigeonhole principle, submitted."},{"key":"S0022481200020235_ref022","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0079691"},{"key":"S0022481200020235_ref001","first-page":"346","volume-title":"Proceedings of the 29th IEEE annual symposium on foundations of computer science","author":"Ajtai","year":"1988"},{"key":"S0022481200020235_ref012","doi-asserted-by":"publisher","DOI":"10.1090\/S0002-9947-1993-1124169-X"},{"key":"S0022481200020235_ref003","volume-title":"Exponential lower bounds for the pigeonhole principle","author":"Beame","year":"1991"},{"key":"S0022481200020235_ref025","first-page":"1","volume-title":"Proceedings of the 26th IEEE annual symposium on foundations of computer science","author":"Yao","year":"1985"},{"key":"S0022481200020235_ref017","first-page":"1235","volume":"53","author":"Paris","year":"1988","journal-title":"Provability of the pigeonhole principle and the existence of infinitely many primes"},{"key":"S0022481200020235_ref005","doi-asserted-by":"publisher","DOI":"10.1090\/conm\/106\/1057816"}],"container-title":["Journal of Symbolic Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0022481200020235","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,15]],"date-time":"2019-05-15T19:16:33Z","timestamp":1557947793000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0022481200020235\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994,3]]},"references-count":25,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1994,3]]}},"alternative-id":["S0022481200020235"],"URL":"https:\/\/doi.org\/10.2307\/2275250","relation":{},"ISSN":["0022-4812","1943-5886"],"issn-type":[{"value":"0022-4812","type":"print"},{"value":"1943-5886","type":"electronic"}],"subject":[],"published":{"date-parts":[[1994,3]]}}}