{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,27]],"date-time":"2025-02-27T19:10:19Z","timestamp":1740683419696,"version":"3.38.0"},"reference-count":10,"publisher":"Wiley","issue":"6","license":[{"start":{"date-parts":[[2010,11,9]],"date-time":"2010-11-09T00:00:00Z","timestamp":1289260800000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/onlinelibrary.wiley.com\/termsAndConditions#vor"}],"funder":[{"name":"NSF","award":["DMS-0700533"],"award-info":[{"award-number":["DMS-0700533"]}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Mathematical Logic Qtrly"],"published-print":{"date-parts":[[2010,12]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We refine the constructions of Ferrante\u2010Rackoff and Solovay on iterated definitions in first\u2010order logic and their expressibility with polynomial size formulas. These constructions introduce additional quantifiers; however, we show that these extra quantifiers range over only finite sets and can be eliminated. We prove optimal upper and lower bounds on the quantifier complexity of polynomial size formulas obtained from the iterated definitions. In the quantifier\u2010free case and in the case of purely existential or universal quantifiers, we show that \u03a9(<jats:italic>n<\/jats:italic>\/log<jats:italic>n<\/jats:italic>) quantifiers are necessary and sufficient. The last lower bounds are obtained with the aid of the Yao\u2010H\u00e5stad switching lemma (\u00a9 2010 WILEY\u2010VCH Verlag GmbH &amp; Co. KGaA, Weinheim)<\/jats:p>","DOI":"10.1002\/malq.200910111","type":"journal-article","created":{"date-parts":[[2010,11,9]],"date-time":"2010-11-09T08:34:48Z","timestamp":1289291688000},"page":"573-590","source":"Crossref","is-referenced-by-count":1,"title":["The quantifier complexity of polynomial\u2010size iterated definitions in first\u2010order logic"],"prefix":"10.1002","volume":"56","author":[{"given":"Samuel R.","family":"Buss","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alan S.","family":"Johnson","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"311","published-online":{"date-parts":[[2010,11,9]]},"reference":[{"key":"e_1_2_1_2_2","unstructured":"P.Beame A switching lemma primer (Typeset manuscript unpublished 1994)."},{"key":"e_1_2_1_3_2","doi-asserted-by":"crossref","unstructured":"J.Ferrante andC. W.Rackoff The Computational Complexity of Logical Theories. Lecture Notes in Mathematics 3718 (Springer Verlag 1979).","DOI":"10.1007\/BFb0062837"},{"key":"e_1_2_1_4_2","unstructured":"M. J.Fischer andM. O.Rabin Super\u2010exponential complexity of Presburger Arithmetic. In: Proc. SIAM\u2010AMS Symposium in Applied Mathematics vol. 7 pp. 27\u201341 (Massachusetts Institute of Technology 1974)."},{"key":"e_1_2_1_5_2","unstructured":"J.H\u00e4stad Computational Limitations for Small\u2010depth Circuits (MIT Press 1987)."},{"key":"e_1_2_1_6_2","doi-asserted-by":"crossref","unstructured":"P.Pudl\u00e4k The lengths of proofs. In: Handbook of Proof Theory (S. R. Buss ed.) pp. 547\u2013637 (Elsevier North\u2010Holland 1998).","DOI":"10.1016\/S0049-237X(98)80023-2"},{"key":"e_1_2_1_7_2","doi-asserted-by":"crossref","unstructured":"P.Pudl\u00e4k On the lengths of proofs of finitistic consistency statements in first order theories. In: Logic Colloquium '84 pp. 165\u2013196 (North\u2010Holland 1986).","DOI":"10.1016\/S0049-237X(08)70462-2"},{"key":"e_1_2_1_8_2","doi-asserted-by":"crossref","unstructured":"P.Pudl\u00e4k Improved bounds to the lengths of proofs of finitistic consistency statements. In: Logic and Combinatorics Contemporary Mathematics vol. 65 (S. G. Simpson ed.) pp. 309\u2013331 (American Mathematical Society 1987).","DOI":"10.1090\/conm\/065\/891256"},{"key":"e_1_2_1_9_2","doi-asserted-by":"crossref","unstructured":"L. J.Stockmeyer andA. R.Meyer Word problems requiring exponential time (Preliminary Report). In: Proc. of the Fifth Annual ACM Symposium on Theory of Computing (STOC'73) pp. 1\u20139 (1973).","DOI":"10.1145\/800125.804029"},{"key":"e_1_2_1_10_2","doi-asserted-by":"crossref","unstructured":"A. S.Troelstra andH.Schwichtenberg Basic Proof Theory. Tracts in Theoretical Computer Science 1143 2nd ed. (Cambridge University Press 2000).","DOI":"10.1017\/CBO9781139168717"},{"key":"e_1_2_1_11_2","doi-asserted-by":"crossref","unstructured":"A. C.\u2010C.Yao Separating the polynomial time hierarchy by oracles. In: Proceedings of the 26th Annual Symposium on Foundations of Computer Science (FOCS'85) pp. 1\u201310 (IEEE Computer Society 1985).","DOI":"10.1109\/SFCS.1985.49"}],"container-title":["Mathematical Logic Quarterly"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.wiley.com\/onlinelibrary\/tdm\/v1\/articles\/10.1002%2Fmalq.200910111","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.wiley.com\/onlinelibrary\/tdm\/v1\/articles\/10.1002%2Fmalq.200910111","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/onlinelibrary.wiley.com\/doi\/pdf\/10.1002\/malq.200910111","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,27]],"date-time":"2025-02-27T17:59:45Z","timestamp":1740679185000},"score":1,"resource":{"primary":{"URL":"https:\/\/onlinelibrary.wiley.com\/doi\/10.1002\/malq.200910111"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,11,9]]},"references-count":10,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2010,12]]}},"alternative-id":["10.1002\/malq.200910111"],"URL":"https:\/\/doi.org\/10.1002\/malq.200910111","archive":["Portico"],"relation":{},"ISSN":["0942-5616","1521-3870"],"issn-type":[{"type":"print","value":"0942-5616"},{"type":"electronic","value":"1521-3870"}],"subject":[],"published":{"date-parts":[[2010,11,9]]}}}