On bounded functional interpretations
type: Item
instance of: scholarly article
title: On bounded functional interpretations
zbMATH Open document ID: 1251.03074
author: Gilda Ferreira
author: Paulo Oliva
published in: Annals of Pure and Applied Logic
publication date: 2012-06-01T00:00:00Z
reviewed by: Jaime Gaspar
Mathematics Subject Classification ID: 03F25
Mathematics Subject Classification ID: 03F07
Mathematics Subject Classification ID: 03F10
Mathematics Subject Classification ID: 03F52
zbMATH DE Number: 6040330
zbMATH Keywords: functional interpretations
zbMATH Keywords: realizability
zbMATH Keywords: majorizability
zbMATH Keywords: intuitionistic linear logic
zbMATH Keywords: intuitionistic logic
MaRDI profile type: Publication
full work available at URL: j.apal.2011.12.025
OpenAlex ID: W2106076660
cites work: Strongly majorizable functionals of finite type: A model for barrecursion containing discontinuous functionals
cites work: Eine Variante zur Dialectica-Interpretation der Heyting-Arithmetik endlicher Typen
cites work: Bounded modified realizability
cites work: Bounded functional interpretation
cites work: Bounded functional interpretation and feasible analysis
cites work: Functional Interpretations of Intuitionistic Linear Logic
cites work: Confined modified realizability
cites work: ÜBER EINE BISHER NOCH NICHT BENÜTZTE ERWEITERUNG DES FINITEN STANDPUNKTES
cites work: Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
cites work: Q5344164
cites work: Unifying functional interpretations
cites work: Functional interpretations of linear and intuitionistic logic
DOI: 10.1016/J.APAL.2011.12.025
review text: Functional interpretations are powerful tools in mathematical logic with many applications, among them witnessing existential statements. The first class of functional interpretations provided precise witnesses for existential statements. A second class of functional interpretations provided bounds for existential statements by changing the target from precise witnesses to bounds in a last step. A third class of functional interpretations, called bounded functional interpretations, provided also bounds but targeting bounds from the first step.NEWLINENEWLINEPaulo Oliva, joined by Gilda Ferreira, has pursued a unification program: to show that different functional interpretations are instances of a parametrized functional interpretation. The first class of unifications took place in the context of the usual intuitionistic logic. A second class of unifications changed the context to classical linear logic. Then a third class of unifications changed the context to intuitionistic linear logic.NEWLINENEWLINEThis being said, now we can easily describe the article in question: It presents a unification in the context of intuitionistic linear logic of bounded functional interpretations. More extensively, the article: {\parindent=6mm \begin{itemize}\item[(1)] presents parametrized functional interpretations of the usual intuitionistic logic and of intuitionistic linear logic; \item[(2)] shows that the two parametrized functional interpretations are the same modulo embedding one logic in the other; \item[(3)] proves the soundness theorem / adequacy lemma for the parametrized functional interpretations; \item[(4)] shows that the parametrized functional interpretations instantiate into three bounded functional interpretations, namely the (simply called) bounded functional interpretation, the bounded modified realizability and the confined modified realizability; \item[(5)] sheds light on the comparison of the bounded functional interpretations by making clear in the parametrized…
description: scientific article; zbMATH DE number 6040330