On bounded functional interpretations (Q424545): Difference between revisions
From MaRDI portal
Created a new Item |
ReferenceBot (talk | contribs) Changed an Item |
||
(6 intermediate revisions by 6 users not shown) | |||
Property / 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. 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}} | |||
Property / 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. 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}} / rank | |||
Normal rank | |||
Property / reviewed by | |||
Property / reviewed by: Jaime Gaspar / rank | |||
Normal rank | |||
Property / Mathematics Subject Classification ID | |||
Property / Mathematics Subject Classification ID: 03F25 / rank | |||
Normal rank | |||
Property / Mathematics Subject Classification ID | |||
Property / Mathematics Subject Classification ID: 03F07 / rank | |||
Normal rank | |||
Property / Mathematics Subject Classification ID | |||
Property / Mathematics Subject Classification ID: 03F10 / rank | |||
Normal rank | |||
Property / Mathematics Subject Classification ID | |||
Property / Mathematics Subject Classification ID: 03F52 / rank | |||
Normal rank | |||
Property / zbMATH DE Number | |||
Property / zbMATH DE Number: 6040330 / rank | |||
Normal rank | |||
Property / zbMATH Keywords | |||
functional interpretations | |||
Property / zbMATH Keywords: functional interpretations / rank | |||
Normal rank | |||
Property / zbMATH Keywords | |||
realizability | |||
Property / zbMATH Keywords: realizability / rank | |||
Normal rank | |||
Property / zbMATH Keywords | |||
majorizability | |||
Property / zbMATH Keywords: majorizability / rank | |||
Normal rank | |||
Property / zbMATH Keywords | |||
intuitionistic linear logic | |||
Property / zbMATH Keywords: intuitionistic linear logic / rank | |||
Normal rank | |||
Property / zbMATH Keywords | |||
intuitionistic logic | |||
Property / zbMATH Keywords: intuitionistic logic / rank | |||
Normal rank | |||
Property / MaRDI profile type | |||
Property / MaRDI profile type: MaRDI publication profile / rank | |||
Normal rank | |||
Property / full work available at URL | |||
Property / full work available at URL: https://doi.org/10.1016/j.apal.2011.12.025 / rank | |||
Normal rank | |||
Property / OpenAlex ID | |||
Property / OpenAlex ID: W2106076660 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Strongly majorizable functionals of finite type: A model for barrecursion containing discontinuous functionals / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Eine Variante zur Dialectica-Interpretation der Heyting-Arithmetik endlicher Typen / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Bounded modified realizability / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Bounded functional interpretation / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Bounded functional interpretation and feasible analysis / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Functional Interpretations of Intuitionistic Linear Logic / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Confined modified realizability / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: ÜBER EINE BISHER NOCH NICHT BENÜTZTE ERWEITERUNG DES FINITEN STANDPUNKTES / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q5344164 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Unifying functional interpretations / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Functional interpretations of linear and intuitionistic logic / rank | |||
Normal rank | |||
links / mardi / name | links / mardi / name | ||
Latest revision as of 07:40, 5 July 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
0 references