JMSS Cover
Frequency: Continuous
ISSN: 1549-3644 (Print)
ISSN: 1558-6359 (Online)
Research Article Open Access

Formalizing Relations in Type Theory

Farida Kachapova1
  • 1 Department of Mathematical Sciences, Auckland University of Technology, New Zealand

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.

Journal of Mathematics and Statistics
Volume 18 No. 1, 2022, 148-162

DOI: https://doi.org/10.3844/jmssp.2022.148.162

Submitted On: 2 March 2022 Published On: 29 October 2022

How to Cite: 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

Open AccessCopyright: © 2022 Farida Kachapova. This is an open access article distributed under the terms of the Creative Commons Attribution License, which permits unrestricted use, distribution, and reproduction in any medium, provided the original author and source are credited.

  • 2,152 Views
  • 1,164 Downloads
  • 0 Citations

Download

Keywords

  • Type Theory
  • Calculus of Constructions
  • Binary Relation
  • Transfinite Induction
  • Flag-Style Derivation