{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,2]],"date-time":"2022-04-02T12:15:53Z","timestamp":1648901753115},"reference-count":10,"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":4394,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. symb. log."],"published-print":{"date-parts":[[2002,3]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We consider equational theories for functions denned via recursion involving equations between closed terms with natural rules based on recursive definitions of the function symbols. We show that consistency of such equational theories can be proved in the weak fragment of arithmetic <jats:italic>S<\/jats:italic><jats:sub arrange=\"stack\">2<\/jats:sub><jats:sup arrange=\"stack\">1<\/jats:sup>. In particular this solves an open problem formulated by Takeuti (c.f. [5, p.5 problem 9.]).<\/jats:p>","DOI":"10.2178\/jsl\/1190150044","type":"journal-article","created":{"date-parts":[[2007,12,13]],"date-time":"2007-12-13T19:12:10Z","timestamp":1197573130000},"page":"279-296","source":"Crossref","is-referenced-by-count":2,"title":["Proving consistency of equational theories in bounded arithmetic"],"prefix":"10.1017","volume":"67","author":[{"given":"Arnold","family":"Beckmann\u2020","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2014,3,12]]},"reference":[{"key":"S0022481200009993_ref001","doi-asserted-by":"publisher","DOI":"10.1007\/s001530050054"},{"key":"S0022481200009993_ref009","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)00135-6"},{"key":"S0022481200009993_ref006","doi-asserted-by":"publisher","DOI":"10.1145\/800116.803756"},{"key":"S0022481200009993_ref005","first-page":"1","volume-title":"Arithmetic, proof theory, and computational complexity. Papers from the conference held in Prague, July 2\u20135, 1991","author":"Clote","year":"1993"},{"key":"S0022481200009993_ref002","volume-title":"Studies in proof theory. Lecture notes, 3","author":"Buss","year":"1986"},{"key":"S0022481200009993_ref003","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(94)00049-9"},{"key":"S0022481200009993_ref004","doi-asserted-by":"publisher","DOI":"10.1016\/S0168-0072(96)00015-2"},{"key":"S0022481200009993_ref007","first-page":"243","volume-title":"Handbook of theoretical computer science. Volume B","author":"Dershowitz","year":"1990"},{"key":"S0022481200009993_ref008","doi-asserted-by":"publisher","DOI":"10.4064\/fm-136-2-85-89"},{"key":"S0022481200009993_ref010","first-page":"261","volume-title":"Annals of Pure and Applied Logic","author":"Wilkie","year":"1987"}],"container-title":["Journal of Symbolic Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0022481200009993","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,7]],"date-time":"2019-05-07T01:34:55Z","timestamp":1557192895000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0022481200009993\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002,3]]},"references-count":10,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2002,3]]}},"alternative-id":["S0022481200009993"],"URL":"https:\/\/doi.org\/10.2178\/jsl\/1190150044","relation":{},"ISSN":["0022-4812","1943-5886"],"issn-type":[{"value":"0022-4812","type":"print"},{"value":"1943-5886","type":"electronic"}],"subject":[],"published":{"date-parts":[[2002,3]]}}}