Functional interpretation and inductive definitions
Logic
2009-02-17 v4
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.
Cite
@article{arxiv.0802.1938,
title = {Functional interpretation and inductive definitions},
author = {Jeremy Avigad and Henry Towsner},
journal= {arXiv preprint arXiv:0802.1938},
year = {2009}
}
Comments
minor corrections and changes