Abstract
We axiomatize hereditarily finite sets in constructive type theory and show that all models of the axiomatization are isomorphic. The axiomatization takes the empty set and adjunction as primitives and comes with a strong induction principle. Based on the axiomatization, we construct the set operations of ZF and develop the basic theory of finite ordinals and cardinality. We construct a model of the axiomatization as a quotient of an inductive type of binary trees. The development is carried out in Coq.
Cite
CITATION STYLE
Smolka, G., & Stark, K. (2016). Hereditarily finite sets in constructive type theory. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 9807 LNCS, pp. 374–390). Springer Verlag. https://doi.org/10.1007/978-3-319-43144-4_23
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
