A formal system for Euclid's Elements

Jeremy Avigad; Edward Dean; John Mumma

Source-linked AI summary

A formal system for Euclid's Elements

Jeremy Avigad, Edward Dean, John Mumma

arXiv:0810.4315v3Oct 23, 2008math.LO

TL;DR

Euclid’s diagram-dependent proofs raised concerns about how particular figures could support general, rigorous conclusions. The paper develops E, a formal system that models construction, deduction, and diagrammatic inference, and shows that it is sound and complete for ruler-and-compass semantics. The authors conclude that Euclidean proofs are governed by precise rules and are more rigorous than commonly claimed, while noting important textual and scope limitations.

Problem
The paper addresses how Euclid’s use of diagrams can support general mathematical proofs despite longstanding concerns that such reasoning relies on intuition.
Method
The authors develop E, a formal system modeling Euclidean construction, deduction, and diagrammatic inference through explicit proof rules.
Results
E provides a close line-by-line model of Euclidean argumentative structure and is sound and complete for an appropriate semantics of ruler-and-compass constructions.
Takeaways & Limitations
The analysis identifies precise, semantically sound rules governing diagrammatic inferences and supports viewing Euclid’s proofs as more rigorous than usually claimed.
Takeaways & Limitations
The historical analysis focuses on one translation of one version of the Elements, and the paper does not claim to address broader cognitive or historical explanations.

Abstract

from arXiv · show

We present a formal system, E, which provides a faithful model of the proofs in Euclid's Elements, including the use of diagrammatic reasoning.

1 Introduction

The paper addresses how Euclid’s diagram-dependent proofs can provide general, rigorous conclusions by formalizing their inferential structure. System E models these practices and is shown sound and complete for ruler-and-compass constructions.

Motivation: Nineteenth-century critics questioned whether diagram-based inferences could support general mathematical claims with certainty.A single drawn triangle has particular geometric features, while the proof must apply to all relevant triangles.
Motivation: Euclid’s proofs nevertheless formed a stable practice that mathematicians across cultures could read, write, and communicate despite apparent logical gaps.The authors therefore seek an explanation of how the practice successfully regulated admissible inferences.
Contribution: The authors argue that diagram use in the Elements is controlled, systematic, and governed by a discernible logic rather than being merely intuitive.Their analysis presents Euclid’s methods as more rigorous than the modern attitude suggests.
Formal approach: E formalizes which inferences can be read from diagrams, building on diagram-based systems that treat relevant information abstractly rather than as particular geometric objects.The formulation follows Mumma’s rule-based approach while treating equivalence classes of information as logically relevant.
Contribution: The system is claimed both to model key methodological features of Books I–IV and to be sound and complete for modern ruler-and-compass semantics.This combines a philosophical claim about Euclidean proof practice with a mathematical claim about the formal semantics.

2 Characterizing the Elements

The paper characterizes Euclidean proofs as diagram-guided arguments organized around construction and deduction. Diagrams need not be communicated as images, yet their encoded spatial relations support immediate inferences that the formal system makes explicit.

2 Characterizing the Elements: The authors aim to identify the salient features of the Elements needed to assess whether E faithfully models Euclidean proofs.They use examples of Euclidean propositions to support this analysis.
Examples of proofs: Proposition I.10 illustrates a construction problem: an equilateral triangle and a bisected angle produce a point that bisects a given segment.The proof uses earlier propositions to establish the required equalities and concludes Q.E.F.
Examples of proofs: The paper distinguishes Euclid’s problems, which expand diagrams through constructions, from theorems, which establish properties of existing diagrams.Euclid marks the distinction with Q.E.F. and Q.E.D. endings.
Examples of proofs: Euclidean proofs typically begin with construction, which introduces objects into a diagram, and continue with deduction, which draws the desired conclusions.The deduction phase mainly records metric equalities and inequalities but also uses diagrammatic configuration.
The role of diagrams: Diagrammatic information can be carried by text, but readers still tend to imagine the diagram when checking spatial claims.The betweenness example is immediately convincing once the relevant configuration is pictured.
Methodology: The authors analyze the logical structure of diagrammatic inference while screening off cognitive, social, and historical explanations for why such inferences are easy or basic.They treat separating these questions as an important methodological point.

