arXiv · 2008.12643
On the Notion of Equal Figures in Euclid
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.
Explore related subjects
Keep this discovery
Explore connections, maps & timelines
Michael Beeson. 2020-08-14. On the Notion of Equal Figures in Euclid. https://doi.org/10.1007/s13366-022-00649-9
Cite the original work for its findings. Save a collection to share your selection of sources.