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

  • Dominik KirstEmail author
  • Gert Smolka


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.


Dependent type theory Second-order set theory Categoricity Model constructions Sets-as-trees interpretation Coq 



This research benefited from a quotient construction yielding the extensional model \(\mathcal {S} _i\) first formalised by Chad E. Brown in Coq using a full choice axiom. We also thank the anonymous reviewers for their helpful comments and suggestions that improved the final version of this paper.


  1. 1.
    Aczel, P.: The type theoretic interpretation of constructive set theory. Stud. Logic Found. Math. 96, 55–66 (1978)MathSciNetCrossRefGoogle Scholar
  2. 2.
    Aczel, P.: On Relating Type Theories and Set Theories. Types for Proofs and Programs. Lecture Notes in Computer Science, pp. 1–18. Springer, Berlin (1998)Google Scholar
  3. 3.
    Barbanera, F., Berardi, S.: Proof-irrelevance out of excluded-middle and choice in the calculus of constructions. J. Funct. Program. 6(3), 519–525 (1996)MathSciNetCrossRefGoogle Scholar
  4. 4.
    Barras, B.: Sets in Coq, Coq in sets. J. Formaliz. Reason. 3(1), 29–48 (2010)MathSciNetzbMATHGoogle Scholar
  5. 5.
    Bauer, A., Gross, J., Lumsdaine, P.L., Shulman, M., Sozeau, M., Spitters, B.: The HoTT library: a formalization of homotopy type theory in Coq. In: CPP 2017. ACM, New York, NY, USA, pp. 164–172 (2017)Google Scholar
  6. 6.
    Bourbaki, N.: Sur le théorème de Zorn. Archiv der Math. 2(6), 434–437 (1949)MathSciNetCrossRefGoogle Scholar
  7. 7.
    Coquand, T.: Metamathematical investigations of a calculus of constructions (1989)RR-1088, INRIA,<inria-00075471>Google Scholar
  8. 8.
    Gylterud, H.R.: From multisets to sets in hotmotopy type theory (2016). arXiv: 1612.05468
  9. 9.
    Hamkins, J.D.: Every countable model of set theory embeds into its own constructible universe. J. Math. Logic 13(02), 1350006 (2013)MathSciNetCrossRefGoogle Scholar
  10. 10.
    Hrbacek, K., Jech, T.: Introduction to Set Theory, Revised and Expanded, 3rd edn. CRC Press, Boca Raton (1999)zbMATHGoogle Scholar
  11. 11.
    Kirst, D., Smolka, G.: Categoricity results for second-order ZF in dependent type theory. In: Ayala-Rincón, M., Muñoz, C.A. (eds.) ITP 2017, Brasília, Brazil, September 26–29, 2017, Vol. 10499 of LNCS. Springer, pp. 304–318 (2017)Google Scholar
  12. 12.
    Kirst, D., Smolka, G.: Large model constructions for second-order ZF in dependent type theory. In: Andronick, J., Felty, A.P. (eds.) CPP 2018, Los Angeles, CA, USA, January 8–9, 2018. ACM, pp. 228–239 (2018)Google Scholar
  13. 13.
    Kreisel, G.: Two notes on the foundations of set-theory. Dialectica 23(2), 93–114 (1969)CrossRefGoogle Scholar
  14. 14.
    Kunen, K.: Set Theory: An Introduction to Independence Proofs. Elsevier, New York (2014)zbMATHGoogle Scholar
  15. 15.
    Ledent, J.: Modeling set theory in homotopy type theory (2014).
  16. 16.
    Paulson, L.C.: Set theory for verification: I. From foundations to functions. J. Autom. Reason. 11(3), 353–389 (1993)MathSciNetCrossRefGoogle Scholar
  17. 17.
    Scott, D.: Axiomatizing set theory. Proc. Symp. Pure Math. 13, 207–214 (1974)MathSciNetCrossRefGoogle Scholar
  18. 18.
    Skolem, T.: Some remarks on axiomatized set theory. In: van Heijenoort, J. (ed) From Frege to Gödel: A Sourcebook in Mathematical Logic. toExcel, Lincoln, NE, USA, pp. 290–301 (1922)Google Scholar
  19. 19.
    Smolka, G., Schäfer, S., Doczkal, C.: Transfinite constructions in classical type theory. In: Zhang, X., Urban, C. (eds.) ITP 2015, Nanjing, China, August 24–27, 2015, LNCS 9236. Springer (2015)Google Scholar
  20. 20.
    Smullyan, R.M., Fitting, M.: Set Theory and the Continuum Problem. Dover Books on Mathematics. Dover Publications, New York (2010)Google Scholar
  21. 21.
    Sozeau, M., Tabareau, N.: Universe Polymorphism in Coq. Interactive Theorem Proving. Lecture Notes in Computer Science, pp. 499–514. Springer, Cham (2014)zbMATHGoogle Scholar
  22. 22.
    Suppes, P.: Axiomatic Set Theory. Dover Books on Mathematics Series. Dover Publications, New York (1960)Google Scholar
  23. 23.
    The Coq Proof Assistant. (2018)
  24. 24.
    T. Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study. (2013)
  25. 25.
    Uzquiano, G.: Models of second-order Zermelo set theory. Bull. Symb. Logic 5(3), 289–302 (1999)MathSciNetCrossRefGoogle Scholar
  26. 26.
    Väänänen, J.: Second-order logic or set theory? Bull. Symb. Logic 18(1), 91–121 (2012)MathSciNetCrossRefGoogle Scholar
  27. 27.
    Werner, B.: Sets in types, types in sets. In: Theoretical Aspects of Computer Software. Springer, Heidelberg, pp. 530–546 (1997)Google Scholar
  28. 28.
    Williams, N.H.: On Grothendieck universes. Compos. Math. 21(1), 1–3 (1969)MathSciNetzbMATHGoogle Scholar
  29. 29.
    Zermelo, E.: Neuer Beweis für die Möglichkeit einer Wohlordnung. Math. Ann. 65, 107–128 (1908)CrossRefGoogle Scholar
  30. 30.
    Zermelo, E.: Über Grenzzahlen und Mengenbereiche: Neue Untersuchungen über die Grundlagen der Mengenlehre. Fundam. Math. 16, 29–47 (1930)CrossRefGoogle Scholar

Copyright information

© Springer Nature B.V. 2018

Authors and Affiliations

  1. 1.Saarland UniversitySaarbrückenGermany

Personalised recommendations