Predicative functionals and an interpretation of ⌢ID<ω Original Research Article

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 View the MathML source, so that each View the MathML source is interpreted in the corresponding Pn. Since the strengths of the theories View the MathML source are cofinal in the ordinal Γ0, as a corollary this analysis provides an ordinal-free characterization of the <Γ0-recursive functions.