Formalizing Relations in Type Theory
Farida Kachapova1 Show affiliations
- Department of Mathematical Sciences, Auckland University of Technology, New Zealand
Journal of Mathematics and Statistics, Volume 18, Issue 1, pp. 148–162 · doi.org/10.3844/jmssp.2022.148.162
Abstract
Typetheory plays an important role in the foundations of mathematics as a frameworkfor formalizing mathematics and a base for proof assistants providingsemi-automatic proof checking and construction. Derivation of each theorem intype theory results in a formal term encapsulating the whole proof process.This study uses a variant of type theory, namely the Calculus of Constructionswith Definitions, to formalize the standardtheory of binary relations. This includes basic operations on relations,criteria for special properties of relations, invariance of these propertiesunder the basic operations, equivalence relation, well-ordering, andtransfinite induction. Definitions and proofs are presented as flag-stylederivations.
Licence and reuse
Open access. This article is licensed under a Creative Commons Attribution 4.0 International Licence (CC BY 4.0), as printed on the article, which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original authors and the source. No permission is needed.
How to reuse this articleResponses (0)
About this article
Kachapova, F. (2022). Formalizing Relations in Type Theory. Journal of Mathematics and Statistics, 18(1), 148–162. https://doi.org/10.3844/jmssp.2022.148.162
- Licence
- CC BY 4.0
- Issue
- Volume 18, Issue 1
- Policies
- Editorial independenceUse of generative AIData availabilityAppeals and complaints
- Version
- Version of record