{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,30]],"date-time":"2025-07-30T15:34:53Z","timestamp":1753889693552,"version":"3.41.2"},"reference-count":19,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2012,8,10]],"date-time":"2012-08-10T00:00:00Z","timestamp":1344556800000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/nonexclusive-distrib\/1.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>One of the central open questions in bounded arithmetic is whether Buss'\nhierarchy of theories of bounded arithmetic collapses or not. In this paper, we\nreformulate Buss' theories using free logic and conjecture that such theories\nare easier to handle. To show this, we first prove that Buss' theories prove\nconsistencies of induction-free fragments of our theories whose formulae have\nbounded complexity. Next, we prove that although our theories are based on an\napparently weaker logic, we can interpret theories in Buss' hierarchy by our\ntheories using a simple translation. Finally, we investigate finitistic G\\\"odel\nsentences in our systems in the hope of proving that a theory in a lower level\nof Buss' hierarchy cannot prove consistency of induction-free fragments of our\ntheories whose formulae have higher complexity.<\/jats:p>","DOI":"10.2168\/lmcs-8(3:7)2012","type":"journal-article","created":{"date-parts":[[2013,11,29]],"date-time":"2013-11-29T08:17:46Z","timestamp":1385713066000},"source":"Crossref","is-referenced-by-count":0,"title":["Bounded Arithmetic in Free Logic"],"prefix":"10.46298","volume":"Volume 8, Issue 3","author":[{"given":"Yoriyuki","family":"Yamagata","sequence":"first","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2012,8,10]]},"reference":[{"key":"10.2168\/LMCS-8(3:7)2012_Adamowicz2002","first-page":"1","volume":"2","author":"Z Adamowicz","year":"2002","journal-title":"Fundamenta Mathematicae"},{"issue":"3","key":"10.2168\/LMCS-8(3:7)2012_Adamowicz2011","doi-asserted-by":"crossref","first-page":"191","DOI":"10.4064\/fm212-3-1","volume":"212","author":"Z Adamowicz and K. Zdanowski","year":"2011","journal-title":"Fundamenta Mathematicae"},{"issue":"6","key":"10.2168\/LMCS-8(3:7)2012_Adamowicz2001","doi-asserted-by":"crossref","first-page":"399","DOI":"10.1007\/s001530000072","volume":"40","author":"Zofia Adamowicz and Pawel Zbierski","year":"2001","journal-title":"Archive for Mathematical Logic"},{"issue":"1","key":"10.2168\/LMCS-8(3:7)2012_Beckmann2002","doi-asserted-by":"crossref","first-page":"279","DOI":"10.2178\/jsl\/1190150044","volume":"67","author":"Arnold Beckmann","year":"2002","journal-title":"Journal of Symbolic Logic"},{"key":"10.2168\/LMCS-8(3:7)2012_Buss:Book","unstructured":"Samuel R. Buss.Bounded arithmetic. Bibliopolis, 1986."},{"key":"10.2168\/LMCS-8(3:7)2012_BussUnprovability","doi-asserted-by":"crossref","first-page":"221","DOI":"10.1016\/0168-0072(94)00049-9","volume":"74","author":"Samuel R. Buss and Aleksandar Ignjatovic","year":"1995","journal-title":"Annals of pure and applied logic"},{"key":"10.2168\/LMCS-8(3:7)2012_Hajek1998","unstructured":"Petr H\u00e1jek and Pavel Pudl\u00e1k.Metamathematics of first-order arithmetic. Springer-Verlag, 1998."},{"issue":"1-2","key":"10.2168\/LMCS-8(3:7)2012_Krajicek1991","doi-asserted-by":"crossref","first-page":"143","DOI":"10.1016\/0168-0072(91)90043-L","volume":"52","author":"J Kraj\u00edcek, Pavel Pudl\u00e1k, and Gaisi Take","year":"1991","journal-title":"Annals of pure and applied logic"},{"key":"10.2168\/LMCS-8(3:7)2012_Krajicek1992","first-page":"107","volume":"6","author":"J Kraj\u00edcek and Gaisi Takeuti","year":"1992","journal-title":"Annals of mathematics and artificial intelligence 1992"},{"key":"10.2168\/LMCS-8(3:7)2012_Leivant2001","doi-asserted-by":"crossref","unstructured":"Daniel Leivant. Termination proofs and complexity certification. In Naoki Kobayashi and Benjamin C. Pierce, editors,Theoretical Aspects of Computer Software, volume 2215 ofLecture notes in computer science, pages 183-200. Springer Berlin \/ Heidelberg, 2001.","DOI":"10.1007\/3-540-45500-0_9"},{"key":"10.2168\/LMCS-8(3:7)2012_FreeLogic","unstructured":"John Nolt. Free logic (Stanford encyclopedia of philosophy). http:\/\/plato.stanford.edu\/entries\/logic-free\/, April 2010."},{"issue":"3","key":"10.2168\/LMCS-8(3:7)2012_Parikh1971","doi-asserted-by":"crossref","first-page":"494","DOI":"10.2307\/2269958","volume":"36","author":"R. Parikh","year":"1971","journal-title":"Journal of Symbolic Logic"},{"issue":"2","key":"10.2168\/LMCS-8(3:7)2012_Pudlak1985","doi-asserted-by":"crossref","first-page":"423","DOI":"10.2307\/2274231","volume":"50","author":"P. Pudl\u00e1k","year":"1985","journal-title":"The Journal of Symbolic Logic"},{"key":"10.2168\/LMCS-8(3:7)2012_PudlakNote","doi-asserted-by":"crossref","first-page":"85","DOI":"10.4064\/fm-136-2-85-89","volume":"136","author":"P. Pudl\u00e1k","year":"1990","journal-title":"Fundamenta mathematicae"},{"key":"10.2168\/LMCS-8(3:7)2012_Scott1979","doi-asserted-by":"crossref","unstructured":"Dana Scott. Identity and existence in intuitionistic logic. In Michael Fourman, Christopher Mulvey, and Dana Scott, editors,Applications of sheaves, volume 753 ofLecture notes in mathematics, pages 660-696. Springer Berlin \/ Heidelberg, 1979.","DOI":"10.1007\/BFb0061839"},{"key":"10.2168\/LMCS-8(3:7)2012_Takeuti:Truth","doi-asserted-by":"crossref","first-page":"75","DOI":"10.1016\/0168-0072(88)90046-2","volume":"39","author":"Gaisi Takeuti","year":"1988","journal-title":"Annals of pure and applied logic"},{"key":"10.2168\/LMCS-8(3:7)2012_Takeuti1996","doi-asserted-by":"crossref","unstructured":"Gaisi Takeuti. Incompleteness theorems andSi2versusSi+12. InLogic Colloquium '96: Proceedings of the Colloquium held in San Sebasti\u00b4an, Spain, July 9-15, 1996, volume 12 ofLecture notes in logic, pages 247-261, 1996.","DOI":"10.1017\/9781316716816.012"},{"issue":"3","key":"10.2168\/LMCS-8(3:7)2012_Takeuti2000","doi-asserted-by":"crossref","first-page":"1338","DOI":"10.2307\/2586703","volume":"65","author":"Gaisi Takeuti","year":"2000","journal-title":"Journal of Symbolic Logic"},{"key":"10.2168\/LMCS-8(3:7)2012_Wilkie1987Scheme","doi-asserted-by":"crossref","first-page":"261","DOI":"10.1016\/0168-0072(87)90066-2","volume":"35","author":"A. Wilkie and J. Paris","year":"1987","journal-title":"Annals of pure and applied logic"}],"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/863\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/863\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,4,11]],"date-time":"2023-04-11T19:58:03Z","timestamp":1681243083000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/863"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,8,10]]},"references-count":19,"URL":"https:\/\/doi.org\/10.2168\/lmcs-8(3:7)2012","relation":{"is-same-as":[{"id-type":"arxiv","id":"1201.3733","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.1201.3733","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"type":"electronic","value":"1860-5974"}],"subject":[],"published":{"date-parts":[[2012,8,10]]},"article-number":"863"}}