{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,1]],"date-time":"2026-07-01T21:30:41Z","timestamp":1782941441550,"version":"3.54.5"},"reference-count":19,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2006,10,1]],"date-time":"2006-10-01T00:00:00Z","timestamp":1159660800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2006,10]]},"abstract":"<jats:p>The<jats:italic>replacement<\/jats:italic>(or<jats:italic>collection<\/jats:italic>or<jats:italic>choice<\/jats:italic>) axiom scheme BB(\u0393) asserts bounded quantifier exchange as follows: \u2200<jats:italic>i<\/jats:italic>&lt; |<jats:italic>a<\/jats:italic>| \u2203<jats:italic>x<\/jats:italic>&lt;<jats:italic>a<\/jats:italic>\u03d5(<jats:italic>i<\/jats:italic>,<jats:italic>x<\/jats:italic>) \u2192 \u2203<jats:italic>w<\/jats:italic>\u2200<jats:italic>i<\/jats:italic>&lt; |<jats:italic>a<\/jats:italic>|\u03d5(<jats:italic>i<\/jats:italic>,[<jats:italic>w<\/jats:italic>]<jats:sub>i<\/jats:sub>), for \u03d5 in the class \u0393 of formulas. The theory<jats:italic>S<\/jats:italic><jats:sup>1<\/jats:sup><jats:sub>2<\/jats:sub>proves the scheme BB(\u03a3<jats:sup><jats:italic>b<\/jats:italic><\/jats:sup><jats:sub>1<\/jats:sub>), and thus in<jats:italic>S<\/jats:italic><jats:sup>1<\/jats:sup><jats:sub>2<\/jats:sub>every \u03a3<jats:sup><jats:italic>b<\/jats:italic><\/jats:sup><jats:sub>1<\/jats:sub>formula is equivalent to a strict \u03a3<jats:sup><jats:italic>b<\/jats:italic><\/jats:sup><jats:sub>1<\/jats:sub>formula (in which all non-sharply-bounded quantifiers are in front). Here we prove (sometimes subject to an assumption) that certain theories weaker than<jats:italic>S<\/jats:italic><jats:sup>1<\/jats:sup><jats:sub>2<\/jats:sub>do not prove either BB(\u03a3<jats:sup><jats:italic>b<\/jats:italic><\/jats:sup><jats:sub>1<\/jats:sub>) or BB(\u03a3<jats:sup><jats:italic>b<\/jats:italic><\/jats:sup><jats:sub>0<\/jats:sub>). We show (unconditionally) that<jats:italic>V<\/jats:italic><jats:sup>0<\/jats:sup>does not prove BB(\u03a3<jats:sup><jats:italic>b<\/jats:italic><\/jats:sup><jats:sub>0<\/jats:sub>), where V<jats:sup>0<\/jats:sup>(essentially I\u03a3<jats:sup>1,<jats:italic>b<\/jats:italic><\/jats:sup><jats:sub>0<\/jats:sub>) is the two-sorted theory associated with the complexity class AC<jats:sup>0<\/jats:sup>. We show that PV does not prove BB(\u03a3<jats:sup><jats:italic>b<\/jats:italic><\/jats:sup><jats:sub>0<\/jats:sub>), assuming that integer factoring is not possible in probabilistic polynomial time. Johannsen and Pollett introduced the theory<jats:italic>C<\/jats:italic><jats:sup>0<\/jats:sup><jats:sub>2<\/jats:sub>associated with the complexity class TC<jats:sup>0<\/jats:sup>, and later introduced an apparently weaker theory \u0394<jats:sup><jats:italic>b<\/jats:italic><\/jats:sup><jats:sub>1<\/jats:sub>\u2212 CR for the same class. We use our methods to show that \u0394<jats:sup><jats:italic>b<\/jats:italic><\/jats:sup><jats:sub>1<\/jats:sub>\u2212 CR is indeed weaker than<jats:italic>C<\/jats:italic><jats:sup>0<\/jats:sup><jats:sub>2<\/jats:sub>, assuming that RSA is secure against probabilistic polynomial time attack.Our main tool is the KPT witnessing theorem.<\/jats:p>","DOI":"10.1145\/1183278.1183283","type":"journal-article","created":{"date-parts":[[2007,1,16]],"date-time":"2007-01-16T19:38:29Z","timestamp":1168976309000},"page":"749-764","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":11,"title":["The strength of replacement in weak arithmetic"],"prefix":"10.1145","volume":"7","author":[{"given":"Stephen","family":"Cook","sequence":"first","affiliation":[{"name":"Department of Computer Science, University of Toronto, Toronto, Ont., Canada"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Neil","family":"Thapen","sequence":"additional","affiliation":[{"name":"Department of Computer Science, University of Toronto, Toronto, Ont., Canada"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2006,10]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0168-0072(83)90038-6","article-title":"\u03a311-formulae on finite structures","volume":"24","author":"Ajtai M.","year":"1983","journal-title":"Ann. Pure Appl. Logic"},{"key":"e_1_2_1_2_1","unstructured":"Buss S. 1986. Bounded Arithmetic. Bibliopolis. Buss S. 1986. Bounded Arithmetic. Bibliopolis."},{"key":"e_1_2_1_3_1","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0168-0072(94)00057-A","article-title":"Relating the bounded arithmetic and polynomial time hierarchies","volume":"75","author":"Buss S.","year":"1995","journal-title":"Ann. Pure Appl. Logic"},{"key":"e_1_2_1_4_1","volume-title":"Proceedings of the 7th Annual ACM Symposium on Theory of Computing. ACM","author":"Cook S.","year":"1975"},{"key":"e_1_2_1_5_1","doi-asserted-by":"crossref","first-page":"73","DOI":"10.1090\/dimacs\/039\/05","article-title":"Relating the provable collapse of P to NC1 and the power of logical theories","volume":"39","author":"Cook S.","year":"1998","journal-title":"DIMACS Ser. Discr. Math. Theoret. Comput. Sci."},{"key":"e_1_2_1_6_1","unstructured":"Cook S. 2002. CSC 2429 Course Notes: Proof Complexity and Bounded Arithmetic. Available from the web at www.cs.toronto.edu\/~sacook\/csc2429h\/. Cook S. 2002. CSC 2429 Course Notes: Proof Complexity and Bounded Arithmetic. Available from the web at www.cs.toronto.edu\/~sacook\/csc2429h\/."},{"key":"e_1_2_1_7_1","volume-title":"Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science. IEEE Computer Society Press","author":"Cook S.","year":"2004"},{"key":"e_1_2_1_8_1","doi-asserted-by":"crossref","first-page":"13","DOI":"10.1007\/BF01744431","article-title":"Parity, circuits and the polynomial-time hierarchy","volume":"17","author":"Furst M.","year":"1984","journal-title":"Math. Syst. Theory"},{"key":"e_1_2_1_9_1","volume-title":"Proceedings of the 13th IEEE Symposium on Logic in Computer Science. IEEE Computer Society Press","author":"Johannsen J."},{"key":"e_1_2_1_10_1","doi-asserted-by":"crossref","unstructured":"Johannsen J. and Pollett C. 2000. On the \u0394b1-bit-comprehension rule. In Logic Colloquium 98 S. Buss P. H\u00e1jek and P. Pudl\u00e1k Eds. ASL Lecture Notes in Logic. 262--279. Johannsen J. and Pollett C. 2000. On the \u0394b1-bit-comprehension rule. In Logic Colloquium 98 S. Buss P. H\u00e1jek and P. Pudl\u00e1k Eds. ASL Lecture Notes in Logic. 262--279.","DOI":"10.1017\/9781316756140.019"},{"key":"e_1_2_1_11_1","doi-asserted-by":"crossref","unstructured":"Kraj\u00ed\u010dek J. 1995. Bounded Arithmetic Propositional Logic and Computational Complexity. Cambridge University Press Cambridge MA. Kraj\u00ed\u010dek J. 1995. Bounded Arithmetic Propositional Logic and Computational Complexity. Cambridge University Press Cambridge MA.","DOI":"10.1017\/CBO9780511529948"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1997.2674"},{"key":"e_1_2_1_13_1","doi-asserted-by":"crossref","first-page":"143","DOI":"10.1016\/0168-0072(91)90043-L","article-title":"Bounded arithmetic and the polynomial hierarchy","volume":"52","author":"Kraj\u00ed\u010dek J.","year":"1991","journal-title":"Ann. Pure Appl. Logic"},{"key":"e_1_2_1_14_1","unstructured":"Nguyen P. 2004. VTC0: A Second-Order Theory for TC0. MSc Thesis Department of Computer Science University of Toronto Toronto Ont. Canada. Nguyen P. 2004. VTC0: A Second-Order Theory for TC0. MSc Thesis Department of Computer Science University of Toronto Toronto Ont. Canada."},{"key":"e_1_2_1_15_1","doi-asserted-by":"crossref","first-page":"1235","DOI":"10.1017\/S0022481200028061","article-title":"Provability of the pigeonhole principle and the existence of infinitely many primes","volume":"53","author":"Paris J.","year":"1988","journal-title":"J. Symb. Logic"},{"key":"e_1_2_1_17_1","doi-asserted-by":"crossref","unstructured":"Razborov A. A. 1993. An equivalence between second order bounded domain bounded arithmetic and first-order bounded arithmetic. In Arithmetic Proof Theory and Computational Complexity P. Clote and J. Krajicek Eds. Oxford University Press 247--77. Razborov A. A. 1993. An equivalence between second order bounded domain bounded arithmetic and first-order bounded arithmetic. In Arithmetic Proof Theory and Computational Complexity P. Clote and J. Krajicek Eds. Oxford University Press 247--77.","DOI":"10.1093\/oso\/9780198536901.003.0012"},{"key":"e_1_2_1_18_1","doi-asserted-by":"crossref","unstructured":"Takeuti G. 1993. RSUV isomorphism. In Arithmetic Proof Theory and Computational Complexity P. Clote and J. Krajicek Eds. Oxford University Press 364--86. Takeuti G. 1993. RSUV isomorphism. In Arithmetic Proof Theory and Computational Complexity P. Clote and J. Krajicek Eds. Oxford University Press 364--86.","DOI":"10.1093\/oso\/9780198536901.003.0016"},{"key":"e_1_2_1_19_1","doi-asserted-by":"crossref","first-page":"175","DOI":"10.1016\/S0168-0072(02)00038-6","article-title":"A model-theoretic characterization of the weak pigeonhole principle","volume":"118","author":"Thapen N.","year":"2002","journal-title":"Ann. Pure Appl. Logic"},{"key":"e_1_2_1_20_1","doi-asserted-by":"crossref","first-page":"942","DOI":"10.2307\/2275794","article-title":"Notes on polynomially bounded arithmetic","volume":"61","author":"Zambella D.","year":"1996","journal-title":"J. Symb. Logic"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1183278.1183283","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1183278.1183283","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T15:06:37Z","timestamp":1750259197000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1183278.1183283"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,10]]},"references-count":19,"aliases":["10.1145\/1166109.1166114"],"journal-issue":{"issue":"4","published-print":{"date-parts":[[2006,10]]}},"alternative-id":["10.1145\/1183278.1183283"],"URL":"https:\/\/doi.org\/10.1145\/1183278.1183283","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"value":"1529-3785","type":"print"},{"value":"1557-945X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006,10]]},"assertion":[{"value":"2006-10-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}