**Unformatted text preview:**

The Role of the Diagram in Euclid’s ElementsJeremy AvigadDepartment of Philosophy and Department of Mathematical SciencesCarnegie Mellon University(including joint work with Ed Dean, John Mumma, and Ben Northrop)June, 2008The ElementsFor more than two thousand years, Euclid’s Elements was held to bethe paradigm for rigorous argumentation.But the nineteenth century raised concerns:•Conclusions are drawn from diagrams, using “intuition” ratherthan precise rules.•Particular diagrams are used to infer general results (withoutsuitable justification).Axiomatizations due to Pasch and Hilbert, and Tarksi’s formalaxiomatization later on, were thought to make Euclid rigorous.The ElementsBut in some ways, they are unsatisfactory.•Proofs in the new systems look very different from Euclid’s.•The initial criticisms belie the fact that Euclidean practice wasremarkably stable for more than two thousand years.Our project (Mumma, Dean, and me):•Describe a formal system that is much more faithful to Euclid.•Argue that the system is sound and complete (for the theorems itcan express) relative to Euclidean fields.•Show that the system can easily be implemented usingcontemporary automated reasoning technology.First salient feature: the use of diagramsObservation: the diagram is inessential to the communication of theproof. (Rather, it is used to “see” that the inferences are correct.)Exercise:•Let p and q be points on a line.•Let r be between p and q.•Let s be between p and r.•Let t be between r and q.Is s necessarily between p and t?Philosophical thesis: from a logical perspective, the right way tocharacterize diagrammatic reasoning is in terms of the class ofinferences that are licensed.First salient feature: the use of diagramsObservation: the diagram is inessential to the communication of theproof. (Rather, it is used to “see” that the inferences are correct.)Exercise:•Let p and q be points on a line.•Let r be between p and q.•Let s be between p and r.•Let t be between r and q.Is s necessarily between p and t?Philosophical thesis: from a logical perspective, the right way tocharacterize diagrammatic reasoning is in terms of the class ofinferences that are licensed.First salient feature: the use of diagramsObservation (Manders): In a Euclidean proof, diagrams are only usedto infer “co-exact” (regional / topological) information, such asincidence, intersection, containment, etc.Exact (metric) information, like congruence, is always made explicitin the text.Poincaré: “Geometry is the art of precise reasoning from badlyconstructed diagrams.”Solution: take the “diagram” to be a representation of the relevantdata.Second salient feature: generalitySome aspects of diagrammatic inference are puzzling:•Let p and q be distinct points.•Let L be a line though p and q.•Let r and s be points on opposite sides of L.•Let M be the line through r and s.•Let t be the intersection of L and M.Is t necessarily between r and s? Is t necessarily between p and q?A diagrammatic inference was necessary even to “see” the L and Mnecessarily intersect. But not every feature found in a particulardiagram is generally valid.Euclid manages to avoid drawing invalid conclusions.We need an explanation as to what secures the generality.Third salient feature: logical for mTheorems in Euclid are of the form:Given points, lines, circles, satisfying . . . , there are points,lines, circles satisfying . . .where each . . . is a conjunction of literals.(If the inner existential quantifier is absent, it is a “demonstration”rather than a “construction.”)Proofs contain a construction part, and a deduction part.Reasoning is linear, assertions are literals.Exceptions: proof by contradiction, using a case distinction(sometimes “without loss of generality”).Fourth salient feature: nondegeneracyIn the statement of a theorem, points are generally assumed to bedistinct, triangles are nondegenerate, etc.Two issues:•Sometimes the theorem still holds in some degenerate cases.•When the theorems are applied, Euclid doesn’t always checknondegeneracy.I will have little to say about this; in our system, nondegeneracyrequirement are stated explicitly.For malizing EuclidPrior efforts:•Nathaniel Miller’s Ph.D. thesis (2001): system is verycomplicated; generality is attained by considering casesexhaustively.•John Mumma’s Ph.D. thesis (2006): employs diagrams (andequivalence relation on diagrams); generality is attained usingrules.Our formal system, E, is derived from Mumma’s. But now a“diagram” is nothing more than an abstract representation oftopological information. The system spells out what can be inferredfrom the diagram.The language of EBasic sorts:•diagram sorts: points p, q, r, . . ., lines L, M, N , . . ., circlesα, β, γ, . . .•metric sorts: lengths, angles, and areas.Basic symbols:•diagram relations: on( p, L), same-side( p, q, L),between( p, q, r ), on(p, γ ), inside(p, γ ), center( p, γ ),intersects(L , M), =•metric functions and relations: +, <, =, right − angle•connecting functions: pq,6pqr, 4pqrOther relations can be defined from these; e.g.diff-side( p, q, L) ≡ ¬on(p, L) ∧ ¬on(q, L) ∧ ¬same-side( p, q, L)SequentsThe proof system establishes sequents of the following form:0 ⇒ ∃Eq,EM,Eβ. 1where 0 and 1 are sets of literals.Applying a construction rule or prior theorem augments Eq,EM,Eβ, 1.Applying deductive inferences augments 1.Case splits and suppositional reasoning temporarily augment 0.I need to describe:•Construction rules.•Deductive inferences.Diagram inferences are implicit in both.Construction rules“Let p be a point on L”No prerequisites.“Let p be a point distinct from q and r”No prerequisites.“Let L be the line through p and q”Requires p 6= q.“Let p be the intersection of L and M.”Requires that L and M intersect.And so on. . .Deductive inferencesFour types:1. Diagram inferences: any fact that can be “read off” from thediagram.2. Metric inferences: essentially linear arithmetic on lengths,angles, and areas.3. Diagram to metric: for example, if q is between p and r, thenpq + qr = pr, and similarly for areas and angles.4. Metric to diagram: for example, if p is the center of γ , q is on γ ,and pr < pq, then r is inside γ .Diagram inferencesBoth construction inferences and diagram inferences require anaccount of what can be “read off” from the diagram.We get this by closing