License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/DagSemProc.05021.23
URN: urn:nbn:de:0030-drops-2919
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2006/291/
Go to the corresponding Portal

Oliva, Paulo

Unifying Functional Interpretations

pdf-format:
05021.OlivaPaulo.Paper.291.pdf (0.3 MB)

Abstract

The purpose of this article is to present a parametrised functional interpretation. Depending on the choice of the two parameters one obtains well-known functional interpretations, among others Gödel's Dialectica interpretation, Diller-Nahm's variant of the Dialectica interpretation, Kreisel's modified realizability, Kohlenbach's monotone interpretations and Stein's family of functional interpretations. We show that all these interpretations only differ on two basic choices, which are captured by the parameters, namely the choices of (1) "how much" of the counter-examples for A becomes witnesses for the negation of A, and of (2) "how much" information about the witnesses of A one is interested in.

BibTeX - Entry

@InProceedings{oliva:DagSemProc.05021.23,
  author =	{Oliva, Paulo},
  title =	{{Unifying Functional Interpretations}},
  booktitle =	{Mathematics, Algorithms, Proofs},
  pages =	{1--20},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2006},
  volume =	{5021},
  editor =	{Thierry Coquand and Henri Lombardi and Marie-Fran\c{c}oise Roy},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2006/291},
  URN =		{urn:nbn:de:0030-drops-2919},
  doi =		{10.4230/DagSemProc.05021.23},
  annote =	{Keywords: Functional interpretation, modified realizability, Dialectica interpretation, intuitionistic logic}
}

Keywords: Functional interpretation, modified realizability, Dialectica interpretation, intuitionistic logic
Collection: 05021 - Mathematics, Algorithms, Proofs
Issue Date: 2006
Date of publication: 16.01.2006

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI