Publication details

Saarland University Computer Science

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

Dominik Kirst, Gert Smolka

Journal of Automated Reasoning, 2018

We formalise second-order ZF set theory in the dependent type theory of Coq. Assuming excluded middle, we prove Zermelo’s embedding theorem for models, categoricity in all cardinalities, and the categoricity of extended axiomatisations fixing the number of Grothendieck universes. These results are based on an inductive definition of the cumulative hierarchy eliminating the need for ordinals and set-theoretic transfinite recursion. Following Aczel’s sets-as-trees interpretation, we give a concise construction of an intensional model of second-order ZF with a weakened replacement axiom. Whereas this construction depends on no additional logical axioms, we obtain intensional and extensional models with full replacement assuming a description operator for trees and a weak form of proof irrelevance. In fact, these assumptions yield large models with n Grothendieck universes for every number n.

Link to Coq formalisation - SpringerLink

Download PDF        Show BibTeX               


Login to edit


Legal notice, Privacy policy