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. (shrink)

ZusammenfassungP. Bernays hat darauf hingewiesen, dass man, um die Widerspruchs freiheit der klassischen Zahlentheorie zu beweisen, den Hilbertschen flniter Standpunkt dadurch erweitern muss, dass man neben den auf Symbole sich beziehenden kombinatorischen Begriffen gewisse abstrakte Begriffe zulässt, Die abstrakten Begriffe, die bisher für diesen Zweck verwendet wurden, sinc die der konstruktiven Ordinalzahltheorie und die der intuitionistischer. Logik. Es wird gezeigt, dass man statt deesen den Begriff einer berechenbaren Funktion endlichen einfachen Typs über den natürlichen Zahler benutzen kann, wobei keine anderen (...) Konstruktionsverfahren für solche Funktionen nötig sind, als einfache Rekursion nach einer Zahlvariablen und Einsetzung von Funktionen ineinander .P. Bernays has pointed out that, in order to prove the consistency of classical number theory, it is necessary to extend Hilbert's finitary stand‐point by admitting certain abstract concepts in addition to the combinatorial concepts referring to symbols. The abstract concepts that so far have been used for this purpose are those of the constructive theory of ordinals and those of intuitionistic logic. It is shown that the concept of a computable function of finite simple type over the integers can be used instead, where no other procedures of constructing such functions are necessary except simple recursion by an integral variable and substitution of functions in each other. (shrink)

8.3 The consistency proof -- 8.4 Applications of the consistency proof -- 8.5 Second-order arithmetic -- Problems -- Chapter 9: Set Theory -- 9.1 Axioms for sets -- 9.2 Development of set theory -- 9.3 Ordinals -- 9.4 Cardinals -- 9.5 Interpretations of set theory -- 9.6 Constructible sets -- 9.7 The axiom of constructibility -- 9.8 Forcing -- 9.9 The independence proofs -- 9.10 Large cardinals -- Problems -- Appendix The Word Problem -- Index.

The present volume is intended as an all-round introduction to constructivism. Here constructivism is to be understood in the wide sense, and covers in particular Brouwer's intuitionism, Bishop's constructivism and A.A. Markov's constructive recursive mathematics. The ending "-ism" has ideological overtones: "constructive mathematics is the (only) right mathematics"; we hasten, however, to declare that we do not subscribe to this ideology, and that we do not intend to present our material on such a basis.

The aim of this article is to give an introduction to functional interpretations of set theory given by the authorin Burr (2000a). The first part starts with some general remarks on Gödel's functional interpretation with a focus on aspects related to problems that arise in the context of set theory. The second part gives an insight in the techniques needed to perform a functional interpretation of systems of set theory. However, the first part of this article is not intended to (...) be a complete survey of functional interpretations and here we recommend, for example, Avigad and Feferman (1998),Troelstra (1990) and Troelstra (1973). (shrink)

It is shown that functional interpretation can be used to show the existence property of intuitionistic number theory. On the basis of truth variants a comparison is then made between realisability and functional interpretation showing a structural difference between the two.

Gödel interpreted Heyting arithmetic HA in a “logic-free” fragment T 0 of his theory T of primitive recursive functionals of finite types by his famous Dialectica-translation D . This works because the logic of HA is extremely simple. If the logic of the interpreted system is different—in particular more complicated—, it forces us to look for different and more complicated functional translations. We discuss the arising logical problems for arithmetical and set theoretical systems from HA to CZF . We want (...) to test the thesis: While the functionals take care of the proof theoretic strength of the interpreted system, it is the functional translation that has to cope with the logical complexities of the system. (shrink)

It is shown that functional interpretation can be used to show the existence property of intuitionistic number theory. On the basis of truth variants a comparison is then made between realisability and functional interpretation showing a structural difference between the two.

The Dialectica-style functional interpretation of Kripke-Platek set theory with infinity (\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document} $\hbox{\sf KP} \omega$\end{document}) given in [1] uses a choice functional (which is not a definable set function of (\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document} $hbox{\sf KP} \omega$\end{document}). By means of a Diller-Nahm-style interpretation (cf. [4]) it is possible to eliminate the choice functional and give an interpretation by set functionals primitive recursive in \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} (...) \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document} $x\mapsto\omega$\end{document}. This yields the following characterization: The class of \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document} $\Sigma$\end{document}-definable set functions of \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document} $\hbox{\sf KP} \omega$\end{document} coincides with the collection of set functionals of type 1 primitive recursive in \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document} $x\mapsto \omega$\end{document}. (shrink)

The Dialectica-style functional interpretation of Kripke-Platek set theory with infinity ( $\hbox{\sf KP} \omega$ ) given in [1] uses a choice functional (which is not a definable set function of ( $hbox{\sf KP} \omega$ ). By means of a Diller-Nahm-style interpretation (cf. [4]) it is possible to eliminate the choice functional and give an interpretation by set functionals primitive recursive in $x\mapsto\omega$ . This yields the following characterization: The class of $\Sigma$ -definable set functions of $\hbox{\sf KP} \omega$ coincides with (...) the collection of set functionals of type 1 primitive recursive in $x\mapsto \omega$. (shrink)

The subject of this paper is a characterization of the $\Sigma_1$ -definable set functions of Kripke-Platek set theory with infinity and a uniform version of axiom of choice: $KP\omega+(uniform\;AC)$ . This class of functions is shown to coincide with the collection of set functionals of type 1 primitive recursive in a given choice functional and $x\mapsto\omega$ . This goal is achieved by a Gödel Dialectica-style functional interpretation of $KP\omega+(uniform\;AC)$ and a computability proof for the involved functionals.