%0 Book Section %1 aczel1986theoretic %A Aczel, Peter %B Logic, Methodology and Philosophy of Science VII Proceedings of the Seventh International Congress of Logic, Methodology and Philosophy of Science %D 1986 %E Ruth Barcan Marcus, Georg J.W. Dorn %E Weingartner, Paul %I Elsevier %K constructive set type %P 17 - 49 %R http://dx.doi.org/10.1016/S0049-237X(09)70683-4 %T The Type Theoretic Interpretation of Constructive Set Theory: Inductive Definitions %U http://www.sciencedirect.com/science/article/pii/S0049237X09706834 %V 114 %X Publisher Summary Constructive set theory is a possible framework for the formalization of constructive mathematics. The chapter describes the formal system CZF+DC and its type theoretic interpretation. An inductive definition usually involves the characterization of a collection of objects as the smallest collection satisfying certain closure conditions. Such a characterization can be made explicit in one of at least two ways. The first way is to define the collection as the intersection of all collections that satisfies the closure conditions. Such an explicit definition is thoroughly impredicative in that the collection is defined using quantification over all collections. The second way is to build up the collection from below as the union of a hierarchy of stages. These stages of the inductive definition are indexed using some suitable notion of “ordinal.” The paradigm for a direct understanding of an inductive definition is that for the collection of natural numbers, which is characterized as the smallest collection containing zero and closed under the successor function.

@incollection{aczel1986theoretic, abstract = {Publisher Summary Constructive set theory is a possible framework for the formalization of constructive mathematics. The chapter describes the formal system CZF+DC and its type theoretic interpretation. An inductive definition usually involves the characterization of a collection of objects as the smallest collection satisfying certain closure conditions. Such a characterization can be made explicit in one of at least two ways. The first way is to define the collection as the intersection of all collections that satisfies the closure conditions. Such an explicit definition is thoroughly impredicative in that the collection is defined using quantification over all collections. The second way is to build up the collection from below as the union of a hierarchy of stages. These stages of the inductive definition are indexed using some suitable notion of “ordinal.” The paradigm for a direct understanding of an inductive definition is that for the collection of natural numbers, which is characterized as the smallest collection containing zero and closed under the successor function. }, added-at = {2014-11-25T12:54:56.000+0100}, author = {Aczel, Peter}, biburl = {https://www.bibsonomy.org/bibtex/2543c5577ba9a7862d770f4075d524af3/t.uemura}, booktitle = {Logic, Methodology and Philosophy of Science VII Proceedings of the Seventh International Congress of Logic, Methodology and Philosophy of Science}, description = {The Type Theoretic Interpretation of Constructive Set Theory: Inductive Definitions}, doi = {http://dx.doi.org/10.1016/S0049-237X(09)70683-4}, editor = {Ruth Barcan Marcus, Georg J.W. Dorn and Weingartner, Paul}, interhash = {892cccdb93b530a3e78bd5502c85a919}, intrahash = {543c5577ba9a7862d770f4075d524af3}, issn = {0049-237X}, keywords = {constructive set type}, pages = {17 - 49}, publisher = {Elsevier}, series = {Studies in Logic and the Foundations of Mathematics }, timestamp = {2014-11-25T12:54:56.000+0100}, title = {The Type Theoretic Interpretation of Constructive Set Theory: Inductive Definitions }, url = {http://www.sciencedirect.com/science/article/pii/S0049237X09706834}, volume = 114, year = 1986 }