Document Open Access Logo

Higher-Order Tarski Grothendieck as a Foundation for Formal Proof

Authors Chad E. Brown, Cezary Kaliszyk , Karol Pąk

PDF
Thumbnail PDF

File

LIPIcs.ITP.2019.9.pdf
  • Filesize: 0.5 MB
  • 16 pages

Document Identifiers

Author Details

Chad E. Brown
  • Czech Technical University in Prague, Czech Republic
Cezary Kaliszyk
  • University of Innsbruck, Austria
  • University of Warsaw, Poland
Karol Pąk
  • University of Białystok, Poland

Funding

  • Brown, Chad E.: European Research Council (ERC) grant no. 649043 AI4REASON
  • Kaliszyk, Cezary: European Research Council (ERC) grant no. 714034 SMART
  • Pąk, Karol: Polish National Science Center granted by decision no. DEC-2015/19/D/ST6/01473

Cite As Get BibTex

Chad E. Brown, Cezary Kaliszyk, and Karol Pąk. Higher-Order Tarski Grothendieck as a Foundation for Formal Proof. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 9:1-9:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019) https://doi.org/10.4230/LIPIcs.ITP.2019.9

Abstract

We formally introduce a foundation for computer verified proofs based on higher-order Tarski-Grothendieck set theory. We show that this theory has a model if a 2-inaccessible cardinal exists. This assumption is the same as the one needed for a model of plain Tarski-Grothendieck set theory. The foundation allows the co-existence of proofs based on two major competing foundations for formal proofs: higher-order logic and TG set theory. We align two co-existing Isabelle libraries, Isabelle/HOL and Isabelle/Mizar, in a single foundation in the Isabelle logical framework. We do this by defining isomorphisms between the basic concepts, including integers, functions, lists, and algebraic structures that preserve the important operations. With this we can transfer theorems proved in higher-order logic to TG set theory and vice versa. We practically show this by formally transferring Lagrange’s four-square theorem, Fermat 3-4, and other theorems between the foundations in the Isabelle framework.

Subject Classification

ACM Subject Classification
  • Theory of computation → Interactive proof systems
  • Theory of computation → Logic and verification
Keywords
  • model
  • higher-order
  • Tarski Grothendieck
  • proof foundation

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Supplementary Materials

