Premium
Proof interpretations with truth
Author(s) -
Gaspar Jaime,
Oliva Paulo
Publication year - 2010
Publication title -
mathematical logic quarterly
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.473
H-Index - 28
eISSN - 1521-3870
pISSN - 0942-5616
DOI - 10.1002/malq.200910112
Subject(s) - realizability , interpretation (philosophy) , truth function , bounded function , mathematics , truth value , relation (database) , intuitionistic logic , linear logic , discrete mathematics , computer science , algorithm , propositional calculus , data mining , programming language , mathematical analysis
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)