Publication details

Saarland University Computer Science

Large Model Constructions for Second-Order ZF in Dependent Type Theory

Dominik Kirst, Gert Smolka

Certified Programs and Proofs - 7th International Conference, CPP 2018, Los Angeles, USA, January 8-9, 2018, January 2018 (to appear)

We study various models of classical second-order set theories in the dependent type theory of Coq. Without logical assumptions, Aczel's sets-as-trees interpretation yields an intensional model of second-order ZF with functional replacement. Building on work of Werner and Barras, we discuss the need for quotient axioms in order to obtain extensional models with relational replacement and to construct large sets. Specifically, we show that the consistency strength of Coq extended by excluded middle and a description operator on well-founded trees allows for constructing models with exactly n Grothendieck universes for every natural number n. By a previous categoricity result based on Zermelo's embedding theorem, it follows that those models are unique up to isomorphism. Moreover, we show that the smallest universe contains exactly the hereditarily finite sets and give a concise independence proof of the foundation axiom based on permutation models.

Link to Coq formalisation

Download PDF        Show BibTeX               

Login to edit

Webmaster, Wed Sep 16 10:47:00 2009