Sets in Types, Types in Sets Export

@misc{citeulike:969587, abstract = {. We present two mutual encodings, respectively of the Calculus of Inductive Constructions in Zermelo-Fraenkel set theory and the opposite way. More precisely, we actually construct two families of encodings, relating the number of universes in the type theory with the number of inaccessible cardinals in the set theory. The main result is that both hierarchies of logical formalisms interleave w.r.t. expressive power and thus are essentially equivalent. Both encodings are quite elementary: type...}, author = {Werner, Benjamin}, citeulike-article-id = {969587}, citeulike-linkout-0 = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.55.1709}, keywords = {calculus-of-construction, coq, zfc}, posted-at = {2008-06-12 15:31:49}, priority = {2}, title = {Sets in Types, Types in Sets}, url = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.55.1709} }

TY - GEN ID - citeulike:969587 L3 - citeulike-article-id:969587 N2 - . We present two mutual encodings, respectively of the Calculus of Inductive Constructions in Zermelo-Fraenkel set theory and the opposite way. More precisely, we actually construct two families of encodings, relating the number of universes in the type theory with the number of inaccessible cardinals in the set theory. The main result is that both hierarchies of logical formalisms interleave w.r.t. expressive power and thus are essentially equivalent. Both encodings are quite elementary: type... TI - Sets in Types, Types in Sets KW - calculus-of-construction KW - coq KW - zfc AU - Werner, Benjamin UR - http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.55.1709 ER -