Predicative functionals and an interpretation of ⌢ID

https://doi.org/10.1016/S0168-0072(97)00045-6Get rights and content
Under an Elsevier user license
open archive

Abstract

In 1958 Gödel published his Dialectica interpretation, which reduces classical arithmetic to a quantifier-free theory T axiomatizing the primitive recursive functionals of finite type. Here we extend Gödel's T to theories Pn of “predicative” functionals, which are defined using Martin-Löf's universes of transfinite types. We then extend Gödel's interpretation to the theories of arithmetic inductive definitions ⌢IDn, so that each ⌢IDn is interpreted in the corresponding Pn. Since the strengths of the theories ⌢IDn are cofinal in the ordinal Γ0, as a corollary this analysis provides an ordinal-free characterization of the <Γ0-recursive functions.

Keywords

Functional interpretation
Inductive definitions
Predicative polymorphism
Dependent types

MSC

03F10

Cited by (0)