{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,2]],"date-time":"2022-04-02T06:11:11Z","timestamp":1648879871677},"reference-count":1,"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":12976,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. symb. log."],"published-print":{"date-parts":[[1978,9]]},"abstract":"<jats:p>This note is concerned with the old topic, initiated by Kleene, of the connections between recursive function theory and provability in intuitionistic arithmetic. More specifically, we are interested in the relationship between the hierarchy of degrees of unsolvability and the interdeducibility of cases of excluded middle. The work described below was motivated by a counterexample, to be given presently, which shows that that relationship is more complicated than one might suppose.<\/jats:p><jats:p>Let HA be first-order intuitionistic arithmetic. Let the symbol \u22a2 mean derivability in HA. For each natural number <jats:italic>n<\/jats:italic>, let n\u00af be the corresponding numeral. Let \u03a9 be the standard model of arithmetic. Say that a sentence <jats:italic>\u03d5<\/jats:italic> is <jats:italic>true<\/jats:italic> iff \u03a9\u22a8 <jats:italic>\u03d5<\/jats:italic>. Now suppose <jats:italic>\u03d5<\/jats:italic>(<jats:italic>x<\/jats:italic>) and <jats:italic>\u03a8<\/jats:italic>(<jats:italic>x<\/jats:italic>) are formulas with only the variable <jats:italic>x<\/jats:italic> free. Suppose<\/jats:p><jats:p><jats:disp-formula><jats:graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" orientation=\"portrait\" mime-subtype=\"gif\" mimetype=\"image\" position=\"float\" xlink:type=\"simple\" xlink:href=\"S0022481200049380_eqnU1\" \/><\/jats:disp-formula><\/jats:p><jats:p>Then it is natural to conjecture that {<jats:italic>n<\/jats:italic>\u2223\u03a9\u22a8<jats:italic>\u03a8<\/jats:italic>(n\u00af)} is recursive in {<jats:italic>n<\/jats:italic>\u2223\u03a9\u22a8<jats:italic>\u03d5<\/jats:italic>(n\u00af)}.<\/jats:p><jats:p>However, this conjecture is false. Consider the formula is a formalization of Kleene's T-predicate.<\/jats:p>","DOI":"10.2307\/2273526","type":"journal-article","created":{"date-parts":[[2006,5,6]],"date-time":"2006-05-06T17:48:21Z","timestamp":1146937701000},"page":"497-501","source":"Crossref","is-referenced-by-count":0,"title":["The nonconstructive content of sentences of arithmetic"],"prefix":"10.1017","volume":"43","author":[{"given":"Nicolas D.","family":"Goodman","sequence":"first","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2014,3,12]]},"reference":[{"key":"S0022481200049380_ref001","first-page":"11","volume":"27","author":"Kleene","year":"1962","journal-title":"Disjunction and existence under implication in elementary intuitionistic formalisms"}],"container-title":["Journal of Symbolic Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0022481200049380","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,27]],"date-time":"2019-05-27T15:33:17Z","timestamp":1558971197000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0022481200049380\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1978,9]]},"references-count":1,"journal-issue":{"issue":"3","published-print":{"date-parts":[[1978,9]]}},"alternative-id":["S0022481200049380"],"URL":"https:\/\/doi.org\/10.2307\/2273526","relation":{},"ISSN":["0022-4812","1943-5886"],"issn-type":[{"value":"0022-4812","type":"print"},{"value":"1943-5886","type":"electronic"}],"subject":[],"published":{"date-parts":[[1978,9]]}}}