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.

Tue 9 Jan

CPP-2018
13:30 - 15:30: CPP 2018 - Type Theory, Set Theory, and Formalized Mathematics at Museum A
Chair(s): Thorsten AltenkirchUniversity of Nottingham
CPP-201813:30 - 14:00
Talk
Dan FruminRadboud University, Herman GeuversRadboud University Nijmegen, Netherlands, Léon GondelmanLRI, Université Paris-Sud, Niels van der WeideRadboud University Nijmegen, Netherlands
DOI
CPP-201814:00 - 14:30
Talk
Denis FirsovUniversity of Iowa, USA, Aaron StumpUniversity of Iowa, USA
DOI
CPP-201814:30 - 15:00
Talk
Dominik KirstSaarland University, Gert SmolkaSaarland University
DOI
CPP-201815:00 - 15:30
Talk