3.1 The language of E

E uses a six-sorted language that separates geometric objects from magnitudes and distinguishes diagrammatic from metric assertions. Its relations and definitional extensions encode spatial configuration, measurement, and construction-relevant properties.

Basic language: E has six sorts for points, lines, circles, segments, angles, and areas, with variables ranging over points, lines, and circles.Segments, angles, and areas are obtained as magnitude objects from points.
Diagrammatic relations: Basic diagrammatic relations express incidence, same-side relations, strict betweenness, and transversal intersection among geometric objects.The system includes distinct intersection relations for lines and circles, with intersections interpreted transversally.
Magnitude language: The language represents segment lengths, angle magnitudes, and triangle areas, with equality, addition, less-than, and zero available on each magnitude sort.A right angle is represented by equating an angle to the right-angle constant.
Assertion types: E distinguishes diagrammatic assertions about points, lines, and circles from metric assertions about segments, angles, and areas.Metric assertions include congruence and comparisons of magnitudes, while diagrammatic assertions describe configuration.
Definitional extensions: Additional predicates such as different-side and outside are defined from the basic relations rather than added as primitive symbols.The strict betweenness relation excludes equality with either endpoint.
Role in proofs: Although diagrammatic assertions are usually implicit in Euclid, E’s rules allow them to license later construction steps and deductive inferences.Raw diagrammatic assertions therefore need not typically appear directly in formal proofs.

3.2 Proofs in E

Proofs in E represent Euclidean reasoning as sequents built from construction and demonstration steps. The system supports direct diagrammatic, metric, and transfer inferences, along with theorem application, case analysis, contradiction, and superposition.

Theorems: An E theorem states that a diagram satisfying input assertions can be extended with constructed objects satisfying output assertions.The output may introduce points, lines, or circles, or may assert a theorem property or impossibility.
Proof steps: Construction steps introduce new geometric objects, whereas demonstration steps add conclusions without introducing new objects.In sequent form, construction enlarges the existential variable list while demonstration preserves it.
Inference rules: E permits diagrammatic, metric, and transfer inferences, respectively deriving configuration facts, magnitude facts, or facts transferred between the two domains.These are direct consequences of assertions already present in the active sequent.
Theorem application: Applying a previously proved theorem requires renaming variables, checking its hypotheses as direct consequences, and selecting relevant conclusions and newly introduced variables.This lets a theorem about one geometric configuration apply to another matching configuration.
Proof structure: Proof trees are generally linear, with branching reserved for proof by cases or contradiction.Case splits duplicate the active context with complementary assumptions, while contradiction is simulated using the falsity symbol.
Special inferences: E includes superposition inferences to model Euclid’s use of side-side-side and side-angle-side triangle congruence criteria.These rules address the special inferences used in Propositions 4 and 8 of Book I.
Scope: The system is intended to capture the essential features of Books I–IV, including more elaborate case splits than its basic rules directly specify.The authors argue that such cases can be represented within E.

3.3 Construction rules

Section 3.3 formalizes Euclidean constructions as rules that introduce new diagram objects under explicit prerequisites and conclusions. The rule set models basic point, line, circle, and intersection constructions, while leaving the principled boundary of “obvious” constructions open.

