The Uniform Functional Interpretation with Informative Types
Fuente:
arXiv
Saved in:
| Main Authors: | , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866916935369752576 |
|---|---|
| author | Ferreira, Fernando Oliva, Paulo |
| author_facet | Ferreira, Fernando Oliva, Paulo |
| contents | 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ödel's functional dialectica interpretation with majorizability. When the information is "canonical" in function types, we obtain new functional interpretations and new models of Gödel's theory T. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2508_12781 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | The Uniform Functional Interpretation with Informative Types Ferreira, Fernando Oliva, Paulo Logic Logic in Computer Science 03F10, 03F25, 03F55 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ödel's functional dialectica interpretation with majorizability. When the information is "canonical" in function types, we obtain new functional interpretations and new models of Gödel's theory T. |
| title | The Uniform Functional Interpretation with Informative Types |
| topic | Logic Logic in Computer Science 03F10, 03F25, 03F55 |
| url | https://arxiv.org/abs/2508.12781 |