{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,9,15]],"date-time":"2023-09-15T01:46:11Z","timestamp":1694742371202},"reference-count":25,"publisher":"Cambridge University Press (CUP)","issue":"2","license":[{"start":{"date-parts":[[2014,3,12]],"date-time":"2014-03-12T00:00:00Z","timestamp":1394582400000},"content-version":"unspecified","delay-in-days":1380,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. symb. log."],"published-print":{"date-parts":[[2010,6]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Let <jats:italic>L<\/jats:italic> be a first-order language and \u03a6 and \u03a8 two <jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"gif\" xlink:type=\"simple\" xlink:href=\"S0022481200002772_inline2\" \/><jats:italic>L<\/jats:italic>-sentences that cannot be satisfied simultaneously in any finite <jats:italic>L<\/jats:italic>-structure. Then obviously the following principle Chain<jats:sub><jats:italic>L<\/jats:italic>,\u03a6,\u03a8<\/jats:sub>(<jats:italic>n, m<\/jats:italic>) holds: For any chain of finite <jats:italic>L<\/jats:italic>-structures <jats:italic>C<\/jats:italic><jats:sub>1<\/jats:sub>, \u2026, <jats:italic>C<jats:sub>m<\/jats:sub><\/jats:italic> with the universe [<jats:italic>n<\/jats:italic>] one of the following conditions must fail:<\/jats:p><jats:p><jats:disp-formula><jats:graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" orientation=\"portrait\" mime-subtype=\"gif\" mimetype=\"image\" position=\"float\" xlink:type=\"simple\" xlink:href=\"S0022481200002772_eqnU1\" \/><\/jats:disp-formula><\/jats:p><jats:p>For each fixed <jats:italic>L<\/jats:italic> and parameters <jats:italic>n, m<\/jats:italic> the principle <jats:italic>Chain<\/jats:italic><jats:sub><jats:italic>L<\/jats:italic>,\u03a6,\u03a8<\/jats:sub>(<jats:italic>n,m<\/jats:italic>) can be encoded into a propositional DNF formula of size polynomial in <jats:italic>n, m<\/jats:italic>.<\/jats:p><jats:p>For any language <jats:italic>L<\/jats:italic> containing only constants and unary predicates we show that there is a constant <jats:italic>C<jats:sub>L<\/jats:sub><\/jats:italic> such that the following holds: If a constant depth Frege system in DeMorgan language proves <jats:italic>Chain<\/jats:italic><jats:sub><jats:italic>L<\/jats:italic>,\u03a6,\u03a8<\/jats:sub>(<jats:italic>n, c<jats:sub>L<\/jats:sub> . n<\/jats:italic>) by a size <jats:italic>s<\/jats:italic> proof then the class of finite <jats:italic>L<\/jats:italic>-structures with universe [<jats:italic>n<\/jats:italic>] satisfying \u03a6 can be separated from the class of those <jats:italic>L<\/jats:italic>-structures on [<jats:italic>n<\/jats:italic>] satisfying \u03c8 by a depth 3 formula of size 2<jats:sup>log(<jats:italic>S<\/jats:italic>)<jats:sup><jats:italic>O<\/jats:italic>(1)<\/jats:sup><\/jats:sup> and with bottom fan-in log(<jats:italic>S<\/jats:italic>)<jats:sup><jats:italic>O<\/jats:italic>(1)<\/jats:sup>.<\/jats:p>","DOI":"10.2178\/jsl\/1268917504","type":"journal-article","created":{"date-parts":[[2010,3,18]],"date-time":"2010-03-18T09:05:57Z","timestamp":1268903157000},"page":"774-784","source":"Crossref","is-referenced-by-count":4,"title":["A form of feasible interpolation for constant depth Frege systems"],"prefix":"10.1017","volume":"75","author":[{"given":"Jan","family":"Kraj\u00ed\u010dek","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2014,3,12]]},"reference":[{"key":"S0022481200002772_ref024","volume-title":"The provably total search problems of bounded arithmetic","author":"Skelley","year":"2008"},{"key":"S0022481200002772_ref021","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(98)80023-2"},{"key":"S0022481200002772_ref018","first-page":"1235","volume":"53","author":"Paris","year":"1988","journal-title":"Provability of the pigeonhole principle and the existence of infinitely many primes"},{"key":"S0022481200002772_ref016","doi-asserted-by":"publisher","DOI":"10.1002\/rsa.3240070103"},{"key":"S0022481200002772_ref015","first-page":"210","volume-title":"Logic and Computational Complexity (Proceedings of the Meeting held in Indianapolis, October 1994)","volume":"960","author":"Kraj\u00ed\u010dek","year":"1995"},{"key":"S0022481200002772_ref012","first-page":"457","volume":"62","author":"Kraj\u00ed\u010dek","year":"1997","journal-title":"Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic"},{"key":"S0022481200002772_ref011","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511529948"},{"key":"S0022481200002772_ref007","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511676277"},{"key":"S0022481200002772_ref005","volume-title":"Bounded Arithmetic","author":"Buss","year":"1986"},{"key":"S0022481200002772_ref004","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539798353230"},{"key":"S0022481200002772_ref003","first-page":"708","author":"Bonet","year":"1997","journal-title":"Lower bounds for cutting planes proofs with small coefficients"},{"key":"S0022481200002772_ref002","doi-asserted-by":"publisher","DOI":"10.1007\/s00037-004-0183-5"},{"key":"S0022481200002772_ref001","first-page":"346","volume-title":"Proceedings of the IEEE Annual Symposium on Foundations of Computer Science (FOCS)","author":"Ajtai","year":"1988"},{"key":"S0022481200002772_ref010","first-page":"73","volume":"59","author":"Kraj\u00ed\u010dek","year":"1994","journal-title":"Lower bounds to the size of constant-depth prepositional proofs"},{"key":"S0022481200002772_ref019","doi-asserted-by":"publisher","DOI":"10.1007\/BF01200117"},{"key":"S0022481200002772_ref023","doi-asserted-by":"publisher","DOI":"10.1070\/IM1995v059n01ABEH000009"},{"key":"S0022481200002772_ref022","first-page":"179","volume-title":"Proof Complexity and Feasible Arithmetic","volume":"39","author":"Pudl\u00e1k","year":"1998"},{"key":"S0022481200002772_ref017","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0075316"},{"key":"S0022481200002772_ref025","first-page":"1","volume-title":"Proceedings of the IEEE Annual Symposium on Foundations of Computer Science (FOCS)","author":"Yao","year":"1985"},{"key":"S0022481200002772_ref020","first-page":"981","author":"Pudl\u00e1k","year":"1997","journal-title":"Lower bounds for resolution and cutting plane proofs and monotone computations"},{"key":"S0022481200002772_ref014","first-page":"227","volume":"73","author":"Kraj\u00ed\u010dek","year":"2008","journal-title":"An exponential lower bound for a constraint propagation proof system based on ordered binary decision diagrams"},{"key":"S0022481200002772_ref009","first-page":"143","volume-title":"Randomness and Computation","volume":"5","author":"Hastad","year":"1989"},{"key":"S0022481200002772_ref006","first-page":"916","volume":"52","author":"Buss","year":"1987","journal-title":"The prepositional pigeonhole principle has polynomial size Frege proofs"},{"key":"S0022481200002772_ref013","first-page":"1582","volume":"63","author":"Kraj\u00ed\u010dek","year":"1998","journal-title":"Discretely ordered modules as a first-order extension of the cutting planes proof system"},{"key":"S0022481200002772_ref008","first-page":"36","volume":"44","author":"Cook","year":"1979","journal-title":"The relative efficiency of prepositional proof systems"}],"container-title":["The Journal of Symbolic Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0022481200002772","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,28]],"date-time":"2019-04-28T15:38:06Z","timestamp":1556465886000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0022481200002772\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,6]]},"references-count":25,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2010,6]]}},"alternative-id":["S0022481200002772"],"URL":"https:\/\/doi.org\/10.2178\/jsl\/1268917504","relation":{},"ISSN":["0022-4812","1943-5886"],"issn-type":[{"value":"0022-4812","type":"print"},{"value":"1943-5886","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010,6]]}}}