Functional interpretation of Aczel's constructive set theory

Annals of Pure and Applied Logic 104 (1-3):31-73 (2000)
  Copy   BIBTEX

Abstract

In the present paper we give a functional interpretation of Aczel's constructive set theories CZF − and CZF in systems T ∈ and T ∈ + of constructive set functionals of finite types. This interpretation is obtained by a translation × , a refinement of the ∧ -translation introduced by Diller and Nahm 49–66) which again is an extension of Gödel's Dialectica translation. The interpretation theorem gives characterizations of the definable set functions of CZF − and CZF in terms of constructive set functionals. In a second part we introduce constructive set theories in all finite types. We expand the interpretation to these theories and give a characterization of the translation × . We further show that the simplest non-trivial axiom of extensionality is not interpretable by functionals of T ∈ and T ∈ + . We obtain this result by adapting Howard's notion of hereditarily majorizable functionals to set functionals. Subject of the last section is the translation ∨ that is defined in Burr for an interpretation of Kripke-Platek set theory with infinity

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 90,593

External links

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

Through your library

Similar books and articles

The natural numbers in constructive set theory.Michael Rathjen - 2008 - Mathematical Logic Quarterly 54 (1):83-97.
The strength of some Martin-Löf type theories.Edward Griffor & Michael Rathjen - 1994 - Archive for Mathematical Logic 33 (5):347-385.
Rudimentary and arithmetical constructive set theory.Peter Aczel - 2013 - Annals of Pure and Applied Logic 164 (4):396-415.
Aspects of general topology in constructive set theory.Peter Aczel - 2006 - Annals of Pure and Applied Logic 137 (1-3):3-29.
The Relation Reflection Scheme.Peter Aczel - 2008 - Mathematical Logic Quarterly 54 (1):5-11.
Unifying Functional Interpretations.Paulo Oliva - 2006 - Notre Dame Journal of Formal Logic 47 (2):263-290.
A note on the monotone functional interpretation.Ulrich Kohlenbach - 2011 - Mathematical Logic Quarterly 57 (6):611-614.
Godel's interpretation of intuitionism.William Tait - 2006 - Philosophia Mathematica 14 (2):208-228.

Analytics

Added to PP
2014-01-16

Downloads
12 (#929,405)

6 months
1 (#1,040,386)

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.
The natural numbers in constructive set theory.Michael Rathjen - 2008 - Mathematical Logic Quarterly 54 (1):83-97.
Hybrids of the ×-translation for CZF ω.Dominic Schulte - 2008 - Journal of Applied Logic 6 (3):443-458.
Logical problems of functional interpretations.Justus Diller - 2002 - Annals of Pure and Applied Logic 114 (1-3):27-42.

View all 8 citations / Add more citations