{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,10,25]],"date-time":"2023-10-25T10:11:21Z","timestamp":1698228681584},"reference-count":6,"publisher":"Wiley","issue":"2","license":[{"start":{"date-parts":[[2006,11,13]],"date-time":"2006-11-13T00:00:00Z","timestamp":1163376000000},"content-version":"vor","delay-in-days":4699,"URL":"http:\/\/onlinelibrary.wiley.com\/termsAndConditions#vor"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Mathematical Logic Qtrly"],"published-print":{"date-parts":[[1994,1]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We introduce a notion of relative efficiency for axiom systems. Given an axiom system <jats:italic>A<\/jats:italic><jats:sub>\u03b2<\/jats:sub> for a theory <jats:italic>T<\/jats:italic> consistent with <jats:italic>S<\/jats:italic><jats:sup>1<\/jats:sup><jats:sub>2<\/jats:sub>, we show that the problem of deciding whether an axiom system <jats:italic>A<\/jats:italic><jats:sub>\u03b1<\/jats:sub> for the same theory is more efficient than <jats:italic>A<\/jats:italic><jats:sub>\u03b2<\/jats:sub> is II<jats:sub>2<\/jats:sub>\u2010hard. Several possibilities of speed\u2010up of proofs are examined in relation to pairs of axiom systems <jats:italic>A<\/jats:italic><jats:sub>\u03b1<\/jats:sub>, <jats:italic>A<\/jats:italic><jats:sub>\u03b2<\/jats:sub>, with <jats:italic>A<\/jats:italic><jats:sub>\u03b1<\/jats:sub> \u2287 <jats:italic>A<\/jats:italic><jats:sub>\u03b2<\/jats:sub>, both in the case of <jats:italic>A<\/jats:italic><jats:sub>\u03b1<\/jats:sub>, <jats:italic>A<\/jats:italic><jats:sub>\u03b2<\/jats:sub> having the same language, and in the case of the language of <jats:italic>A<\/jats:italic><jats:sub>\u03b1<\/jats:sub> extending that of <jats:italic>A<\/jats:italic><jats:sub>\u03b2<\/jats:sub>: in the latter case, letting Pr<jats:sub>\u03b1<\/jats:sub>, Pr<jats:sub>\u03b2<\/jats:sub> denote the theories axiomatized by <jats:italic>A<\/jats:italic><jats:sub>\u03b1<\/jats:sub>, <jats:italic>A<\/jats:italic><jats:sub>\u03b2<\/jats:sub>, respectively, and assuming Pr<jats:sub>\u03b1<\/jats:sub> to be a conservative extension of Pr<jats:sub>\u03b2<\/jats:sub>, we show that if <jats:italic>A<\/jats:italic><jats:sub>\u03b1<\/jats:sub> \u2014 <jats:italic>A<\/jats:italic><jats:sub>\u03b2<\/jats:sub> contains no nonlogical axioms, then <jats:italic>A<\/jats:italic><jats:sub>\u03b1<\/jats:sub> can only be a linear speed\u2010up of <jats:italic>A<\/jats:italic><jats:sub>\u03b2<\/jats:sub>; otherwise, given any recursive function <jats:italic>g<\/jats:italic> and any <jats:italic>A<\/jats:italic><jats:sub>\u03b2<\/jats:sub>, there exists a finite extension <jats:italic>A<\/jats:italic><jats:sub>\u03b1<\/jats:sub> of <jats:italic>A<\/jats:italic><jats:sub>\u03b2<\/jats:sub> such that <jats:italic>A<\/jats:italic><jats:sub>\u03b1<\/jats:sub> is a speed\u2010up of <jats:italic>A<\/jats:italic><jats:sub>\u03b2<\/jats:sub> with respect to <jats:italic>g<\/jats:italic>.<\/jats:p><jats:p><jats:bold>Mathematics Subject Classification:<\/jats:bold> 03F20, 03F30.<\/jats:p>","DOI":"10.1002\/malq.19940400211","type":"journal-article","created":{"date-parts":[[2007,5,26]],"date-time":"2007-05-26T17:20:36Z","timestamp":1180200036000},"page":"261-272","source":"Crossref","is-referenced-by-count":1,"title":["A Note on Relative Efficiency of Axiom Systems"],"prefix":"10.1002","volume":"40","author":[{"given":"Sandra","family":"Fontani","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Franco","family":"Montagna","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrea","family":"Sorbi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"311","published-online":{"date-parts":[[2006,11,13]]},"reference":[{"key":"e_1_2_1_2_2","unstructured":"Buss S. R. Bounded Arithmetic: Studies in Proof Theory. Bibliopolis Naples1986."},{"key":"e_1_2_1_3_2","volume-title":"Computability and Unsolvability","author":"Davis M.","year":"1983"},{"key":"e_1_2_1_4_2","doi-asserted-by":"publisher","DOI":"10.1090\/S0002-9904-1971-12696-4"},{"key":"e_1_2_1_5_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-22156-3"},{"key":"e_1_2_1_6_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(08)70462-2"},{"key":"e_1_2_1_7_2","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(87)90066-2"}],"container-title":["Mathematical Logic Quarterly"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.wiley.com\/onlinelibrary\/tdm\/v1\/articles\/10.1002%2Fmalq.19940400211","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/onlinelibrary.wiley.com\/doi\/pdf\/10.1002\/malq.19940400211","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,10,24]],"date-time":"2023-10-24T02:44:53Z","timestamp":1698115493000},"score":1,"resource":{"primary":{"URL":"https:\/\/onlinelibrary.wiley.com\/doi\/10.1002\/malq.19940400211"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994,1]]},"references-count":6,"journal-issue":{"issue":"2","published-print":{"date-parts":[[1994,1]]}},"alternative-id":["10.1002\/malq.19940400211"],"URL":"https:\/\/doi.org\/10.1002\/malq.19940400211","archive":["Portico"],"relation":{},"ISSN":["0942-5616","1521-3870"],"issn-type":[{"value":"0942-5616","type":"print"},{"value":"1521-3870","type":"electronic"}],"subject":[],"published":{"date-parts":[[1994,1]]}}}