Rule format: Construction rules have the form Π ⇒∃x⃗. Θ, where Π gives prerequisites and Θ characterizes the newly constructed objects.The variables x⃗ do not occur in Π, and the rules function as built-in theorems.
Rule format: The system distinguishes uniquely determined constructions, such as line intersections, from arbitrary choices, such as selecting a point on a line.Both are called construction rules because they introduce objects used in Euclidean constructions.
Basic constructions: Basic rules introduce arbitrary points, points on or between points on lines, points on specified sides of lines, and points inside or outside circles.The corresponding conclusions record incidence, betweenness, side relations, or circle location, together with distinctness conditions where required.
Geometric constructions: Further rules construct lines through distinct points, circles from centers and points, and intersections of lines, lines with circles, or pairs of circles.Intersection rules specify the relevant incidence, distinctness, betweenness, or same-side properties.
Geometric constructions: Circle-intersection rules 8 and 9 select the intersection on the same or opposite side of the center line from a reference point.These rules were included to model particular construction steps in the Elements, although some could be derived from more basic rules.
Scope and limitation: The rule list is sound and complete for the paper’s purposes, but lacks a principled account of which constructions count as “obvious.”The authors reject unrestricted introduction of points satisfying consistent constraints as potentially difficult to decide and conceptually too permissive.

3.4 Diagrammatic inferences

Section 3.4 introduces axioms that infer diagrammatic assertions from available diagram information. These axioms formalize identity, incidence, betweenness, and related line-order properties, while some are included for restricted notions of consequence even when derivable in first-order logic.

Axiom role: The axioms license diagrammatic inferences from information present in a proof context, with their precise use specified later in the system.They are initially presented as first-order axioms.
Incidence and circles: The incidence axioms state that two distinct shared points determine a unique line, circle centers are unique and inside their circles, and degenerate circles are excluded.The accompanying explanation identifies the geometric meaning of the first three axioms and the role of the final nondegeneracy axiom.
Betweenness: The betweenness axioms constrain symmetry, line incidence, nesting, ordering among three points, and incompatibility of competing betweenness relations.Together they axiomatize a strict betweenness relation on points lying on lines.
Betweenness: These betweenness axioms are closely related to an established axiomatization whose countable models embed as points on the real line.The paper notes that analogous completeness or representation results for other axiom groups would be interesting.
Betweenness: The axiom stating that a point between two others cannot also lie between them in the reverse configuration is a first-order consequence of the remaining axioms.It remains useful under the more restrictive consequence relation used later.

Same side axioms

The same-side axioms formalize how points are partitioned by a line and how same-side relations interact with betweenness and intersections. Additional rules capture Pasch-style separation and region structure around intersecting lines.

Same-side relation: The same-side axioms make “on the same side of L” an equivalence relation among points not on L.Any point off L partitions points into those on L, those on its side, and those on the opposite side.
Same-side relation: The axioms also derive how same-side and different-side relations compose relative to a fixed line.Two points different from a reference point lie on the same side, while a same-side and a different-side relation propagate the difference.
Pasch and regions: The Pasch-related rules encode how three lines meeting at a point divide the plane into regions.The cited figures group these rules visually, while the axioms specify the corresponding side relationships.
Interaction with betweenness: Betweenness axioms connect line separation with side relations, including side preservation, side switching across a line, and separation when the between-point lies on the line.An intersection condition also yields betweenness when points on a second line are separated by the first.

Triple incidence axioms

The triple-incidence axioms describe side relations among points on three lines meeting at one point. Circle axioms then constrain betweenness and side relations for points inside, on, or outside circles.

Triple incidence: The first three triple-incidence axioms relate side conditions on three concurrent lines and derive further same-side or different-side relations.Their hypotheses specify which points lie on which lines and how the points compare across the other lines.
Triple incidence: These axioms explain how three lines intersecting at one point divide space into regions.The paper explicitly identifies this regional interpretation as their geometric role.
Circle relations: The circle axioms characterize betweenness for a point inside a circle relative to two boundary points and preserve interiority along segments.They also state that extending a segment from an interior or boundary point through an exterior point reaches a point outside the circle.
Circle relations: For two distinct intersecting circles, their two intersection points lie on opposite sides of the line through the centers.This gives the side relation needed for the circle-intersection geometry encoded by the system.

