The Uniform Functional Interpretation with Informative Types
Logic
2025-09-08 v2 Logic in Computer Science
Abstract
We discuss a new approach to functional interpretations based on uniform quantification and relativization. The uniform quantification in the background permits a more penetrating analysis of principles related to collection and contra-collection. Relativization comes from a computationally informative notion of being an element of a given type. The approach is flexible. When the information takes the shape of bounds, we can recapture a form of the combination of G\"odel's functional dialectica interpretation with majorizability. When the information is "canonical" in function types, we obtain new functional interpretations and new models of G\"odel's theory T.
Cite
@article{arxiv.2508.12781,
title = {The Uniform Functional Interpretation with Informative Types},
author = {Fernando Ferreira and Paulo Oliva},
journal= {arXiv preprint arXiv:2508.12781},
year = {2025}
}