Functional interpretation and inductive definitions

TL;DR

This paper extends G"odel's Dialectica interpretation to classical theories of positive arithmetic inductive definitions, translating them into theories of finite-type functionals via transfinite recursion on well-founded trees.

Contribution

It introduces a novel functional interpretation of inductive definitions, connecting classical theories to finite-type functionals through transfinite recursion.

Findings

Provides a new interpretation framework for inductive definitions.

Reduces classical theories to finite-type functional theories.

Establishes a connection between inductive definitions and well-founded trees.

Abstract

Extending G\"odel's \emph{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.