Publication details
Categoricity Results for Second-Order ZF in Dependent Type Theory
Dominik Kirst, Gert Smolka
Interactive Theorem Proving - 8th International Conference, ITP 2017, Brasilia, Brazil, September 26-29, 2017, September 2017
We formalise the axiomatic set theory second-order ZF in the constructive type theory of Coq assuming excluded middle. In this setting we prove Zermelo's embedding theorem for models, categoricity in all cardinalities, and the correspondence of inner models and Grothendieck universes. Our results are based on an inductive definition of the cumulative hierarchy eliminating the need for ordinals and transfinite recursion.
Link to Coq Formalisation
Download PDF
Show BibTeX
@INPROCEEDINGS{KirstSmolka:2017:Categoricity,
title = {Categoricity Results for Second-Order ZF in Dependent Type Theory},
author = {Dominik Kirst and Gert Smolka},
year = {2017},
month = {Sep},
booktitle = {Interactive Theorem Proving - 8th International Conference, ITP 2017, Brasilia, Brazil, September 26-29, 2017},
}
Login to edit
Legal notice, Privacy policy
