The Uniform Functional Interpretation with Informative Types

TL;DR

This paper introduces a flexible new approach to functional interpretations using uniform quantification and relativization, enabling deeper analysis of collection principles and new models of G"odel's theory T.

Contribution

It presents a novel framework combining uniform quantification and relativization, leading to new functional interpretations and models of G"odel's theory T.

Findings

Recovers a form of G"odel's dialectica interpretation with bounds

Develops new functional interpretations based on canonical information

Provides new models of G"odel's theory T

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.