Proof interpretations with truth

&
Mathematical Logic Quarterly 56 (6):591-610 (2010)
  Copy   BIBTEX

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

Categories

Keywords

Reprint years

DOI

10.1002/malq.200910112

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 91,349

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

My notes

Similar books and articles

Unifying Functional Interpretations.Paulo Oliva - 2006 - Notre Dame Journal of Formal Logic 47 (2):263-290.
Confined modified realizability.Gilda Ferreira & Paulo Oliva - 2010 - Mathematical Logic Quarterly 56 (1):13-28.
A general notion of realizability.Lars Birkedal - 2002 - Bulletin of Symbolic Logic 8 (2):266-282.
Existence, proof and truth-making: A perspective on the intuitionistic conception of truth.Göran Sundholm - 1994 - Topoi 13 (2):117-126.
Lifschitz realizability for intuitionistic Zermelo–Fraenkel set theory.Ray-Ming Chen & Michael Rathjen - 2012 - Archive for Mathematical Logic 51 (7-8):789-818.
On the linear decoration of intuitionistic derivations.Vincent Danos, Jean-Baptiste Joinet & Harold Schellinx - 1995 - Archive for Mathematical Logic 33 (6):387-412.
The logic of bunched implications.Peter W. O'Hearn & David J. Pym - 1999 - Bulletin of Symbolic Logic 5 (2):215-244.
An analysis of gödel's dialectica interpretation via linear logic.Paulo Oliva - 2008 - Dialectica 62 (2):269–290.
The Friedman—Sheard programme in intuitionistic logic.Graham E. Leigh & Michael Rathjen - 2012 - Journal of Symbolic Logic 77 (3):777-806.
Review: S. C. Kleene, Realizability; S. C. Kleene, Realizability. [REVIEW]Donald L. Kreider - 1962 - Journal of Symbolic Logic 27 (2):242-243.
Frege structures and the notions of truth and proposition.P. Aczel - 1980 - In J. Barwise, H. J. Keisler & K. Kunen (eds.), The Kleene Symposium. North-Holland.
Frege Structures and the notions of proposition, truth and set.Peter Aczel - 1980 - Journal of Symbolic Logic 51 (1):244-246.

Analytics

Added to PP
2013-12-01

Downloads
18 (#808,169)

6 months
4 (#818,853)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

A parametrised functional interpretation of Heyting arithmetic.Bruno Dinis & Paulo Oliva - 2021 - Annals of Pure and Applied Logic 172 (4):102940.

Add more citations

References found in this work

Bounded functional interpretation.Fernando Ferreira & Paulo Oliva - 2005 - Annals of Pure and Applied Logic 135 (1):73-112.
Pointwise hereditary majorization and some applications.Ulrich Kohlenbach - 1992 - Archive for Mathematical Logic 31 (4):227-241.
Relative constructivity.Ulrich Kohlenbach - 1998 - Journal of Symbolic Logic 63 (4):1218-1238.
Bounded Modified Realizability.Fernando Ferreira & Ana Nunes - 2006 - Journal of Symbolic Logic 71 (1):329 - 346.

View all 9 references / Add more references