Euclid and His Twentieth Century Rivals: Diagrams in the Logic of Euclidean Geometry

Has Miller restored faith in Euclidean geometry by revealing a natural foundation upon which it rests? This is a question that could be asked after reading his book. Miller assesses his work in this way:

Our formalization of Euclid’s proof methods is useful for several 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 modern foundations of geometry must look completely different from the ancient foundations found in the Elements. (p. 4)

In the title of his book, Miller alludes to Charles L. Dodgson’s (i.e., Lewis Carroll’s) Euclid and his Modern Rivals (1885). The famous author contended that none of Euclid’s rivals of Dodgson’s time were, in Miller’s paraphrase, “a more appropriate basis for the study of a beginning geometry student” (p. 1). Of his own work, Miller remarks:

[T]he aims of this book are not far removed from Dodgson’s aims in 1879: to show that, while modern developments of logic and geometry may require changes in Euclid’s development, his basic ideas are neither outdated nor obsolete. (p. 4)

I provide a very rough indication of Miller’s formalization (which is too extensive to present in this review). Miller’s goal is ‘to give…a formal system in which Euclid’s proofs can be duplicated’ (p. 13), in this way demonstrating their correctness. He provides a way of proving Euclid’s propositions by capturing formally the topology of Euclid’s geometry, by generating topological cases, and then by eliminating cases from consideration, leaving a solution. This formalization, Miller claims, brings Euclid into the realm of completely formal systems. (‘The simplest possible definition that we can adopt here is that a system is completely formal if it can be completely implemented on a computer’ (p. 13).) Miller remarks:

A crucial idea will be that all crucial information given by a diagram is contained in its topology, on the general arrangement of its points and lines in the plane. Another way of saying this is that if one diagram can be transformed into another by stretching, then the two diagrams are essentially the same. This is typical of diagrammatic reasoning, and, although it has not been previously treated formally, this idea has a long tradition in geometry. Proclus, the fifth century commentator on Euclid, writes that each case in a geometric proof ‘announces different ways of construction and alternative positions due to the transposition of points or lines or planes or solids.’ (This is Sir Thomas Heath’s translation, given in Euclid (1956).) Thus, we see that the idea of considering cases to be different when the arrangements of the geometric object being considered are topologically different is an ancient one. (p. 4)

With regard to SAS (the side-angle-side criterion for triangle congruence),

[t]he proof is essentially identical to Euclid’s proof, with a lot of tedious extra cases showing all of the ways that the triangles could possibly intersect. The idea is to move the two triangles together using the symmetry transformations and to then check that they must be completely superimposed. (p. 44)

 

Figure 1

More specifically,

[t]he first step [of the proof] is to apply rule S1 to the diagram in [Figure 1], moving triangle ABC so that the imageA'B' of AB lies along DE. The possible cases that result are shown in the diagram arrays in [Figure 2] and [Figure 3]. For the sake of readability, many markings have been left off these diagrams, although all markings that are later needed have been left. (p. 25)

Note that curved lines are needed to depict many of the topological cases. (Does this distance Miller’s treatment from Euclid? — a worry raised in my mind.) Also note that the generation of cases takes place within Miller’s formalism (which he has implemented with a computer algorithm). The software-generated diagrams assist human understanding. Figure 4 magnifies four diagrams in the upper-left corner of Figure 2.

 

Figure 2

 

 

Figure 3

 

Figure 4

 

 

Norman’s second step ‘remove[s] all of the extra cases using the rules of inference CA and CS’ (p. 45). Informally, a diagram is removed by inference CA if in the diagram there is a line properly contained in another line of equal length. Similarly, informally, a diagram is removed by inference CS if in the diagram there is an angle properly contained in another angle of equal degree. Norman observes that ‘[a]ll the diagrams shown in [Figure 2] except the very first one can be eliminated by applying CS to A'B'and DE’ (p. 45). Furthermore, all the cases in Figures 2 and 3 can be eliminated using CA or CS except the first one in Figure 2. The first diagram in Figure 2, then, is ‘provable’ from the diagram in Figure 1. Miller gives a formal definition of provable. Indeed, the mathematical work is done by the formalism, implemented by a computer algorithm.

Miller’s book seems to have thrown new light — philosophical and mathematical — on an old classic.

References:

Dodgson, Charles. 1885. Euclid and his Modern Rivals. London: MacMillan and Co., 2^nd edition.

Euclid. 1956. The Elements . Translated with an introduction by Thomas L. Heath.

---

Dennis Lomas (dlomas@upei.ca) has studied computer science (MSc), mathematics (half dozen, or so, graduate courses), and philosophy (PhD). Retired, he does some part-time teaching at the University of Prince Edward Island.