Functional interpretations of linear and intuitionistic logic (Q964504)

The paper under review is a contribution to the unification of the various proof interpretations in the context of linear logic. The author shows how different functional interpretations of intuitionistic logic can be obtained via a parametrised interpretation of classical linear logic, using Girard's standard translation \((\cdot)^*\) of intuitionistic logic into linear logic. The parametrised interpretation of classical linear logic is presented in terms of simultaneous one-move two-player games, where the moves are higher-order functionals in the language of finite types. It consists of a basic, parameter-free, interpretation of the logical connectives and quantifiers and of a parametrised interpretation of the exponentials. Regarding the pure fragment of classical linear logic, the soundness of the interpretation is proved and the characterization of the interpretation (using principles with branching quantifiers) is investigated. Concerning the interpretation of the modalities there is a break of symmetry: one player can see the opponent's move before playing and instead of a single move he is allowed to play a set of moves. More important, the interpretation of the modalities is parametrised, i.e. the choice of sets is left open, apart from the imposition of some conditions to ensure the soundness of the interpretation. Different alternatives for the interpretation of the exponentials (i.e. different instantiations of the set parameter satisfying the required conditions) are presented. It is shown that these different interpretations, when combined with the embedding of intuitionistic logic into linear logic, correspond to well-known functional interpretations of intuitionistic logic, such as Kreisel's modified realizability, Gödel's Dialectica interpretation, Diller-Nahm interpretation, and Stein's interpretation. Some considerations on how to include the bounded functional interpretation into this unified framework are also made, using a prior relativisation of the quantifiers to Bezem's model of strongly majorizable functionals. For related work on the subject see: [\textit{P. Oliva}, ``Unifying functional interpretations'', Notre Dame J. Formal Logic 47, No. 2, 263--290 (2006; Zbl 1113.03052)]; [\textit{P. Oliva}, ``Modified realizability interpretation of classical linear logic'', in: Proceedings of the 22nd Annual IEEE Symposium on Logic in Computer Science LICS 2007, 431--440 (2007)]; and [\textit{G. Ferreira} and \textit{P. Oliva}, ``Functional interpretations of intuitionistic linear logic'', Lect. Notes Comput. Sci. 5771, 3--19 (2009; Zbl 1193.03080)].