On bounded functional interpretations (Q424545): Difference between revisions
From MaRDI portal
Changed an Item |
Added link to MaRDI item. |
||
links / mardi / name | links / mardi / name | ||
Revision as of 04:50, 30 January 2024
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | On bounded functional interpretations |
scientific article |
Statements
On bounded functional interpretations (English)
0 references
1 June 2012
0 references
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. Paulo 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. This 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. \end{itemize}}
0 references
functional interpretations
0 references
realizability
0 references
majorizability
0 references
intuitionistic linear logic
0 references
intuitionistic logic
0 references