论文标题
关于欧几将相等数字的概念
On the Notion of Equal Figures in Euclid
论文作者
论文摘要
Euclid使用了“相等数字”的未定义概念，他将其应用于对等于或从等价减去的平等的共同概念。当（在先前的工作中）我们为计算机进行检查的正式化欧几里得书籍〜I时，我们必须添加有关“相等三角形”和“相等的四边形”的不确定关系的15个公理，以取代欧几里得对常见概念的使用。在本文中，我们提供了欧几里得可以给出的“相等三角形”和“相等的四边形”的定义，并证明它们具有所需的属性。这消除了添加新公理的需求。证明使用比例理论。因此，我们还讨论了具有悠久历史的“比例早期理论”。
Euclid uses an undefined notion of "equal figures", to which he applies the common notions about equals added to equals or subtracted from equals. When (in previous work) we formalized Euclid Book~I for computer proof-checking, we had to add fifteen axioms about undefined relations "equal triangles" and "equal quadrilaterals" to replace Euclid's use of the common notions. In this paper, we offer definitions of "equal triangles" and "equal quadrilaterals", that Euclid could have given, and prove that they have the required properties. This removes the need for adding new axioms. The proof uses the theory of proportions. Hence we also discuss the "early theory of proportions", which has a long history.
