Hybrid functional interpretations of linear and intuitionistic logic (Q2882562)

In the present paper it is shown how to combine Kreisel's modified realizability, Diller-Nahm interpretation and Gödel's Dialectica interpretation into a single functional interpretation. The goal is to maximize the applicability of the usual proof mining techniques taking advantage, with this single hybrid interpretation, of the best features of each of the known functional interpretations. The hybrid interpretation is presented in the setting of a multi-modal linear logic which includes distinct modalities to correspond to each of the various functional interpretations. It is well known that intuitionistic proofs can be embedded into linear logic ones. The paper presents an algorithm for decorating a linear translation of a given intuitionistic proof with different modalities. In this way the hybrid interpretation technique can be applied to intuitionistic logic (or even classical logic via a negative translation). A monotone soundness theorem for the hybrid interpretation is proved and an attempt for a bounded variant of the hybrid interpretation (which combines the bounded modified realizability and a variant of the bounded functional interpretation) is presented.NEWLINENEWLINEThis paper is the journal version of the conference paper [\textit{M.-D. Hernest} and \textit{P. Oliva}, Lect. Notes Comput. Sci. 5028, 251--260 (2008; Zbl 1142.03368)]. The study of the hybrid interpretation was preceded by work of the same author concerning different interpretations for the exponentials and how they correspond to well-known functional interpretations of intuitionistic logic. See the pioneer papers [\textit{P. Oliva}, ``Modified realizability interpretation of classical linear logic'', Proceedings of the Twenty Second Annual IEEE Symposium LICS'07, 431--440 (2007)] and [\textit{P. Oliva}, Lect. Notes Comput. Sci. 4576, 285--296 (2007; Zbl 1213.03074)], or the more recent [\textit{P. Oliva}, Inf. Comput. 208, No. 5, 565--577 (2010; Zbl 1193.03081)] and [\textit{G. Ferreira} and \textit{P. Oliva}, Log. Methods Comput. Sci. 7, No. 1, Paper No. 9, 22 p. (2011; Zbl 1227.03079)].