Proof interpretations with truth

12 years 8 months ago
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
Jaime Gaspar, Paulo Oliva
Added 29 Jan 2011
Updated 29 Jan 2011
Type Journal
Year 2010
Where MLQ
Authors Jaime Gaspar, Paulo Oliva
Comments (0)