Ensuring generality in euclid's diagrammatic arguments

Abstract

This paper presents and compares FG and Eu, two recent formalizations of Euclid's diagrammatic arguments in the Elements. The analysis of FG, developed by the mathematician Nathaniel Miller, and that of Eu, developed by the author, both exploit the fact that Euclid's diagrammatic inferences depend only on the topology of the diagram. In both systems, the symbols playing the role of Euclid's diagrams are discrete objects individuated in proofs by their topology. The key difference between FG and Eu lies in the way that a derivation is ensured to have the generality of Euclid's results. Carrying out one of Euclid's constructions on an individual diagram can produce topological relations which are not shared by all diagrams so constructed. FG meets this difficulty by an enumeration of cases with every construction step. Eu, on the other hand, specifies a procedure for interpreting a constructed diagram in terms of the way it was constructed. After describing both approaches, the paper discusses the theoretical significance of their differences. There is in Eu a context dependence to diagram use, which enables one to bypass the (sometimes very long) case analyses required by FG. © 2008 Springer-Verlag Berlin Heidelberg.