Skip to main content
SpringerLink
Log in

Transfinite Constructions in Classical Type Theory

  • Conference paper
  • First Online:
Interactive Theorem Proving (ITP 2015)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 9236))

Included in the following conference series:

Abstract

We study a transfinite construction we call tower construction in classical type theory. The construction is inductive and applies to partially ordered types. It yields the set of all points reachable from a starting point with an increasing successor function and a family of admissible suprema. Based on the construction, we obtain type-theoretic versions of the theorems of Zermelo (well-orderings), Hausdorff (maximal chains), and Bourbaki and Witt (fixed points). The development is formalized in Coq assuming excluded middle.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    Our initial motivation for studying the general tower construction was the direct construction of the cumulative hierarchy in axiomatic set theory. Only after finishing the proofs for the general tower construction in type theory, we discovered Bourbaki’s marvelous presentation [2] of the tower construction in set theory.

References

  1. Bauer, A., Lumsdaine, P.L.: On the Bourbaki-Witt principle in toposes. Math. Proc. Camb. Philos. Soc. 155, 87–99 (2013)

    Article  MATH  MathSciNet  Google Scholar 

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

    Article  MATH  MathSciNet  Google Scholar 

  3. Felscher, W.: Doppelte Hülleninduktion und ein Satz von Hessenberg und Bourbaki. Archiv der Mathematik 13(1), 160–165 (1962)

    Article  MATH  MathSciNet  Google Scholar 

  4. Halmos, P.R.: Naive Set Theory. Springer, New York (1960)

    MATH  Google Scholar 

  5. Hausdorff, F.: Grundzüge der Mengenlehre. Viet, Leipzig (1914). English translation appeared with AMS Chelsea Publishing

    Google Scholar 

  6. Hessenberg, G.: Kettentheorie und Wahlordnung. Journal für die reine und Angewandte Mathematik 135, 81–133 (1909)

    MathSciNet  Google Scholar 

  7. Ilik, D.: Zermelo’s well-ordering theorem in type theory. In: Altenkirch, T., McBride, C. (eds.) TYPES 2006. LNCS, vol. 4502, pp. 175–187. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  8. Isabelle/HOL: a generic proof assistant (2015). http://isabelle.in.tum.de

  9. Lang, S.: Algebra. Graduate Texts in Mathematics, 3rd edn. Springer, New York (2002)

    Book  MATH  Google Scholar 

  10. van Heijenoort, J.: From Frege to Gödel: a source book in mathematical logic. Harvard University Press, Cambridge (1967)

    MATH  Google Scholar 

  11. Witt, E.: Beweisstudien zum Satz von M. Zorn. Mathematische Nachrichten 4(1–6), 434–438 (1950)

    Article  MathSciNet  Google Scholar 

  12. Zermelo, E.: Beweis, daß jede Menge wohlgeordnet werden kann. (Aus einem an Herrn Hilbert gerichteten Briefe). Mathematische Annalen 59, 514–516 (1904). English translation in [10]

    Article  MathSciNet  Google Scholar 

  13. Zermelo, E.: Neuer Beweis für die Möglichkeit einer Wohlordnung. Mathematische Annalen 65, 107–128 (1908). English translation in [10]

    Article  MATH  Google Scholar 

Download references

Acknowledgement

It was Chad E. Brown who got us interested in the topic of this paper when in February 2014 he came up with a surprisingly small Coq formalization of Zermelo’s second proof of the well-ordering theorem using an inductive definition for the least \(\varTheta \)-chain. In May 2015, Frédéric Blanqui told us about the papers of Felscher and Hessenberg in Tallinn.

Author information

Authors and Affiliations

  1. Saarland University, Saarbrücken, Germany

    Gert Smolka, Steven Schäfer & Christian Doczkal

Authors
  1. Gert Smolka
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Steven Schäfer
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Christian Doczkal
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Gert Smolka .

Editor information

Editors and Affiliations

  1. Department of Informatics, King's College London, London, United Kingdom

    Christian Urban

  2. PLA University of Science and Technology, Nanjing, China

    Xingyuan Zhang

Rights and permissions

Reprints and permissions

Copyright information

© 2015 Springer International Publishing Switzerland

About this paper

Cite this paper

Smolka, G., Schäfer, S., Doczkal, C. (2015). Transfinite Constructions in Classical Type Theory. In: Urban, C., Zhang, X. (eds) Interactive Theorem Proving. ITP 2015. Lecture Notes in Computer Science(), vol 9236. Springer, Cham. https://doi.org/10.1007/978-3-319-22102-1_26

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-22102-1_26

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-22101-4

  • Online ISBN: 978-3-319-22102-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation