file.pdf (221.7 kB)
Download fileFunctional Interpretation and Inductive Definitions
Extending Gödel's Dialectica interpretation, we provide a functional interpretation of classical theories of positive arithmetic inductive definitions, reducing them to theories of finite-type functionals defined using transfinite recursion on well-founded trees.