Proof interpretations with truth
Jaime Gaspar, Paulo B. Oliva · Mathematical logic quarterly · 2010
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)