Proof interpretations with truth

被引：3
|
作者：
Gaspar, Jaime [1 ]
Oliva, Paulo [2 ]
机构：
[1] Tech Univ Darmstadt, Fachbereich Math, D-64289 Darmstadt, Germany
[2] Queen Mary Univ London, Sch Elect Engn & Comp Sci, London E1 4NS, England
来源：
MATHEMATICAL LOGIC QUARTERLY | 2010年 / 56卷 / 06期
关键词：
Modified realizability with truth and q-variant; intuitionistic linear logic; Aczel and Kleene slashes; CLASSICAL LINEAR LOGIC; FUNCTIONAL INTERPRETATIONS; MODIFIED REALIZABILITY;
D O I：
10.1002/malq.200910112
中图分类号：
O1 [数学];
学科分类号：
0701 ; 070101 ;
摘要：
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 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. (C) 2010 WILEY-VCH Verlag GmbH & Co. KGaA, Weinheim
引用
收藏
页码：591 / 610
页数：20
相关论文
共 50 条
12345