Functional interpretation of the β-rule

Extract

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 (x_i, f_ij) where f_ij is the morphism from x_i, to x_j. If the direct limit exists we denote it by (x, f_i), where f_i is the morphism from x_i to x. We write (x, f_i) =lim(x_if_ij). In ON the direct limits are unique.