Proof interpretations with truth

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 to be derived from a single “functional interpretation with truth” of intuitionistic linear logic. This analysis suggests that, contrary to what is believed, 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. Keywords Modified realizability with truth and q-variant, intuitionistic linear logic, Aczel and Kleene slashes Subject classification 03F07, 03F10, 03F25

• Type: Journal
• Year: 2010
• Where: MLQ
• Authors: Jaime Gaspar, Paulo Oliva
• Keywords: Functional Interpretation, Intuitionistic Linear Logic, MLQ 2010, Realizability