{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,14]],"date-time":"2026-05-14T13:13:01Z","timestamp":1778764381330,"version":"3.51.4"},"reference-count":25,"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>A classical quantified modal logic is used to define a \u201cfeasible\u201d arithmetic <jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"gif\" xlink:type=\"simple\" xlink:href=\"S0022481200009877_inline1\"\/> whose provably total functions are exactly the polynomial-time computable functions. Informally, one understands \u20de\u221d as \u201c\u221d is feasibly demonstrable\u201d.<\/jats:p><jats:p><jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"gif\" xlink:type=\"simple\" xlink:href=\"S0022481200009877_inline1\"\/> differs from a system <jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"gif\" xlink:type=\"simple\" xlink:href=\"S0022481200009877_inline2\"\/> that is as powerful as Peano Arithmetic only by the restriction of induction to ontic (i.e., \u20de-free) formulas. Thus, <jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"gif\" xlink:type=\"simple\" xlink:href=\"S0022481200009877_inline1\"\/> is defined without any reference to bounding terms, and admitting induction over formulas having arbitrarily many alternations of unbounded quantifiers. The system also uses only a very small set of initial functions.<\/jats:p><jats:p>To obtain the characterization, one extends the Curry-Howard isomorphism to include modal operations. This leads to a realizability translation based on recent results in higher-type ramified recursion. The fact that induction formulas are not restricted in their logical complexity, allows one to use the Friedman A translation directly.<\/jats:p><jats:p>The development also leads us to propose a new Frege rule, the \u201cModal Extension\u201d rule: if \u22a2 \u221d a then \u22a2 <jats:italic>A<\/jats:italic>  \u2194 \u221d for new symbol <jats:italic>A<\/jats:italic>.<\/jats:p>","DOI":"10.2178\/jsl\/1190150032","type":"journal-article","created":{"date-parts":[[2007,12,13]],"date-time":"2007-12-13T19:12:10Z","timestamp":1197573130000},"page":"104-116","source":"Crossref","is-referenced-by-count":11,"title":["A new \u201cfeasible\u201d arithmetic"],"prefix":"10.1017","volume":"67","author":[{"given":"Stephen","family":"Bellantoni","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Martin","family":"Hofmann","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2014,3,12]]},"reference":[{"key":"S0022481200009877_ref007","volume-title":"Bounded arithmetic","author":"Buss","year":"1986"},{"key":"S0022481200009877_ref021","volume-title":"Ramified recursion and intuitionism","author":"Nelson","year":"1997"},{"key":"S0022481200009877_ref022","volume-title":"Rencontre du reseau georges reeb","author":"Nelson","year":"1997"},{"key":"S0022481200009877_ref020","doi-asserted-by":"publisher","DOI":"10.1515\/9781400858927"},{"key":"S0022481200009877_ref012","first-page":"275","article-title":"A mixed modal\/linear lambda calculus with applications to Bellantoni-Cook safe recursion","volume":"1414","author":"Hofmann","year":"1998","journal-title":"CSL '97"},{"key":"S0022481200009877_ref018","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-60178-3_84"},{"key":"S0022481200009877_ref006","doi-asserted-by":"publisher","DOI":"10.1007\/BF00370383"},{"key":"S0022481200009877_ref009","volume":"143","author":"Girard","year":"1998","journal-title":"Light linear logic"},{"key":"S0022481200009877_ref011","volume":"49","author":"Goodman","year":"1984","journal-title":"Epistemic arithmetic is a conservative extension of intuitionistic arithmetic"},{"key":"S0022481200009877_ref001","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(93)90181-R"},{"key":"S0022481200009877_ref002","volume-title":"Proof complexity and feasible arithmetics","volume":"39","author":"Bellantoni","year":"1998"},{"key":"S0022481200009877_ref025","volume-title":"Constructivism in mathematics, volume I","author":"Troelstra","year":"1988"},{"key":"S0022481200009877_ref024","doi-asserted-by":"publisher","DOI":"10.1007\/BF01620765"},{"key":"S0022481200009877_ref005","volume-title":"Annals of Pure and Applied Logic","author":"Bellantoni","year":"2000"},{"key":"S0022481200009877_ref003","doi-asserted-by":"publisher","DOI":"10.1007\/BF01201998"},{"key":"S0022481200009877_ref019","unstructured":"Leivant D. and Marion J. Y. , Ramified recurrence and computational complexity IV: Predicative functionals and poly-space, Information and Computation , (to appear)."},{"key":"S0022481200009877_ref008","volume-title":"Semantics and logics of computation","author":"Coquand","year":"1997"},{"key":"S0022481200009877_ref004","unstructured":"Bellantoni S. and Niggl K. H. , Ranking recursions: the low Grzegorczyk hierarchy reconsidered, SIAM Journal of Computing , (to appear)."},{"key":"S0022481200009877_ref015","article-title":"Languages that capture complexity classes","volume":"4","author":"Immerman","journal-title":"SIAM Journal of Computing"},{"key":"S0022481200009877_ref016","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511529948"},{"key":"S0022481200009877_ref017","first-page":"320","volume-title":"Feasible mathematics II","author":"Leivant","year":"1994"},{"key":"S0022481200009877_ref023","volume-title":"Intensional mathematics","volume":"113","author":"Shapiro","year":"1985"},{"key":"S0022481200009877_ref013","volume-title":"Technical report","author":"Hofmann","year":"1999"},{"key":"S0022481200009877_ref010","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90386-T"},{"key":"S0022481200009877_ref014","doi-asserted-by":"publisher","DOI":"10.1016\/S0168-0072(00)00010-5"}],"container-title":["Journal of Symbolic Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0022481200009877","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,7]],"date-time":"2019-05-07T01:34:41Z","timestamp":1557192881000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0022481200009877\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002,3]]},"references-count":25,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2002,3]]}},"alternative-id":["S0022481200009877"],"URL":"https:\/\/doi.org\/10.2178\/jsl\/1190150032","relation":{},"ISSN":["0022-4812","1943-5886"],"issn-type":[{"value":"0022-4812","type":"print"},{"value":"1943-5886","type":"electronic"}],"subject":[],"published":{"date-parts":[[2002,3]]}}}