论欧几里得中的等图形概念

欧几里得使用了一个未定义的“等图形”概念，并对其应用了关于等量加等量或等量减等量的公共概念。当我们（在先前工作中）为计算机证明检查形式化欧几里得第一卷时，不得不添加关于未定义关系“等三角形”和“等四边形”的十五条公理，以取代欧几里得对公共概念的使用。在本文中，我们给出了欧几里得本可给出的“等三角形”和“等四边形”的定义，并证明它们具有所需性质。这消除了添加新公理的必要性。该证明使用了比例理论。因此我们 also 讨论了具有悠久历史的“早期比例理论”。