{"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":"Since the invention of \u03b2<\/jats:italic>-logic by J. Y. Girard, a lot of work has been done concerning different aspects of this logic, \u03b2<\/jats:italic>-completeness (classical and intuitionistic), interpolation theorems, and completeness of L\u03b2\u03c9<\/jats:italic><\/jats:sub> are some examples of this (see [2], [4] and [5]).<\/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>The central notion in \u03b2<\/jats:italic>-logic is the notion of the \u03b2<\/jats:italic>-rule. The \u03b2<\/jats:italic>-rule is a functor which appropriately groups x<\/jats:italic>-proofs, for every ordinal x<\/jats:italic>. An x<\/jats:italic>-proof is like a proof in \u03c9<\/jats:italic>-logic but instead of the \u03c9<\/jats:italic>-rule, with premises indexed by \u03c9<\/jats:italic>, we use the x<\/jats:italic>-rule, with premises indexed by x<\/jats:italic>.<\/jats:p>In order to obtain the G\u00f6del-functional interpretation of the \u03b2<\/jats:italic>-rule, we need, first<\/jats:italic>, a functional interpretation of the x<\/jats:italic>-proofs, which require functionals using the x<\/jats:italic>-rule for their construction (the x<\/jats:italic>-functionals) and, second<\/jats:italic>, an appropriate grouping of these x<\/jats:italic>-functionals by means of a functor (the \u03b2<\/jats:italic>-functionals).<\/jats:p>We use the letters x,y,z<\/jats:italic>, \u2026 and sometimes the Greek letters \u03b1<\/jats:italic> and \u03b3<\/jats:italic> to denote ordinals. ON is the category of ordinals. The objects are the ordinals, and the morphisms from x<\/jats:italic> to y<\/jats:italic> are the members of I(x, y)<\/jats:italic>, which is the set of all strictly increasing functions from x<\/jats:italic> to y<\/jats:italic>. ON < \u03c9<\/jats:italic> denotes the restriction of ON to \u03c9<\/jats:italic>, the set of finite ordinals. We denote direct systems, in ON or in more general categories, by (xi<\/jats:sub><\/jats:italic>, fij<\/jats:sub><\/jats:italic>) where fij<\/jats:sub><\/jats:italic> is the morphism from xi<\/jats:sub><\/jats:italic>, to xj<\/jats:sub><\/jats:italic>. If the direct limit exists we denote it by (x, fi<\/jats:sub><\/jats:italic>), where fi<\/jats:sub><\/jats:italic> is the morphism from xi<\/jats:sub><\/jats:italic> to x<\/jats:italic>. We write (x, fi<\/jats:sub><\/jats:italic>) =lim<\/jats:underline>(xi<\/jats:sub><\/jats:italic>fij<\/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":[]}],"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":"http:\/\/dx.doi.org\/10.2307\/2274331","relation":{},"ISSN":["0022-4812","1943-5886"],"issn-type":[{"value":"0022-4812","type":"print"},{"value":"1943-5886","type":"electronic"}],"subject":["Logic","Philosophy"],"published":{"date-parts":[[1985,9]]}}}