On bounded functional interpretations (Q424545)

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 functional interpretations what they have in common and in what they differ.NEWLINENEWLINE\end{itemize}}