Unifying Functional Interpretations

Notre Dame Journal of Formal Logic 47 (2):263-290 (2006)
  Copy   BIBTEX


This article presents a parametrized functional interpretation. Depending on the choice of two parameters one obtains well-known functional interpretations such as Gödel's Dialectica interpretation, Diller-Nahm's variant of the Dialectica interpretation, Kohlenbach's monotone interpretations, Kreisel's modified realizability, and Stein's family of functional interpretations. A functional interpretation consists of a formula interpretation and a soundness proof. I show that all these interpretations differ only on two design choices: first, on the number of counterexamples for A which became witnesses for ¬A when defining the formula interpretation and, second, the inductive information about the witnesses of A which is considered in the proof of soundness. Sufficient conditions on the parameters are also given which ensure the soundness of the resulting functional interpretation. The relation between the parametrized interpretation and the recent bounded functional interpretation is also discussed



    Upload a copy of this work     Papers currently archived: 84,179

External links

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

Through your library


Added to PP

22 (#553,190)

6 months
1 (#510,113)

Historical graph of downloads
How can I increase my downloads?