{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,29]],"date-time":"2025-09-29T11:50:56Z","timestamp":1759146656795},"reference-count":11,"publisher":"Cambridge University Press (CUP)","issue":"3","license":[{"start":{"date-parts":[[2014,3,12]],"date-time":"2014-03-12T00:00:00Z","timestamp":1394582400000},"content-version":"unspecified","delay-in-days":3479,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. symb. log."],"published-print":{"date-parts":[[2004,9]]},"abstract":"<jats:title>Abstract.<\/jats:title><jats:p>We prove here that the intuitionistic theory <jats:bold>T<jats:sub>0<\/jats:sub><\/jats:bold>\u21be + <jats:bold>UMID<\/jats:bold><jats:sub><jats:italic>N<\/jats:italic><\/jats:sub>. or even <jats:bold>EETJ<\/jats:bold>\u21be + <jats:bold>UMID<\/jats:bold><jats:sub><jats:italic>N<\/jats:italic><\/jats:sub>, of Explicit Mathematics has the strength of <jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"gif\" xlink:type=\"simple\" xlink:href=\"S0022481200007635_inline1\" \/>\u2013CA<jats:sub>0<\/jats:sub>. In Section 1 we give a double-negation translation for the classical second-order <jats:italic>\u03bc<\/jats:italic>-calculus, which was shown in [M\u00f602] to have the strength of <jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"gif\" xlink:type=\"simple\" xlink:href=\"S0022481200007635_inline1\" \/>\u2013CA<jats:sub>0<\/jats:sub>. In Section 2 we interpret the intuitionistic <jats:italic>\u03bc<\/jats:italic>-calculus in the theory <jats:bold>EETJ<\/jats:bold>\u21be + <jats:bold>UMID<\/jats:bold><jats:sub><jats:italic>N<\/jats:italic><\/jats:sub>. The question about the strength of monotone inductive definitions in <jats:italic>T<\/jats:italic><jats:sub>0<\/jats:sub> was asked by S. Feferman in 1982, and \u2014 assuming classical logic \u2014 was addressed by M. Rathjen.<\/jats:p>","DOI":"10.2178\/jsl\/1096901767","type":"journal-article","created":{"date-parts":[[2005,3,2]],"date-time":"2005-03-02T21:43:19Z","timestamp":1109799799000},"page":"790-798","source":"Crossref","is-referenced-by-count":7,"title":["On the intuitionistic strength of monotone inductive definitions"],"prefix":"10.1017","volume":"69","author":[{"given":"Sergei","family":"Tupailo","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2014,3,12]]},"reference":[{"key":"S0022481200007635_ref011","doi-asserted-by":"publisher","DOI":"10.1016\/S0168-0072(02)00065-9"},{"key":"S0022481200007635_ref010","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(89)90019-5"},{"key":"S0022481200007635_ref005","unstructured":"M\u00f6llerfeld M. , Generalized Inductive Definitions. The \u03bc-calculus and -comprehension, Ph.D. thesis , Universit\u00e4t M\u00fcnster, 2002."},{"key":"S0022481200007635_ref006","first-page":"125","volume":"61","author":"Rathjen","year":"1996","journal-title":"Monotone inductive definitions in explicit mathematics"},{"key":"S0022481200007635_ref001","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0062852"},{"key":"S0022481200007635_ref002","first-page":"159","volume-title":"Logic colloquium \u201978","author":"Feferman","year":"1979"},{"key":"S0022481200007635_ref004","doi-asserted-by":"publisher","DOI":"10.1016\/S0168-0072(96)00040-1"},{"key":"S0022481200007635_ref007","first-page":"509","volume":"63","author":"Rathjen","year":"1998","journal-title":"Explicit mathematics with the monotone fixed point principle"},{"key":"S0022481200007635_ref008","first-page":"517","volume":"64","author":"Rathjen","year":"1999","journal-title":"Explicit mathematics with the monotone fixed point principle. II. Models"},{"key":"S0022481200007635_ref009","first-page":"329","volume-title":"Reflections on the foundations of mathematics: Essays in Honour of Solomon Feferman","volume":"15","author":"Rathjen","year":"2002"},{"key":"S0022481200007635_ref003","first-page":"77","volume-title":"The L. E. J. Brouwer centenary symposium","author":"Feferman","year":"1982"}],"container-title":["Journal of Symbolic Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0022481200007635","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,6]],"date-time":"2019-05-06T20:26:50Z","timestamp":1557174410000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0022481200007635\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004,9]]},"references-count":11,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2004,9]]}},"alternative-id":["S0022481200007635"],"URL":"https:\/\/doi.org\/10.2178\/jsl\/1096901767","relation":{},"ISSN":["0022-4812","1943-5886"],"issn-type":[{"value":"0022-4812","type":"print"},{"value":"1943-5886","type":"electronic"}],"subject":[],"published":{"date-parts":[[2004,9]]}}}