Functional interpretations of constructive set theory in all finite types

Dialectica 62 (2):149–177 (2008)
  Copy   BIBTEX


Gödel's dialectica interpretation of Heyting arithmetic HA may be seen as expressing a lack of confidence in our understanding of unbounded quantification. Instead of formally proving an implication with an existential consequent or with a universal antecedent, the dialectica interpretation asks, under suitable conditions, for explicit 'interpreting' instances that make the implication valid. For proofs in constructive set theory CZF-, it may not always be possible to find just one such instance, but it must suffice to explicitly name a set consisting of such interpreting instances. The aim of eliminating unbounded quantification in favor of appropriate constructive functionals will still be obtained, as our ∧-interpretation theorem for constructive set theory in all finite types CZFω- shows. By changing to a hybrid interpretation ∧q, we show closure of CZFω- under rules that – in stronger forms – have already been studied in the context of Heyting arithmetic. In a similar spirit, we briefly survey modified realizability of CZFω- and its hybrids. Central results of this paper have been proved by Burr 2000a and Schulte 2006, however, for different translations. We use a simplified interpretation that goes back to Diller and Nahm 1974. A novel element is a lemma on absorption of bounds which is essential for the smooth operation of our translation.



    Upload a copy of this work     Papers currently archived: 79,912

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 (#537,418)

6 months
1 (#479,283)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

From the weak to the strong existence property.Michael Rathjen - 2012 - Annals of Pure and Applied Logic 163 (10):1400-1418.

Add more citations

References found in this work

Mathematical Logic.Joseph R. Shoenfield - 1967 - Reading, MA, USA: Reading, Mass., Addison-Wesley Pub. Co..
Constructivism in mathematics: an introduction.A. S. Troelstra - 1988 - New York, N.Y.: Sole distributors for the U.S.A. and Canada, Elsevier Science Pub. Co.. Edited by D. van Dalen.
Constructive set theory.John Myhill - 1975 - Journal of Symbolic Logic 40 (3):347-382.
On the interpretation of intuitionistic number theory.S. C. Kleene - 1945 - Journal of Symbolic Logic 10 (4):109-124.

View all 20 references / Add more references