References

  1. P. B. Andrews. An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof. Kluwer Academic Publishers, 2nd edition, 2002. Google Scholar
  2. Peter B. Andrews. General Models and Extensionality. J. Symb. Log., 37:395-397, 1972. Google Scholar
  3. Ali Assaf. A framework for defining computational higher-order logics. (Un cadre de définition de logiques calculatoires d'ordre supérieur). PhD thesis, École Polytechnique, Palaiseau, France, 2015. URL: https://tel.archives-ouvertes.fr/tel-01235303.
  4. Ali Assaf and Raphaël Cauderlier. Mixing HOL and Coq in Dedukti. In Cezary Kaliszyk and Andrei Paskevich, editors, Proof eXchange for Theorem Proving (PxTP 2015), volume 186 of EPTCS, pages 89-96, 2015. Google Scholar
  5. Julian Backes and Chad E. Brown. Analytic Tableaux for Higher-Order Logic with Choice. Journal of Automated Reasoning, 47(4):451-479, 2011. Google Scholar
  6. Grzegorz Bancerek, Czesław Byliński, Adam Grabowski, Artur Korniłowicz, Roman Matuszewski, Adam Naumowicz, and Karol Pąk. The Role of the Mizar Mathematical Library for Interactive Proof Development in Mizar. Journal of Automated Reasoning, 2017. URL: https://doi.org/10.1007/s10817-017-9440-6.
  7. Grzegorz Bancerek and Piotr Rudnicki. A Compendium of Continuous Lattices in MIZAR. J. Autom. Reasoning, 29(3-4):189-224, 2002. URL: http://doi.org/10.1023/A:1021966832558.
  8. Christoph Benzmüller, Chad E. Brown, and Michael Kohlhase. Higher-order semantics and extensionality. J. Symb. Log., 69:1027-1088, 2004. Google Scholar
  9. Jasmin Christian Blanchette, Maximilian Haslbeck, Daniel Matichuk, and Tobias Nipkow. Mining the Archive of Formal Proofs. In Manfred Kerber, Jacques Carette, Cezary Kaliszyk, Florian Rabe, and Volker Sorge, editors, Intelligent Computer Mathematics (CICM 2015), volume 9150 of LNCS, pages 3-17. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-20615-8_1.
  10. Chad E. Brown. The Egal Manual, 2014. URL: http://grid01.ciirc.cvut.cz/~chad/egalmanual.pdf.
  11. Chad E. Brown and Gert Smolka. Analytic Tableaux for Simple Type Theory and its First-Order Fragment. Logical Methods in Computer Science, 6(2), June 2010. Google Scholar
  12. Alonzo Church. A Formulation of the Simple Theory of Types. J. Symb. Log., 5:56-68, 1940. Google Scholar
  13. Thibault Gauthier and Cezary Kaliszyk. Sharing HOL4 and HOL Light Proof Knowledge. In Martin Davis, Ansgar Fehnker, Annabelle McIver, and Andrei Voronkov, editors, 20th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2015), volume 9450 of Lecture Notes in Computer Science, pages 372-386. Springer, 2015. URL: https://doi.org/10.1007/978-3-662-48899-7_26.
  14. Thibault Gauthier and Cezary Kaliszyk. Aligning Concepts across Proof Assistant Libraries. J. Symbolic Computation, 90:89-123, 2019. URL: https://doi.org/10.1016/j.jsc.2018.04.005.
  15. Michael Gordon. Set Theory, Higher Order Logic or Both? In Joakim von Wright, Jim Grundy, and John Harrison, editors, Theorem Proving in Higher Order Logics, TPHOLs'96, volume 1125 of LNCS, pages 191-201. Springer, 1996. URL: https://doi.org/10.1007/BFb0105405.
  16. Adam Grabowski, Artur Korniłowicz, and Adam Naumowicz. Four Decades of Mizar. Journal of Automated Reasoning, 55(3):191-198, 2015. URL: https://doi.org/10.1007/s10817-015-9345-1.
  17. A. Grothendieck and J.-L. Verdier. Théorie des topos et cohomologie étale des schémas - (SGA 4) - vol. 1, volume 269 of Lecture notes in mathematics. Springer-Verlag, 1972. Google Scholar
  18. Thomas C. Hales, Mark Adams, Gertrud Bauer, Tat Dat Dang, John Harrison, Le Truong Hoang, Cezary Kaliszyk, Victor Magron, Sean McLaughlin, Tat Thang Nguyen, Quang Truong Nguyen, Tobias Nipkow, Steven Obua, Joseph Pleso, Jason M. Rute, Alexey Solovyev, Thi Hoai An Ta, Nam Trung Tran, Thi Diep Trieu, Josef Urban, Ky Vu, and Roland Zumkeller. A Formal Proof of the Kepler conjecture. Forum of Mathematics, Pi, 5, 2017. URL: https://doi.org/10.1017/fmp.2017.1.
  19. Leon Henkin. Completeness in the Theory of Types. J. Symb. Log., 15:81-91, 1950. Google Scholar
  20. Peter V. Homeier. A Design Structure for Higher Order Quotients. In Joe Hurd and Thomas F. Melham, editors, Theorem Proving in Higher Order Logics, 18th International Conference, TPHOLs 2005, Oxford, UK, August 22-25, 2005, Proceedings, volume 3603 of Lecture Notes in Computer Science, pages 130-146. Springer, 2005. URL: https://doi.org/10.1007/11541868_9.
  21. Brian Huffman and Ondrej Kuncar. Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL. In Georges Gonthier and Michael Norrish, editors, Certified Programs and Proofs - Third International Conference, CPP 2013, Melbourne, VIC, Australia, December 11-13, 2013, Proceedings, volume 8307 of LNCS, pages 131-146. Springer, 2013. URL: https://doi.org/10.1007/978-3-319-03545-1_9.
  22. Cezary Kaliszyk and Karol Pąk. Isabelle Formalization of Set Theoretic Structures and Set Comprehensions. In Johannes Blamer, Temur Kutsia, and Dimitris Simos, editors, Mathematical Aspects of Computer and Information Sciences, MACIS 2017, volume 10693 of LNCS. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-72453-9_12.
  23. Cezary Kaliszyk and Karol Pąk. Isabelle Import Infrastructure for the Mizar Mathematical Library. In Florian Rabe, William M. Farmer, Grant O. Passmore, and Abdou Youssef, editors, 11th International Conference on Intelligent Computer Mathematics (CICM 2018), volume 11006 of LNCS, pages 131-146. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-96812-4_13.
  24. Cezary Kaliszyk and Karol Pąk. Semantics of Mizar as an Isabelle Object Logic. Journal of Automated Reasoning, 2018. URL: https://doi.org/10.1007/s10817-018-9479-z.
  25. Cezary Kaliszyk, Karol Pąk, and Josef Urban. Towards a Mizar Environment for Isabelle: Foundations and Language. In Jeremy Avigad and Adam Chlipala, editors, Proc. 5th Conference on Certified Programs and Proofs (CPP 2016), pages 58-65. ACM, 2016. URL: https://doi.org/10.1145/2854065.2854070.
  26. Cezary Kaliszyk and Christian Urban. Quotients revisited for Isabelle/HOL. In William C. Chu, W. Eric Wong, Mathew J. Palakal, and Chih-Cheng Hung, editors, Proc. of the 26th ACM Symposium on Applied Computing (SAC'11), pages 1639-1644. ACM, 2011. Google Scholar
  27. Akihiro Kanamori. The higher infinite: Large cardinals in set theory from their beginnings. Springer Monographs in Mathematics. Springer-Verlag Berlin Heidelberg, 2 edition, 2003. Google Scholar
  28. Dominik Kirst and Gert Smolka. Large Model Constructions for Second-Order ZF in Dependent Type Theory. Certified Programs and Proofs - 7th International Conference, CPP 2018, Los Angeles, USA, January 8-9, 2018, January 2018. Google Scholar
  29. Alexander Krauss and Andreas Schropp. A Mechanized Translation from Higher-Order Logic to Set Theory. In Matt Kaufmann and Lawrence C. Paulson, editors, Interactive Theorem Proving (ITP 2010), volume 6172 of LNCS, pages 323-338. Springer, 2010. Google Scholar
  30. Ondřej Kunčar. Reconstruction of the Mizar Type System in the HOL Light System. In Jiri Pavlu and Jana Safrankova, editors, WDS Proceedings of Contributed Papers: Part I – Mathematics and Computer Sciences, pages 7-12. Matfyzpress, 2010. Google Scholar
  31. Stephan Merz. Mechanizing TLA in Isabelle. In Robert Rodošek, editor, Workshop on Verification in New Orientations, pages 54-74, Maribor, 1995. Univ. of Maribor. Google Scholar
  32. Dennis Müller, Thibault Gauthier, Cezary Kaliszyk, Michael Kohlhase, and Florian Rabe. Classification of Alignments Between Concepts of Formal Mathematical Systems. In Herman Geuvers, Matthew England, Osman Hasan, Florian Rabe, and Olaf Teschke, editors, 10th International Conference on Intelligent Computer Mathematics (CICM'17), volume 10383 of LNCS, pages 83-98. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-62075-6_7.
  33. Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. Isabelle/HOL: A Proof Assistant for Higher-Order Logic, volume 2283 of LNCS. Springer, 2002. Google Scholar
  34. Steven Obua. Partizan Games in Isabelle/HOLZF. In Kamel Barkaoui, Ana Cavalcanti, and Antonio Cerone, editors, Theoretical Aspects of Computing - ICTAC 2006, volume 4281 of LNCS, pages 272-286. Springer, 2006. Google Scholar
  35. Steven Obua, Jacques D. Fleuriot, Phil Scott, and David Aspinall. ProofPeer: Collaborative theorem proving. CoRR, abs/1404.6186, 2014. URL: http://arxiv.org/abs/1404.6186.
  36. Lawrence C. Paulson. Set Theory for Verification: I. From foundations to functions. J. Autom. Reasoning, 11(3):353-389, 1993. URL: https://doi.org/10.1007/BF00881873.
  37. Karol Pąk. Brouwer Fixed Point Theorem in the General Case. Formalized Mathematics, 19(3):151-153, 2011. URL: https://doi.org/10.2478/v10037-011-0024-3.
  38. Karol Pąk. Brouwer Invariance of Domain Theorem. Formalized Mathematics, 22(1):21-28, 2014. URL: https://doi.org/10.2478/forma-2014-0003.
  39. Karol Pąk. Topological Manifolds. Formalized Mathematics, 22(2):179-186, 2014. URL: https://doi.org/10.2478/forma-2014-0019.
  40. Florian Rabe. How to identify, translate and combine logics? J. Log. Comput., 27(6):1753-1798, 2017. URL: https://doi.org/10.1093/logcom/exu079.
  41. Christoph Schwarzweller. The Ring of Integers, Euclidean Rings and Modulo Integers. Formalized Mathematics, 8(1):29-34, 1999. Google Scholar
  42. Alfred Tarski. Über unerreichbare Kardinalzahlen. Fundamenta Mathematica, 30:68-89, 1938. URL: http://matwbn.icm.edu.pl/ksiazki/fm/fm30/fm30113.pdf.
  43. Andrzej Trybulec. Tarski Grothendieck Set Theory. Journal of Formalized Mathematics, Axiomatics, 2002. Released 1989. Google Scholar
  44. Makarius Wenzel, Lawrence C. Paulson, and Tobias Nipkow. The Isabelle Framework. In Otmane Aït Mohamed, César A. Muñoz, and Sofiène Tahar, editors, Theorem Proving in Higher Order Logics, 21st International Conference, TPHOLs 2008, volume 5170 of LNCS, pages 33-38. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-71067-7_7.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact