{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,6,9]],"date-time":"2024-06-09T08:55:31Z","timestamp":1717923331232},"reference-count":19,"publisher":"Cambridge University Press (CUP)","issue":"6","license":[{"start":{"date-parts":[[2014,3,11]],"date-time":"2014-03-11T00:00:00Z","timestamp":1394496000000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2014,12]]},"abstract":"<jats:p>For any partial combinatory algebra (PCA for short) <jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"gif\" xlink:type=\"simple\" xlink:href=\"S0960129513000856_inline1\" \/><jats:tex-math>$\\mathcal{A}$<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula>, the class of <jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"gif\" xlink:type=\"simple\" xlink:href=\"S0960129513000856_inline1\" \/><jats:tex-math>$\\mathcal{A}$<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula>-representable partial functions from <jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"gif\" xlink:type=\"simple\" xlink:href=\"S0960129513000856_inline2\" \/><jats:tex-math>$\\mathbb{N}$<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula> to <jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"gif\" xlink:type=\"simple\" xlink:href=\"S0960129513000856_inline1\" \/><jats:tex-math>$\\mathcal{A}$<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula> quotiented by the filter of cofinite sets of <jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"gif\" xlink:type=\"simple\" xlink:href=\"S0960129513000856_inline2\" \/><jats:tex-math>$\\mathbb{N}$<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula> is a PCA such that the representable partial functions are exactly the limiting partial functions of <jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"gif\" xlink:type=\"simple\" xlink:href=\"S0960129513000856_inline1\" \/><jats:tex-math>$\\mathcal{A}$<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula>-representable partial functions (Akama 2004). The <jats:italic>n<\/jats:italic>-times iteration of this construction results in a PCA that represents any <jats:italic>n<\/jats:italic>-iterated limiting partial recursive function, and the inductive limit of the PCAs over all <jats:italic>n<\/jats:italic> is a PCA that represents any arithmetical partial function. Kleene's realizability interpretation over the former PCA interprets the logical principles of double negation elimination for \u03a3<jats:sup>0<\/jats:sup><jats:sub><jats:italic>n<\/jats:italic><\/jats:sub>-formulae, and over the latter PCA, it interprets Peano's arithmetic (PA for short). A hierarchy of logical systems between Heyting's arithmetic (HA for short) and PA is used to discuss the prenex normal form theorem, relativised independence-of-premise schemes, and the statement \u2018PA is an unbounded extension of HA\u2019.<\/jats:p>","DOI":"10.1017\/s0960129513000856","type":"journal-article","created":{"date-parts":[[2014,3,11]],"date-time":"2014-03-11T14:12:02Z","timestamp":1394547122000},"source":"Crossref","is-referenced-by-count":1,"title":["Realizability interpretation of PA by iterated limiting PCA"],"prefix":"10.1017","volume":"24","author":[{"given":"YOHJI","family":"AKAMA","sequence":"first","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2014,3,11]]},"reference":[{"key":"S0960129513000856_ref18","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(09)70144-2"},{"key":"S0960129513000856_ref19","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0066739"},{"key":"S0960129513000856_ref9","volume-title":"Introduction to Combinators and Lambda-calculus","author":"Hindley","year":"1986"},{"key":"S0960129513000856_ref14","first-page":"429","article-title":"Recursive functions modulo CO-r-maximal sets.","volume":"148","author":"Lerman","year":"1970","journal-title":"Transactions of the American Mathematical Society"},{"key":"S0960129513000856_ref2","doi-asserted-by":"crossref","unstructured":"Akama Y. , Berardi S. , Hayashi S. and Kohlenbach U. (2004) An arithmetical hierarchy of the laws of excluded middle and related principles. In: Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science 192\u2013201.","DOI":"10.1109\/LICS.2004.1319613"},{"key":"S0960129513000856_ref5","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129504004529"},{"key":"S0960129513000856_ref4","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-68952-9"},{"key":"S0960129513000856_ref1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(03)00360-8"},{"key":"S0960129513000856_ref7","volume-title":"Metamathematics of first-order arithmetic","author":"H\u00e1jek","year":"1998"},{"key":"S0960129513000856_ref16","doi-asserted-by":"publisher","DOI":"10.1002\/malq.19610070710"},{"key":"S0960129513000856_ref11","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2010.08.003"},{"key":"S0960129513000856_ref12","doi-asserted-by":"publisher","DOI":"10.2307\/2269016"},{"key":"S0960129513000856_ref3","first-page":"57","volume-title":"Logic Colloquium '98","author":"Avigad","year":"2000"},{"key":"S0960129513000856_ref15","volume-title":"Classical Recursion Theory: The Theory of Functions and Sets of Natural Numbers","author":"Odifreddi","year":"1989"},{"key":"S0960129513000856_ref6","doi-asserted-by":"publisher","DOI":"10.2307\/2586854"},{"key":"S0960129513000856_ref10","doi-asserted-by":"publisher","DOI":"10.1007\/BF02757881"},{"key":"S0960129513000856_ref8","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00350-9"},{"key":"S0960129513000856_ref13","volume-title":"Introduction to metamathematics","author":"Kleene","year":"1952"},{"key":"S0960129513000856_ref17","unstructured":"Smory\u0144ski C. (1978) Nonstandard models of arithmetic. Course notes, fall 1978, Utrecht University. Logic group preprint series."}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129513000856","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,21]],"date-time":"2019-04-21T21:13:55Z","timestamp":1555881235000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129513000856\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,3,11]]},"references-count":19,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2014,12]]}},"alternative-id":["S0960129513000856"],"URL":"https:\/\/doi.org\/10.1017\/s0960129513000856","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,3,11]]},"article-number":"e240603"}}