Functional interpretation of the β-rule

Since the invention of β-logic by J. Y. Girard, a lot of work has been done concerning different aspects of this logic, β-completeness (classical and intuitionistic), interpolation theorems, and completeness of Lβω are some examples of this (see [2], [4] and [5]).In this paper we examine the question, posed by J. Y. Girard, of the Gödel-functional interpretation for this new logic.The central notion in β-logic is the notion of the β-rule. The β-rule is a functor which appropriately groups x-proofs, for every ordinal x. An x-proof is like a proof in ω-logic but instead of the ω-rule, with premises indexed by ω, we use the x-rule, with premises indexed by x.In order to obtain the Gödel-functional interpretation of the β-rule, we need, first, a functional interpretation of the x-proofs, which require functionals using the x-rule for their construction (the x-functionals) and, second, an appropriate grouping of these x-functionals by means of a functor (the β-functionals).We use the letters x,y,z, … and sometimes the Greek letters α and γ to denote ordinals. ON is the category of ordinals. The objects are the ordinals, and the morphisms from x to y are the members of I(x, y), which is the set of all strictly increasing functions from x to y. ON < ω denotes the restriction of ON to ω, the set of finite ordinals. We denote direct systems, in ON or in more general categories, by (xi, fij) where fij is the morphism from xi, to xj. If the direct limit exists we denote it by (x, fi), where fi is the morphism from xi to x. We write (x, fi) =lim(xifij). In ON the direct limits are unique.