Document Open Access Logo

Some Axioms for Mathematics

Authors Frédéric Blanqui , Gilles Dowek , Émilie Grienenberger, Gabriel Hondet, François Thiré

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2021.20.pdf
  • Filesize: 0.77 MB
  • 19 pages

Document Identifiers

Author Details

Frédéric Blanqui
  • Université Paris-Saclay, ENS Paris-Saclay, LMF, CNRS, Inria, France
Gilles Dowek
  • Université Paris-Saclay, ENS Paris-Saclay, LMF, CNRS, Inria, France
Émilie Grienenberger
  • Université Paris-Saclay, ENS Paris-Saclay, LMF, CNRS, Inria, France
Gabriel Hondet
  • Université Paris-Saclay, ENS Paris-Saclay, LMF, CNRS, Inria, France
François Thiré
  • Nomadic Labs, Paris, France

Acknowledgements

The authors want to thank Michael Färber, César Muñoz, Thiago Felicissimo, and Makarius Wenzel for helpful remarks on a first version of this paper.

Cite As Get BibTex

Frédéric Blanqui, Gilles Dowek, Émilie Grienenberger, Gabriel Hondet, and François Thiré. Some Axioms for Mathematics. In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 20:1-20:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021) https://doi.org/10.4230/LIPIcs.FSCD.2021.20

Abstract

The λΠ-calculus modulo theory is a logical framework in which many logical systems can be expressed as theories. We present such a theory, the theory {U}, where proofs of several logical systems can be expressed. Moreover, we identify a sub-theory of {U} corresponding to each of these systems, and prove that, when a proof in {U} uses only symbols of a sub-theory, then it is a proof in that sub-theory.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic
  • Theory of computation → Type theory
  • Theory of computation → Equational logic and rewriting
Keywords
  • logical framework
  • axiomatic theory
  • dependent types
  • rewriting
  • interoperabilty

Metrics

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

