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

Saarland University Computer Science

Dominik Kirst, Gert Smolka

We study various models of classical second-order set theories in 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 model contains exactly the hereditarily finite sets and give a constructive independence proof of the foundation axiom based on permutation models.


Coq Formalisation (Edited 11.10.2017, Coq 8.6)