Intersection rules

The system formalizes five intersection axioms for lines and circles, capturing transversal intersection under separation, containment, and crossing conditions. The third axiom excludes lines bounded by circles, while the others express continuity principles.

Intersection rules: The first axiom makes a line through points on opposite sides of another line intersect it.
Intersection rules: The second and third axioms ensure line-circle intersection when a circle straddles a line or a line passes through a circle.
Intersection rules: The fourth and fifth axioms provide analogous intersection conditions for pairs of circles.
Intersection rules: Five axioms specify when lines or circles must intersect under separation, containment, and crossing conditions.The axioms cover line-line, line-circle, and circle-circle intersections.
Intersection rules: The equality axioms are standard first-order logic principles and are treated as first-order consequences.

3.5 Metric inferences

Metric inferences formalize Euclid’s reasoning about nonnegative magnitudes using ordered addition, while adding explicit rules for degenerate triangles and congruent-triangle areas. Transfer inferences connect these magnitudes to diagrammatic facts.

3.5 Metric inferences: The metric structure uses nonnegative magnitudes with associative and commutative addition, zero, linear order, and order-preserving addition.These axioms describe the nonnegative part of any linearly ordered abelian group.
3.5 Metric inferences: The formalization applies this metric structure to segment lengths, angles, and areas.
3.5 Metric inferences: Degenerate triangles are assigned area 0.
3.5 Metric inferences: Congruent triangles are assigned equal areas, making explicit a fact Euclid uses without comment.
3.5 Metric inferences: Further transfer inferences relate diagrammatic facts to metric properties and are treated in the next section.

3.6 Transfer inferences

Transfer inferences connect diagrammatic configurations with segment lengths, angles, and areas. They encode geometric relations such as betweenness, circle membership, angle composition, right angles, line intersections, and area decomposition.

3.6 Transfer inferences: Transfer inferences are divided into segment-length, angle, and area groups.
3.6 Transfer inferences: Segment rules connect betweenness and center-radius conditions with circle membership and interiority.One axiom states that a circle is determined by its center and radius.
3.6 Transfer inferences: The circle axioms imply that a circle is determined by its center and radius, with a converse relation when the circles coincide.
3.6 Transfer inferences: Angle rules formalize zero angles, angle addition, right angles, ray-description invariance, and a non-parallel intersection condition.
3.6 Transfer inferences: The fifth diagram-angle transfer axiom formalizes Euclid’s parallel-postulate-style condition using angles less than two right angles.
3.6 Transfer inferences: The area rules characterize collinearity by zero area and express triangle-area addition when a triangle is divided.

3.7 Superposition

Superposition addresses Euclid’s SAS and SSS proofs without treating imagined constructions as newly available objects. In E, superposition functions as an elimination rule that supports conclusions about objects already present in the diagram.

3.7 Superposition: Euclid’s Proposition I.4 uses superposition to establish the side-angle-side congruence property.
3.7 Superposition: Superposition creates a foundational problem because copying the required angle relies on a proposition whose proof already depends on SAS.
3.7 Superposition: Adding construction rules for copied angles and triangles would directly model superposition but adds new construction machinery.
3.7 Superposition: Adding SAS and SSS as axioms is unsatisfactory because it does not explain why Euclid proves them.
3.7 Superposition: E treats superposition as an elimination rule: conclusions derived under hypothetical new objects apply to existing diagram objects, without constructing those objects.
3.7 Superposition: The formalization represents copied-object conditions as sequents and separates these assumptions from the conclusions drawn about existing objects.

3.8 The notion of a “direct consequence”

The paper defines direct diagrammatic consequence as a controlled closure process designed to model Euclid’s immediate diagram-based inferences while satisfying fidelity, soundness, completeness, and tractability requirements. In the resulting system, direct consequences are computable by rule closure and support formal correspondence results.

