{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,5]],"date-time":"2022-04-05T06:06:02Z","timestamp":1649138762692},"reference-count":0,"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":10419,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. symb. log."],"published-print":{"date-parts":[[1985,9]]},"abstract":"<jats:p>Since the invention of <jats:italic>\u03b2<\/jats:italic>-logic by J. Y. Girard, a lot of work has been done concerning different aspects of this logic, <jats:italic>\u03b2<\/jats:italic>-completeness (classical and intuitionistic), interpolation theorems, and completeness of L<jats:sub><jats:italic>\u03b2\u03c9<\/jats:italic><\/jats:sub> are some examples of this (see [2], [4] and [5]).<\/jats:p><jats:p>In this paper we examine the question, posed by J. Y. Girard, of the G\u00f6del-functional interpretation for this new logic.<\/jats:p><jats:p>The central notion in <jats:italic>\u03b2<\/jats:italic>-logic is the notion of the <jats:italic>\u03b2<\/jats:italic>-rule. The <jats:italic>\u03b2<\/jats:italic>-rule is a functor which appropriately groups <jats:italic>x<\/jats:italic>-proofs, for every ordinal <jats:italic>x<\/jats:italic>. An <jats:italic>x<\/jats:italic>-proof is like a proof in <jats:italic>\u03c9<\/jats:italic>-logic but instead of the <jats:italic>\u03c9<\/jats:italic>-rule, with premises indexed by <jats:italic>\u03c9<\/jats:italic>, we use the <jats:italic>x<\/jats:italic>-rule, with premises indexed by <jats:italic>x<\/jats:italic>.<\/jats:p><jats:p>In order to obtain the G\u00f6del-functional interpretation of the <jats:italic>\u03b2<\/jats:italic>-rule, we need, <jats:italic>first<\/jats:italic>, a functional interpretation of the <jats:italic>x<\/jats:italic>-proofs, which require functionals using the <jats:italic>x<\/jats:italic>-rule for their construction (the <jats:italic>x<\/jats:italic>-functionals) and, <jats:italic>second<\/jats:italic>, an appropriate grouping of these <jats:italic>x<\/jats:italic>-functionals by means of a functor (the <jats:italic>\u03b2<\/jats:italic>-functionals).<\/jats:p><jats:p>We use the letters <jats:italic>x,y,z<\/jats:italic>, \u2026 and sometimes the Greek letters <jats:italic>\u03b1<\/jats:italic> and <jats:italic>\u03b3<\/jats:italic> to denote ordinals. ON is the category of ordinals. The objects are the ordinals, and the morphisms from <jats:italic>x<\/jats:italic> to <jats:italic>y<\/jats:italic> are the members of <jats:italic>I(x, y)<\/jats:italic>, which is the set of all strictly increasing functions from <jats:italic>x<\/jats:italic> to <jats:italic>y<\/jats:italic>. ON &lt; <jats:italic>\u03c9<\/jats:italic> denotes the restriction of ON to <jats:italic>\u03c9<\/jats:italic>, the set of finite ordinals. We denote direct systems, in ON or in more general categories, by (<jats:italic>x<jats:sub>i<\/jats:sub><\/jats:italic>, <jats:italic>f<jats:sub>ij<\/jats:sub><\/jats:italic>) where <jats:italic>f<jats:sub>ij<\/jats:sub><\/jats:italic> is the morphism from <jats:italic>x<jats:sub>i<\/jats:sub><\/jats:italic>, to <jats:italic>x<jats:sub>j<\/jats:sub><\/jats:italic>. If the direct limit exists we denote it by (<jats:italic>x, f<jats:sub>i<\/jats:sub><\/jats:italic>), where <jats:italic>f<jats:sub>i<\/jats:sub><\/jats:italic> is the morphism from <jats:italic>x<jats:sub>i<\/jats:sub><\/jats:italic> to <jats:italic>x<\/jats:italic>. We write (<jats:italic>x, f<jats:sub>i<\/jats:sub><\/jats:italic>) =<jats:underline>lim<\/jats:underline>(<jats:italic>x<jats:sub>i<\/jats:sub><\/jats:italic><jats:italic>f<jats:sub>ij<\/jats:sub><\/jats:italic>). In ON the direct limits are unique.<\/jats:p>","DOI":"10.2307\/2274331","type":"journal-article","created":{"date-parts":[[2006,5,6]],"date-time":"2006-05-06T22:14:36Z","timestamp":1146953676000},"page":"791-805","source":"Crossref","is-referenced-by-count":0,"title":["Functional interpretation of the \u03b2-rule"],"prefix":"10.1017","volume":"50","author":[{"given":"George","family":"Koletsos","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2014,3,12]]},"container-title":["Journal of Symbolic Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0022481200032412","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,22]],"date-time":"2019-05-22T21:56:09Z","timestamp":1558562169000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0022481200032412\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1985,9]]},"references-count":0,"journal-issue":{"issue":"3","published-print":{"date-parts":[[1985,9]]}},"alternative-id":["S0022481200032412"],"URL":"https:\/\/doi.org\/10.2307\/2274331","relation":{},"ISSN":["0022-4812","1943-5886"],"issn-type":[{"value":"0022-4812","type":"print"},{"value":"1943-5886","type":"electronic"}],"subject":[],"published":{"date-parts":[[1985,9]]}}}