On the Notion of Equal Figures in Euclid

TL;DR

This paper formalizes Euclid's notion of equal figures by providing definitions and proofs that eliminate the need for additional axioms, using the theory of proportions to clarify Euclid's approach.

Contribution

It offers definitions of equal triangles and quadrilaterals consistent with Euclid, removing the necessity for extra axioms in formalization.

Findings

Definitions align with Euclid's original concepts

Proofs demonstrate the properties of equal figures

Uses the theory of proportions to support the definitions

Abstract

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.