Top

Journal of Automated Reasoning

Published in:

11-10-2018

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

Authors: Dominik Kirst, Gert Smolka

Published in: Journal of Automated Reasoning | Issue 2/2019

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

Abstract

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.

previous article Call-by-Value Lambda Calculus as a Model of Computation in Coq

next article Effect Polymorphism in Higher-Order Logic (Proof Pearl)

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

Aczel, P.: The type theoretic interpretation of constructive set theory. Stud. Logic Found. Math. 96, 55–66 (1978)MathSciNetMATHCrossRef

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)

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)MathSciNetMATHCrossRef

Barras, B.: Sets in Coq, Coq in sets. J. Formaliz. Reason. 3(1), 29–48 (2010)MathSciNetMATH

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)

Bourbaki, N.: Sur le théorème de Zorn. Archiv der Math. 2(6), 434–437 (1949)MathSciNetMATHCrossRef

Coquand, T.: Metamathematical investigations of a calculus of constructions (1989)RR-1088, INRIA,<inria-00075471>

Gylterud, H.R.: From multisets to sets in hotmotopy type theory (2016). arXiv: 1612.05468

Hamkins, J.D.: Every countable model of set theory embeds into its own constructible universe. J. Math. Logic 13(02), 1350006 (2013)MathSciNetMATHCrossRef

10.

Hrbacek, K., Jech, T.: Introduction to Set Theory, Revised and Expanded, 3rd edn. CRC Press, Boca Raton (1999)MATH

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)

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)

13.

Kreisel, G.: Two notes on the foundations of set-theory. Dialectica 23(2), 93–114 (1969)MATHCrossRef

14.

Kunen, K.: Set Theory: An Introduction to Independence Proofs. Elsevier, New York (2014)MATH

15.

Ledent, J.: Modeling set theory in homotopy type theory (2014). https://perso.ens-lyon.fr/jeremy.ledent/internship_report.pdf

16.

Paulson, L.C.: Set theory for verification: I. From foundations to functions. J. Autom. Reason. 11(3), 353–389 (1993)MathSciNetMATHCrossRef

17.

Scott, D.: Axiomatizing set theory. Proc. Symp. Pure Math. 13, 207–214 (1974)MathSciNetMATHCrossRef

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)

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)

20.

Smullyan, R.M., Fitting, M.: Set Theory and the Continuum Problem. Dover Books on Mathematics. Dover Publications, New York (2010)

21.

Sozeau, M., Tabareau, N.: Universe Polymorphism in Coq. Interactive Theorem Proving. Lecture Notes in Computer Science, pp. 499–514. Springer, Cham (2014)MATHCrossRef

22.

Suppes, P.: Axiomatic Set Theory. Dover Books on Mathematics Series. Dover Publications, New York (1960)

23.

The Coq Proof Assistant. http://coq.inria.fr (2018)

24.

T. Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study. https://homotopytypetheory.org/book (2013)

25.

Uzquiano, G.: Models of second-order Zermelo set theory. Bull. Symb. Logic 5(3), 289–302 (1999)MathSciNetMATHCrossRef

26.

Väänänen, J.: Second-order logic or set theory? Bull. Symb. Logic 18(1), 91–121 (2012)MathSciNetMATHCrossRef

27.

Werner, B.: Sets in types, types in sets. In: Theoretical Aspects of Computer Software. Springer, Heidelberg, pp. 530–546 (1997)

28.

Williams, N.H.: On Grothendieck universes. Compos. Math. 21(1), 1–3 (1969)MathSciNetMATH

29.

Zermelo, E.: Neuer Beweis für die Möglichkeit einer Wohlordnung. Math. Ann. 65, 107–128 (1908)MATHCrossRef

30.

Zermelo, E.: Über Grenzzahlen und Mengenbereiche: Neue Untersuchungen über die Grundlagen der Mengenlehre. Fundam. Math. 16, 29–47 (1930)MATHCrossRef

Title: Categoricity Results and Large Model Constructions for Second-Order ZF in Dependent Type Theory
Authors: Dominik Kirst
Gert Smolka
Publication date: 11-10-2018
Publisher: Springer Netherlands
Published in: Journal of Automated Reasoning / Issue 2/2019
Print ISSN: 0168-7433
Electronic ISSN: 1573-0670
DOI: https://doi.org/10.1007/s10817-018-9480-6

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Wirtschaft"

Springer Professional "Technik"

Other articles of this Issue 2/2019

From Signatures to Monads in UniMath

The Univalence Axiom in Cubical Sets

CompCertS: A Memory-Aware Verified C Compiler Using a Pointer as Integer Semantics

Canonicity for Cubical Type Theory

A Formal Proof of the Expressiveness of Deep Learning

Preface: Special Issue on Homotopy Type Theory and Univalent Foundations

Premium Partner