nach oben

Journal of Automated Reasoning

Erschienen in:

11.10.2018

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

verfasst von: Dominik Kirst, Gert Smolka

Erschienen in: Journal of Automated Reasoning | Ausgabe 2/2019

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

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.

Vorheriger Artikel Call-by-Value Lambda Calculus as a Model of Computation in Coq

Nächster Artikel Effect Polymorphism in Higher-Order Logic (Proof Pearl)

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

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!

Jetzt informieren

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!

Jetzt informieren

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!

Jetzt informieren

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

Titel: Categoricity Results and Large Model Constructions for Second-Order ZF in Dependent Type Theory
verfasst von: Dominik Kirst
Gert Smolka
Publikationsdatum: 11.10.2018
Verlag: Springer Netherlands
Erschienen in: Journal of Automated Reasoning / Ausgabe 2/2019
Print ISSN: 0168-7433
Elektronische ISSN: 1573-0670
DOI: https://doi.org/10.1007/s10817-018-9480-6

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Wirtschaft"

Springer Professional "Technik"

Weitere Artikel der Ausgabe 2/2019

Formalization of the Fundamental Group in Untyped Set Theory Using Auto2

From Signatures to Monads in UniMath

Verifying a Concurrent Garbage Collector with a Rely-Guarantee Methodology

The Univalence Axiom in Cubical Sets

A Formalization of Convex Polyhedra Based on the Simplex Method

Preface: Special Issue on Homotopy Type Theory and Univalent Foundations