类型论中的关系形式化

摘要：

类型理论作为数学形式化的框架和提供半自动证明检查和构造的证明助手的基础，在数学基础中起着重要的作用。在类型论中，每个定理的推导都导致了一个形式化的术语来封装整个证明过程。在本文中，我们使用类型理论的一个变体，即具有定义的构造演算，来形式化二元关系的标准理论。这包括关系的基本运算，关系的特殊性质的准则，这些性质在基本运算下的不变性，等价关系，良序，和超穷归纳法。定义和证明作为旗帜式推导。

英文摘要：

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.

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。