{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,10,18]],"date-time":"2023-10-18T21:37:05Z","timestamp":1697665025513},"reference-count":15,"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 show that Intuitionistic Open Induction <jats:italic>iop<\/jats:italic> is not closed under the rule <jats:italic>DNS<\/jats:italic>(\u018e<jats:sub>1<\/jats:sub>). This is established by constructing a Kripke model of <jats:italic>iop<\/jats:italic> + \u00acL<jats:sub><jats:italic>y<\/jats:italic><\/jats:sub>(2<jats:italic>y<\/jats:italic> &gt; <jats:italic>x<\/jats:italic>), where L<jats:sub><jats:italic>y<\/jats:italic><\/jats:sub>(2<jats:italic>y<\/jats:italic> &gt; <jats:italic>x<\/jats:italic>) is universally quantified on <jats:italic>x<\/jats:italic>. On the other hand, we prove that <jats:italic>iop<\/jats:italic> is equivalent with the intuitionistic theory axiomatized by <jats:italic>PA<\/jats:italic><jats:sup>\u2212<\/jats:sup> plus the scheme of weak \u00ac\u00ac <jats:italic>LNP<\/jats:italic> for open formulas, where universal quantification on the parameters precedes double negation. We also show that for any open formula <jats:italic>\u03c6<\/jats:italic>(<jats:italic>y<\/jats:italic>) having only <jats:italic>y<\/jats:italic> free. (<jats:italic>PA<\/jats:italic><jats:sup>\u2212<\/jats:sup>)<jats:sup><jats:italic>i<\/jats:italic><\/jats:sup> \u22a2 <jats:italic>L<jats:sub>y<\/jats:sub>\u03c6<\/jats:italic>(<jats:italic>y<\/jats:italic>). We observe that the theories <jats:italic>iop<\/jats:italic>, <jats:italic>i<\/jats:italic>\u2200<jats:sub>1<\/jats:sub> and <jats:italic>i<\/jats:italic>\u03a0<jats:sub>1<\/jats:sub> are closed under Friedman's translation by negated formulas and so under <jats:italic>VR<\/jats:italic> and <jats:italic>IP<\/jats:italic>. We include some remarks on the classical worlds in Kripke models of <jats:italic>iop<\/jats:italic>.<\/jats:p>","DOI":"10.2178\/jsl\/1190150031","type":"journal-article","created":{"date-parts":[[2007,12,13]],"date-time":"2007-12-13T14:12:10Z","timestamp":1197555130000},"page":"91-103","source":"Crossref","is-referenced-by-count":3,"title":["Some weak fragments of <i>HA<\/i> and certain closure properties"],"prefix":"10.1017","volume":"67","author":[{"given":"Morteza","family":"Moniri","sequence":"first","affiliation":[]},{"given":"Mojtaba","family":"Moniri","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2014,3,12]]},"reference":[{"key":"S0022481200009865_ref003","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511551574"},{"key":"S0022481200009865_ref002","doi-asserted-by":"publisher","DOI":"10.1090\/mmono\/067"},{"key":"S0022481200009865_ref013","doi-asserted-by":"crossref","first-page":"452","DOI":"10.1305\/ndjfl\/1039886521","article-title":"Classical and intuitionistic models of arithmetic","volume":"37","author":"Wehmeier","year":"1996","journal-title":"Notre Dame Journal of Formal Logic"},{"key":"S0022481200009865_ref015","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(08)72011-1"},{"key":"S0022481200009865_ref008","volume-title":"Metamathematical investigations of intuitionistic arithmetic and analysis","author":"Smorynski","year":"1973"},{"key":"S0022481200009865_ref009","volume-title":"Basic proof theory","author":"Troelstra","year":"1996"},{"key":"S0022481200009865_ref014","doi-asserted-by":"publisher","DOI":"10.1007\/s001530050081"},{"key":"S0022481200009865_ref007","doi-asserted-by":"publisher","DOI":"10.1016\/0022-4049(92)90127-2"},{"key":"S0022481200009865_ref010","volume-title":"Constructivism in mathematics, an introduction, v.1","author":"Troelstra","year":"1988"},{"key":"S0022481200009865_ref001","doi-asserted-by":"crossref","first-page":"212","DOI":"10.1305\/ndjfl\/1039293063","article-title":"Intuitionistic open induction and least number principle and the Buss operator","volume":"39","author":"Ardeshir","year":"1998","journal-title":"Notre Dame Journal of Formal Logic"},{"key":"S0022481200009865_ref004","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(89)90025-0"},{"key":"S0022481200009865_ref011","volume-title":"Logic and structure","author":"van Dalen","year":"1997"},{"key":"S0022481200009865_ref012","doi-asserted-by":"publisher","DOI":"10.1305\/ndjfl\/1093636765"},{"key":"S0022481200009865_ref006","first-page":"79","article-title":"A nonstandard model for a free variable fragment of number theory","volume":"12","author":"Shepherdson","year":"1964","journal-title":"Bulletin of the Polish Academy of Sciences"},{"key":"S0022481200009865_ref005","doi-asserted-by":"publisher","DOI":"10.1002\/malq.19930390154"}],"container-title":["Journal of Symbolic Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0022481200009865","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,6]],"date-time":"2019-05-06T21:34:31Z","timestamp":1557178471000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0022481200009865\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002,3]]},"references-count":15,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2002,3]]}},"alternative-id":["S0022481200009865"],"URL":"https:\/\/doi.org\/10.2178\/jsl\/1190150031","relation":{},"ISSN":["0022-4812","1943-5886"],"issn-type":[{"value":"0022-4812","type":"print"},{"value":"1943-5886","type":"electronic"}],"subject":[],"published":{"date-parts":[[2002,3]]}}}