Proof interpretations with truth |
| |
| Authors: | Jaime Gaspar Paulo Oliva |
| |
| Affiliation: | 1. Fachbereich Mathematik, Technische Universit?t Darmstadt, Schlossgartenstrasse 7, 64289 Darmstadt, Germany;2. Queen Mary University of London, School of Electronic Engineering and Computer Science, London E1 4NS |
| |
| Abstract: | This article systematically investigates so‐called “truth variants” of several functional interpretations. We start by showing a close relation between two variants of modified realizability, namely modified realizability with truth and q‐modified realizability. Both variants are shown tobe derived from a single “functional interpretation with truth” of intuitionistic linear logic. This analysis suggests that several functional interpretations have truth and q‐variants. These variants, however, require a more involved modification than the ones previously considered. Following this lead we present truth and q‐variants of the Diller‐Nahm interpretation, the bounded modified realizability and the bounded functional interpretation (© 2010 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim) |
| |
| Keywords: | Modified realizability with truth and q‐variant intuitionistic linear logic Aczel and Kleene slashes |
|
|
