Extended abstract of Euclid and his Twentieth Century Rivals: Diagrams in the Logic of Euclidean Geometry

Abstract

This extended abstract describes a forthcoming book which should be of interest to those attending the Diagrams 2006 conference and to others generally interested in diagrammatic reasoning in the context of Euclidean Geometry. The book, Euclid and His Twentieth Century Rivals: Diagrams in the Logic of Euclidean Geometry[4], is still in preparation, but will be published by CSLI press once it is completed. In 1879, the English mathematician Charles Dodgson, better know to the world under his pen name of Lewis Carroll, published a little book entitled Euclid and His Modern Rivals. [1] Dodgson was concerned by the fact that quite a number of different nineteenth century authors had written their own treatments of planar geometry, most claiming to improve on Euclid, and each one slightly different in the order of its theorems, in which theorems it chose to include, in the proofs given of these theorems, in its treatment of the theory of parallel lines, and in other aspects. Dodgson's book was written "[i]n furtherance of the great cause which I have at heart - the vindication of Euclid's masterpiece...." It is written mostly in the form of a dream dialogue between a nineteenth century mathematician, Minos, and the ghost of Euclid. In it, they consider each of the modern rivals in turn, and conclude in each case that, while many of the rivals have interesting things to say, none of them are a more appropriate basis for the study of a beginning geometry student than Euclid's Elements. At the time at which Dodgson wrote his book, the subjects of geometry and logic were both entering a period of rapid change after having remained relatively constant for two thousand years. There had been enough change already to make Dodgson feel that Euclid needed defending. In the hundred and twenty-five years since then, however, there have been much larger changes in these fields, and, as a result, rather than just undergoing some small changes, Euclidean geometry in general, and Euclid's proofs in particular, have mostly fallen out of the standard mathematics curriculum. This is at least in part because Euclid's Elements[2], which was viewed for most of its existence as being the gold standard of careful reasoning and mathematical rigor, has come to be viewed as being inherently and unsalvageably informal and unrigorous. One reason for this is certainly its essential use of geometric diagrams. Around the turn of the twentieth century, David Hilbert published his Foundations of Geometry[3], which fit more easily into the new framework of mathematical logic that was developing at that time, and did not use diagrams except as an explanatory tool. Since that time, most mathematicians have viewed Hilbert's Foundations rather than Euclid's Elements as the proper and more solid foundation of Euclidean Geometry. Euclid and His Twentieth Century Rivals traces this history and tries to explain some of the reasons why this happened. It then brings twentieth century logical methods to bear on Euclid's proof methods, and shows how such methods can make Euclid's style of diagrammatic proofs as rigorous as Hilbert's proofs, which do not employ diagrams. A formal system, FG, is defined to manipulate geometric diagrams, and this system is used to study Euclid's informal methods of proof, methods that are still commonly used in informal treatments of geometry today. It is argued that, because they can be made rigorous in a formal system, these methods are in fact valid modes of argument. Implicit in this method of evaluating an informal mode of argument by replacing it with an essentially similar formal system is what I call the formality hypothesis: Hypothesis 1 (Formality Hypothesis). An informal proof method is sound if and only if it is possible to give a formal system with the property that informal proofs using the informal methods can always be translated into equivalent correct proofs in the formal system. By a formal system, we mean a system of argument that is carefully enough specified that it can be implemented on a computer. Modern ideas of logic give us the means of saying, at least in principle, what it means for such a formal system to be sound - that is, whether or not it will only lead to correct conclusions. They don't give us, by themselves, the means to say what it means for an informal method of proof to be correct; but the formality hypothesis gives us a basis for evaluating such informal methods by translating them into corresponding formal methods. Euclid and His Twentieth Century Rivals analyses Euclid's proof methods in this way, by translating them into a formal system, FG, which is strong enough and similar enough to what Euclid does to be able to formalize most of what is contained in the first four books of Euclid's Elements, which are the part of the Elements that deal with planar geometry. FG accomplishes this by giving a careful, formal definition of what constitutes a geometric diagram in this context, and then by giving careful rules for manipulating such diagrams. The definition of what constitutes a diagram is quite complicated, but it captures a comparatively simple and ancient idea: two diagrams are the same if they share the same topology. That is, if one can be stretched without tearing into the other; or, put another way, that all of the points and lines are arranged in the same way. This idea can already be found in the writings of Proclus, a fifth century commentator on Euclid, who writes that each case in a geometric proof "announces different ways of construction and alteration of positions due to the transposition of points or lines or planes or solids." (This is Sir Thomas Heath's translation, as given in [2].) A computer system, CDEG, which implements this formal system on a computer in order to demonstrate that it is, in fact, completely formal, is also discussed. The book also discusses several other ways that we can use this formal system to better understand the history and practice of the use of diagrams in informal treatments of geometry. For example, commentators writing about Euclid's Elements often note that he uses the principle of superposition to prove the Side-Angle-Side rule and from then on uses this derived rule in place of the principle of superposition whenever possible, and conclude that Euclid must have thought that this principle was somehow suspect. However, Euclid and His Twentieth Century Rivals uses the formal system FG to show that there are very good reasons to use the Side-Angle-Side rule, once you have derived it, in place of the principle of superposition, even if there is nothing suspect about the principle. Furthermore, it is shown that by weakening the principle of superposition slightly, other weaker systems of geometry can be obtained in which the Side-Angle-Side rule is not derivable, and that these weaker geometries have a fascinating logical structure of their own. Euclid and His Twentieth Century Rivals also discusses the significance of several technical results relating to the computational complexity of working with diagrams in the formal system FG, results published elsewhere in the Journal of Complexity [5]. The field of computational complexity measures how much time and other resources are necessary to do a given computation. Such results are highly relevant to the study of diagrammatic reasoning because once we know that arguments employing diagrams are logically sound, we would then like to know whether or not they require more time and resources than arguments that do not employ diagrams. In [5], it is shown that the diagram satisfaction problem of whether or not a diagram represents a physically possible arrangement of points and lines is solvable by computer in a finite amount of time, but that this problem is at least NP-hard, meaning that it can take an intractably large amount of time to solve in practice.1 What does this mean? It means that, while diagram satisfiability can theoretically be decided by a computer, and case analysis in geometry can therefore be theoretically be done by a computer in a way that will never return unsatisfiable diagrams, it is nonetheless impractical to do so, and any real world computer system or formal system will therefore sometimes unavoidably return extra unsatisfiable cases. This shows us that the long tradition of considering and disposing of extra cases in geometry is unavoidable in a diagrammatic approach. The formalization of Euclid's proof methods in the formal system FG is therefore useful for several different reasons: it lets us better understand his proofs; it allows us to prove metamathematical results about these kinds of proofs; and it shows that there is no inherent reason that the modern foundations of geometry must look completely different from the ancient foundations found in the Elements. Thus, the aims of Euclid and His Twentieth Century Rivals are not far removed from Dodgson's aims in 1879: to show that, while modern developments in logic and geometry may require changes in Euclid's development, his basic ideas are neither outdated nor obsolete. © Springer-Verlag Berlin Heidelberg 2006.