Direct consequences are defined as diagrammatic facts obtained by closing established assertions under specified inference rules.The closure captures the paper’s notion of what can be read directly from a diagram.
The definition is constrained to model Euclid faithfully, remain sound and complete with respect to diagrammatic reasoning, and be computationally tractable.The authors reject unrestricted first-order consequence because it would exceed Euclid’s explicit reasoning and may be computationally infeasible.
Rules may be chained, split conjunctive conclusions into separate rules, and used in contrapositive variants to derive further diagrammatic information.The contrapositive treatment is illustrated with Pasch-style betweeness and same-side relations.
In the propositional formulation, closure starts from given literals and repeatedly applies clauses until no further literals can be added, with contradiction entailing every literal.A clause adds its remaining literal when all other literals are negated in the current closure.
Direct consequence avoids excluded-middle case splits, preserving a distinction between diagrammatic inference and classical consequence.With case splits, consequence becomes NP-complete, whereas direct-consequence checking is polynomial in the propositional setting.
The system is sound and complete for the intended diagrammatic consequences, and direct consequence for assertions involving at most n geometric objects is decidable in polynomial time.The paper also establishes decidability for first-order consequence under its full collection of axioms.

4 Comparison with the Elements

E translates Euclid’s language and diagrammatic reasoning into a formal system while preserving key proof practices. The comparison also exposes where Euclid’s abbreviated arguments require fuller case analyses or differ from E’s axioms.

4.1 Language: E uses a minimal language that translates Euclid’s finite segments and extensions into points and lines, with the differences treated as relatively minor.The translation distinguishes bounded diagrammatic information from entire lines while retaining a straightforward correspondence with Euclid’s terminology.
4.1 Language: E represents diagrammatic assertions such as betweenness and sidedness, using transfer axioms to license construction steps and explicit metric inferences.These primitives are designed primarily to track the information needed internally, even when Euclid leaves it implicit or conveys it through the physical diagram.
4.1 Language: E can model areas of convex quadrilaterals by defining them as sums of triangle areas, while arbitrary convex polygons would require a more substantial extension.The Elements does not require the latter extension because arbitrary-sided convex polygons never arise there.
4.2 Examples of proofs in E: E formalizes Euclid’s circle-center construction naturally as ∃a .center(a, γ), and its proof remains essentially Euclid’s.Using a relation rather than a function permits a circle to be given without its center already being selected.
4.2 Examples of proofs in E: E requires a metric proof that a circle’s chord lies inside the circle, thereby accounting for a fact that appears directly readable from a diagram.This example illustrates how E can explain why some seemingly obvious geometric facts are proved in the Elements rather than treated as diagrammatic assertions.
4.3 Departures from the Elements: Euclid’s abbreviated proofs depart from E chiefly when E requires separate case analyses or transfer-rule licenses for relations read directly from diagrams.For Proposition I.35, Euclid’s proof establishes only a weaker result under an additional nonintersection condition, while E requires separate treatment of the positional cases.
4.4 Euclid’s postulates and common notions: E’s axioms distribute Euclid’s postulates and common notions across construction rules, diagram inferences, metric inferences, and transfer inferences.The mapping is not clean because E makes explicit diagrammatic understanding that Euclid leaves implicit in definitions and undefined terms.

5 Completeness

The paper proves that E is sound and complete for ruler-and-compass constructions, using translations to and from a suitably restricted variant of Tarski’s system. The completeness argument combines geometric rules, cut elimination, and translations that preserve validity and provability.