References

  1. L. Allali and O. Hermant. Semantic A-translation and super-consistency entail classical cut elimination. CoRR, abs/1401.0998, 2014. URL: http://arxiv.org/abs/1401.0998.
  2. A. Assaf. A framework for defining computational higher-order logics. PhD thesis, École polytechnique, 2015. Google Scholar
  3. A. Assaf, G. Burel, R. Cauderlier, D. Delahaye, G. Dowek, C. Dubois, F. Gilbert, P. Halmagrand, O. Hermant, and R. Saillard. Dedukti: a logical framework based on the lambda-Pi-calculus modulo theory. Manuscript, 2016. Google Scholar
  4. H. Barendregt. Lambda calculi with types. In S. Abramsky, D.M. Gabbay, and T.S.E. Maibaum, editors, Handbook of Logic in Computer Science, volume 2, pages 117-309. Oxford University Press, 1992. Google Scholar
  5. B. Barras. Auto-validation d'un système de preuves avec familles inductives. PhD thesis, Université Paris 7, France, 1999. Google Scholar
  6. S. Berardi. Towards a mathematical analysis of the Coquand-Huet calculus of constructions and the other systems in Barendregt’s cube. Manuscript, 1988. Google Scholar
  7. F. Blanqui. Type theory and rewriting. PhD thesis, Université Paris-Sud, France, 2001. URL: http://hal.inria.fr/inria-00105525.
  8. F. Blanqui. Type Safety of Rewrite Rules in Dependent Types. In Proceedings of the 5th International Conference on Formal Structures for Computation and Deduction, Leibniz International Proceedings in Informatics 167, 2020. URL: https://doi.org/10.4230/LIPIcs.FSCD.2020.13.
  9. F. Blanqui and G. Hondet. Encoding of predicate subtyping and proof irrelevance in the λπ-calculus modulo theory. In Proceedings of the 26th International Conference on Types for Proofs and Programs, Leibniz International Proceedings in Informatics 188, 2021. Google Scholar
  10. A. Church. A formulation of the simple theory of types. The Journal of Symbolic Logic, 5(2):56-68, 1940. Google Scholar
  11. Th. Coquand. An analysis of Girard’s paradox. Technical Report RR-0531, Inria, 1986. URL: https://hal.inria.fr/inria-00076023.
  12. Th. Coquand and G. Huet. The calculus of constructions. Information and Computation, 76(2):95-120, 1988. Google Scholar
  13. D. Cousineau and G. Dowek. Embedding pure type systems in the lambda-Pi-calculus modulo. In Proceedings of the 8th International Conference on Typed Lambda Calculi and Applications, Lecture Notes in Computer Science 4583, 2007. URL: https://doi.org/10.1007/978-3-540-73228-0_9.
  14. N. Dershowitz and J.-P. Jouannaud. Rewrite systems. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science. Volume B: Formal Models and Semantics, chapter 6, pages 243-320. North-Holland, 1990. Google Scholar
  15. A. Dorra. équivalence de curry-howard entre le λΠ calcul et la logique intuitionniste. Internship report, 2010. Google Scholar
  16. G. Dowek. On the definition of the classical connectives and quantifiers. In E.H. Haeusler, W. de Campos Sanz, and B. Lopes, editors, Why is this a Proof?, Festschrift for Luiz Carlos Pereira. College Publications, 2015. Google Scholar
  17. G. Dowek, T. Hardin, and C. Kirchner. Theorem proving modulo. Journal of Automated Reasoning, 31:33-72, 2003. URL: https://doi.org/10.1023/A:1027357912519.
  18. G. Dowek and B. Werner. Proof normalization modulo. Journal of Symbolic Logic, 68(4):1289-1316, 2003. URL: https://doi.org/10.2178/jsl/1067620188.
  19. G. Dowek and B. Werner. Arithmetic as a theory modulo. In Jürgen Giesl, editor, Term Rewriting and Applications, 16th International Conference, RTA 2005, Nara, Japan, April 19-21, 2005, Proceedings, volume 3467 of Lecture Notes in Computer Science, pages 423-437. Springer, 2005. Google Scholar
  20. Gaspard Férey and François Thiré. Proof Irrelevance in LambdaPi Modulo Theory. https://eutypes.cs.ru.nl/eutypes_pmwiki/uploads/Main/books-of-abstracts-TYPES2019.pdf, 2019.
  21. G. Genestier. Dependently-Typed Termination and Embedding of Extensional Universe-Polymorphic Type Theory using Rewriting. PhD thesis, Université Paris-Saclay, 2020. Google Scholar
  22. H. Geuvers. The Calculus of Constructions and Higher Order Logic. In Ph. de Groote, editor, The Curry-Howard isomorphism, volume 8 of Cahiers du Centre de logique, pages 139-191. Université catholique de Louvain, 1995. Google Scholar
  23. F. Gilbert. Extending higher-order logic with predicate subtyping: Application to PVS. (Extension de la logique d'ordre supérieur avec le sous-typage par prédicats). PhD thesis, Sorbonne Paris Cité, France, 2018. Google Scholar
  24. J.-Y. Girard. Interprétation fonctionelle et élimination des coupures de l'arithmétique d'ordre supérieur. PhD thesis, Université de Paris VII, 1972. Google Scholar
  25. É. Grienenberger. A logical system for an Ecumenical formalization of mathematics, 2019. Manuscript. Google Scholar
  26. É. Grienenberger. Expressing Ecumenical systems in the lambda-pi-calculus modulo theory, 2021. In preparation. Google Scholar
  27. R. Harper, F. Honsell, and G. Plotkin. A framework for defining logics. Journal of the ACM, 40(1):143-184, 1993. URL: https://doi.org/10.1145/138027.138060.
  28. D. Hilbert and W. Ackermann. Grundzüge der theoretischen Logik. Springer-Verlag, 1928. Google Scholar
  29. G. Hondet and F. Blanqui. The New Rewriting Engine of Dedukti. In Proceedings of the 5th International Conference on Formal Structures for Computation and Deduction, Leibniz International Proceedings in Informatics 167, 2020. URL: https://doi.org/10.4230/LIPIcs.FSCD.2020.35.
  30. A. J. C. Hurkens. A simplification of Girard’s paradox. In M. Dezani-Ciancaglini and G. Plotkin, editors, Typed Lambda Calculi and Applications, pages 266-278, Berlin, Heidelberg, 1995. Springer Berlin Heidelberg. Google Scholar
  31. J. W. Klop, V. van Oostrom, and F. van Raamsdonk. Combinatory reduction systems: introduction and survey. Theoretical Computer Science, 121:279-308, 1993. URL: https://doi.org/10.1016/0304-3975(93)90091-7.
  32. G. Nadathur and D. Miller. An overview of lambda-prolog. In Logic Programming, Proceedings of the Fifth International Conference and Symposium, Seattle, Washington, USA, August 15-19, 1988 (2 Volumes), pages 810-827, 1988. Google Scholar
  33. Sam Owre and Natarajan Shankar. The Formal Semantics of PVS. SRI International, SRI International, Computer Science Laboratory, Menlo Park CA 94025 USA, 1997. URL: http://pvs.csl.sri.com/doc/semantics.pdf.
  34. L.C. Paulson. Isabelle: The next 700 theorem provers. CoRR, cs.LO/9301106, 1993. URL: http://arxiv.org/abs/cs.LO/9301106.
  35. L.C. Pereira and R.O. Rodriguez. Normalization, soundness and completeness for the propositional fragment of Prawitzquoteright Ecumenical system. Revista Portuguesa de Filosofia, 73(3-4):1153-1168, 2017. Google Scholar
  36. D. Prawitz. Classical versus intuitionistic logic. In E.H. Haeusler, W. de Campos Sanz, and B. Lopes, editors, Why is this a Proof?, Festschrift for Luiz Carlos Pereira. College Publications, 2015. Google Scholar
  37. J. C. Reynolds. Towards a theory of type structure. In Programming Symposium, pages 408-425. Springer, 1974. Google Scholar
  38. TeReSe. Term rewriting systems, volume 55 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2003. Google Scholar
  39. J. Terlouw. Een nadere bewijstheoretische analyse van GSTT’s. Manuscript, 1989. Google Scholar
  40. F. Thiré. Sharing a Library between Proof Assistants: Reaching out to the HOL Family. In Frédéric Blanqui and Giselle Reis, editors, Proceedings of the 13th International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP@FSCD 2018, Oxford, UK, 7th July 2018, volume 274 of EPTCS, pages 57-71, 2018. Google Scholar
  41. F. Thiré. Interoperability between proof systems using the Dedukti logical framework. PhD thesis, Université Paris-Saclay, France, 2020. Google Scholar
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