Formalizing relations in type theory

TL;DR

This paper formalizes the theory of binary relations within a variant of type theory, enabling precise proof representations and analysis of relation properties using the Calculus of Constructions with Definitions.

Contribution

It introduces a formalization of binary relations in a type-theoretic framework, including definitions, properties, and proofs using flag-style derivations.

Findings

Formalization of binary relations in type theory.

Proofs of properties like invariance and well-ordering.

Framework supports semi-automatic proof checking.

Abstract

Type theory plays an important role in foundations of mathematics as a framework for formalizing mathematics and a base for proof assistants providing semi-automatic proof checking and construction. Derivation of each theorem in type theory results in a formal term encapsulating the whole proof process. In this paper we use a variant of type theory, namely the Calculus of Constructions with Definitions, to formalize the standard theory of binary relations. This includes basic operations on relations, criteria for special properties of relations, invariance of these properties under the basic operations, equivalence relation, well-ordering, and transfinite induction. Definitions and proofs are presented as flag-style derivations.