5 Completeness: E is not complete for the full Euclidean-plane semantics because ruler-and-compass constructions cannot trisect a sixty-degree angle.The paper also notes that E cannot prove or refute the existence of an equilateral triangle with a trisected angle.
5 Completeness: E is sound and complete for ruler-and-compass constructions: a sequent is valid exactly when it is provable in E.This is Theorem 5.1’s central result.
5 Completeness: The completeness proof is presented as a chain of validity and translation results rather than as a direct construction of a countermodel for every unprovable sequent.The indirect route avoids the difficulties created by E’s restricted logic and Tarski’s richer first-order system.
5 Completeness: Tarski’s axioms are reformulated as geometric rule schemes, enabling cut elimination and proofs whose intermediate sequents retain restricted geometric complexity.Cut-free proofs use only subformulas of the endsequent, together with possibly additional atomic formulas.
5 Completeness: The proof introduces a variant T of Tarski’s system, together with translations π from E to T and ρ back to E.T is chosen to retain soundness and completeness for ruler-and-compass constructions while providing useful proof-theoretic properties.
5 Completeness: The translation π preserves ruler-and-compass validity, and the reverse translation ρ converts cut-free T proofs into proofs in E.The completeness proof applies these lemmas in sequence: validity in E’s target semantics, cut-free provability in T, translation back through ρ, and recovery of the original sequent.

6 Implementation

The authors investigate computational verification of Euclidean-style proofs using formal rules, theorem provers, and SMT solvers. Preliminary results support checking diagrammatic inferences, but the studies remain suggestive and do not address automatic construction discovery.

Proof checking: E is intended to support a computational proof checker that verifies Euclid-like proof texts against the system’s rules.The checker would take proofs resembling those in the Elements and verify their correctness.
Proof checking: Direct diagram inferences are first-order consequences of universal axioms and diagram literals, with no function symbols.These properties make the relevant problems suitable for off-the-shelf first-order theorem provers.
Preliminary studies: A five-line, six-point diagram yielded instantaneous verification of several consequences in the systems E and Spass.The passage reports a small preliminary experiment using TPTP-formatted axioms and consequences.
SMT implementation: SMT solvers are proposed as a complete back end because they support quantifier-free logic, incremental fact management, and linear arithmetic.The proof checker would parse an input proof, assert relevant facts, and check claimed consequences.
Limitations: The computational evidence is preliminary: performance depends on language and axiom formulation, and more experimentation is needed.Replacing strict with nonstrict betweenness reduced performance, so the reported data is only suggestive.
Scope: The system verifies smaller diagrammatic inferences given higher-level structure and construction, but does not solve automatic construction discovery.The authors distinguish verification from finding the constructions required by Euclidean proofs.

7 Conclusions

The paper presents a formal analysis of Euclidean proof that models the argumentative structure of Books I–IV while preserving the role of controlled diagrammatic inference. It establishes semantic and computational support for treating Euclid’s proofs as close to formal proofs, while delimiting historical, cognitive, and philosophical claims.

Summary of results: The analysis provides a clean account of the argumentative structure of proofs in Books I–IV of the Elements.The authors also identify ways in which proofs in E differ from Euclid’s presentations.
Summary of results: The system models individual inferences licensed by Euclidean practice rather than only geometric validity or entailment.This makes line-by-line comparison with Euclid’s proofs possible.
Summary of results: E is sound and complete for an appropriate semantics of ruler-and-compass constructions.Under the assumption that E captures Euclidean practice, this supports the accuracy of modern semantics for provable Euclidean theorems.
Summary of results: Initial automated-reasoning experiments suggest that developing a formal proof checker for E should not be difficult.Separating metric and diagrammatic data makes each component more manageable and suggests a broader formal-verification strategy.
Broader issues: The project’s logical analysis deliberately screens off cognitive, historical, and broader philosophical questions about diagram use.The authors present the analysis as a foundation that can support those studies without explaining how Euclidean norms arose or why they should be followed.
Broader issues: The analysis focuses on Heath’s translation of Heiberg’s version of the Elements, although the authors expect most findings to remain robust across editions.Earlier diagrams’ overspecification is presented as consistent with the distinction between diagrammatic and metric information.