A Formal Exploration of Constructive Geometry

Sarah Sernaker and Robert L. Constable Sept 2016

Abstract

We investigated synthetic (coordinate-free) geometry and propositions from Euclid's Elements using constructive mathematics and utilizing results from Beeson, Tarski, Hilbert, and of course, Euclid. Our theory in Nuprl is built using Beeson's constructive version of Tarski's theory of geometry. A few of the propositions from the first book of Elements were formalized in Nuprl. The proofs done in Nuprl and the original proofs by Euclid are both presented in order to compare the constructive and classical logics used. Interactive diagrams accompany all of the lemmas and propositions presented here. They're for the reader to manipulate, under the constraints of the lemma or theorem it depicts, and to test cases that Euclid doesn't consider, such as degenerate cases.

Euclid's propositions

References

Introduction & History

Synthetic geometry stemming from Euclid's Elements is the study of the relative position of points and lines and the properties of the space or figures they define. Synthetic geometry, and the constructive geometry presented here, strive to remain as abstract as possible in such a way that, as Hilbert stated, we should be able to replace points, lines, and planes in Euclid's proofs with tables, chairs, and beer mugs, as the names of the entities are just place holders. In other words, we wish to define a precise abstract geometry such that the properties of the constructions, built with any entity, are consistent regardless of what they may be; the reasoning should still be valid. The concepts and axiomatic reasoning from Euclid's Elements have strongly influenced prominent mathematicians across various fields since its writing.

Euclidean geometry has been of enduring interest to mathematicians, logicians, scientists, engineers and students for over 23 centuries, and to computer scientists for half a century. One enduring goal is to understand the nature of space and time, the continua in which we live. Most of our tools for thought are grounded in discrete phenomena: symbols, words, digits, numbers, and expressions. We use these to construct an understanding of the continua. We strive to impose a "digital order", and we have built digital computers using symbolic language to help us understand the most difficult concepts.

Classic vs constructive geometery. Euclid uses classical reasoning to prove his propositions. Though, while Euclid doesn't use constructive reasoning by way of intuitionistic logic, his proofs are often referred to as 'constructions' and the Elements is therefore referred to in some papers as 'constructive geometry.' It is referred to as 'constructive geometry' because Euclid's proofs provide steps using a straightedge and compass to construct geometric diagrams. However, our use of the term constructive geometry will henceforth refer to geometric proofs using intutionistic, or constructive, logic. This account is interesting to type theorist because it provides an abstract account of geometric concepts, thus illustrating the ability of constructive type theory to capture abstract computational ideas as well as those grounded in concrete types such as the natural numbers and constructive reals.

Using the interactive diagrams. Diagrams are essential when studying geometry. If there were no diagrams to accompany this exploration, the reader would surely try to imagine the diagram themselves while reading, or the maybe try to draw it themselves. However, this would only provide one instance of the geometric relationship. The interactive diagrams are to encourage the reader to experiment with different cases and representations of the geometry, such as degenerate cases. They are rendered on a coordinate-free space to maintain the abstractness and to demonstrate that the relationships will hold, as long as the assumptions remain, no matter how the figure is oriented or distorted from the initial depiction. These diagrams hope to contrast the static diagrams drawn in Elements, or elsewhere, which only provide one actualization that usually corresponds to an ideal visualization.

The diagrams were rendered by following as exactly as possible the constructions by each Euclid, Tarski, and Beeson. The points in the diagrams that can be moved are those given from the assumption, the rest of the diagram moves dependently on these. For example, Proposition 1 from Euclid's Elements constructs an equilateral triangle by intersecting two circles and using one of the intersection points as a vertex in the triangle. We are given points A and B to start, from which the rest is built. Therefore A and B are able to be moved in this diagram however the intersection point C is not able to be moved by the user since it is strictly consequence to A and B. The diagrams of Euclid's propositions depict the conclusion of each proposition. Additionally, a step-by-step construction of Euclid's propositions can be followed using the buttons under the diagrams.

Euclid (300 BCE)

Euclid's Elements may be the longest standing mathematical textbook. Comprised of 13 books, it is an exemplar of axiomatic and deductive reasoning, conveyed through classical geometry. We used and reference therein the Thomas Heath translation of the Elements [6]; we focus only on a selection of propositions from the first book in this investigation.

Euclid's geometry is based on ruler and compass constructions, specifically the 'collapsible' compass - one that 'collapses' as soon as it is picked up. Euclid's Elements is not without errors however, he often omits alternative cases, the postulates are not always stated precisely, some proofs are logically incomplete, and more. Euclid employs the use of geometric diagrams to accompany his proofs - sometimes relied on as picture proofs, however many of Euclid's proofs rely too heavily on the accompanying diagram, which undermines the deductive reasoning of the proof itself. The accompanying diagrams only provide one particular instance of the construction defined.

Euclid has 23 definitions of primitives in the beginning of Book 1. These include the definition of a point, a line, a plane (called surface in the text), a circle, types of angles, types of triangles, other polygons, and parallelism. He then states 5 postulates: that two points can be joined by a line, a line can be drawn infinitely long, a circle can be constructed with any center and diameter, all right angles are equal, and the parallel postulate.

The parallel postulate states that if a straight line crossing two straight lines make the interior angle on the same side less than two right angles, then the two straight lines, if extended infinitely, will meet. While Euclid's first 4 postulates are straightforward, the parallel postulate is stated more like a proposition rather than something that should be taken as basic truth. Euclid is often criticized for adding this as a postulate and it's thought that Euclid added this postulate only when he could not proceed without it, at Proposition 29 (Book 1).

This postulate is represented in the diagram to the right. We see that the interior angles of the two vertical lines add up to 180 degrees. If the interior angles do not add up to 180 then the parallel postulate states that the lines will intersect at some point.

5 common notions follow the 23 definitions and 5 postulates. It is debatable whether Euclid defined those himself or if they were added in later editions. They are: things which are equal to the same thing are also equal to each other (i.e. if ab=cd and cd=ef then ab=ef); if equals be added to equals the wholes are equal (i.e. if ab=AB and cd=CD then ab+cd = AB+CD); if equals be subtracted from equals, the remainders are equal (i.e. if ab=AB and cd = CD then cd-ab=CD-AB); things which coincide with one another are equal to one another; and, the whole is greater than the part.

Hilbert (1899)

Hilbert wanted to create a simpler and complete set of independent axioms that would more precisely define Euclidean geometry [7]. He defines a second-order theory over five groups of axioms. Hilbert uses points (A,B,C), straight lines (a,b,c), and planes (α, β, γ) as his primitives and applies three primitive relations: betweenness, a ternary relation between points; 'lies on', three binary relations between points & lines, points & planes, and lines & planes; and congruence, two binary relations for lines segments and another for angles.

His theory was comprised of:

Axioms of connections. 7 axioms and 2 theorems to establish a connection between the points, lines, and planes. Hilbert defines a sense dimensionsionality in this group of axioms, stating that two distinct points define a line, and 3 distinct points define a plane.
Axioms of order. 5 axioms and a definiton to define the idea expressed by 'between' and define an order of sequence of points upon a straight line and plane.

Hilbert makes use of Pasch's theorem (1882), which is not derivable from Euclid although Euclid used this property and implications thereof throughtout the Elements. Pasch's theorem states: given points a,b,c, and d on a line, if it is known that the points are ordered as (a,b,c) and (b,c,d) then it is also true that (a,b,d).

Axiom of parallels (Euclid's Axiom). This single axiom defines the property of parallels and the uniqueness of those lines. Hilbert extends the latter idea into a theorem.
Axioms of congruence. 6 axioms and 1 definiton define congruence relations through commutativity and associativity. He does this not only for line segments but angles as well.
Axiom of continuity (Archimedean Axiom). This axiom introduces the idea of continuity to geometry. With the addition of the Axiom of Completeness, Hilbert shows that it is possible to establish a bijection between abstract points and the system of real numbers.

The consequences of the axioms of connections and the axioms of order yield an intuition of the infinitude of geometry and geometric space. One theorem Hilbert presents as consequence to these two groups is that there are an infinite number of points between two endpoints of a line segment. He extends these ideas to planes and defines some of their infinite properties. The consequences of the Axioms of Congruence yield the definition of supplementary angles, vertical angles, right angles, and congruent triangles. From these axioms we can also prove the SAS and SSS property. These ideas preface the Axiom of Continuity, which together with the completeness axiom says it is possible to map Euclidean geometry to the real numbers. This idea provides foundational groundwork that ultimately led to the coordinatization of Euclidean geometry.

Tarski (1958)

Tarski wanted to simplify Hilbert's theory, which has many axioms and is second-order. He makes use of the term elementary geometry, which he describes as follows [9,10].

We regard as elementary that part of Euclidean geometry which can be formulated and established without the help of any set-theoretical devices.

Tarski defines his theory using first-predicate calculus with points as the only primitive. He realized that everything could be defined using points only, e.g. line segments are defined as two distinct points, and triangles and angles as three distinct points. Tarski defined two predicates to describe the betweenness relation and the equidistant relation. β(xyz) represents betweenness, as in y lies between x and z. δ(xyzu) represents the equidistance relation that says x is as distant from y as z is from u.

Since Tarski didn't use set-theoretical bases there are no variables or symbols to represent geometric figures. However, these can be expressed with points and the defined predicates, as every geometrical figure and subsequent properties are determined by a fixed finite number of points.

Tarski's system consisted of 13 axioms, one of which represents the collection of all elementary continuity axioms. The first three axioms are the identity, transitivity, and connectivity axioms for betweenness. The following three are the reflexivity, identity, and transitivity axioms for equidistance. The seventh axiom is Pasch's Axiom, which is defined above under Hilbert's axiom of order. The eighth is Euclid's axiom, then the Five-Segment Axiom, Axiom of Segment construction, lower dimension axiom, and the upper dimension axiom, then finally the elementary continuity axioms.

Beeson (2009)

Although Hilbert refined Euclid's idea of geometry, and then Tarski further so, neither theory was totally constructive, so Beeson refined Tarski's theory to make it constructive [2,3,4,5].

Beeson's axioms are mostly unchanged from Tarski. One major difference, besides the use of intuitionistic logic, is Beeson's use of strict betweenness, where Tarski uses non-strict betweenness. In fact he defines non-strict betweenness, T(p₁,p₂,p₃), in terms of strict betweenness, B(p₁,p₂,p₃): T(a,b,c) = ¬(a ≠ b ∧ b≠c ∧ ¬B(a,b,c)). Beeson also redefines colinearity in terms of strict betweenness. Tarski defines collinearity as follows: Col(a,b,c) ≡ T(a,b,c) ∨ T(b,c,a) ∨ T(c,a,b). We can see that this isn't constructive because it poses a decidability problem. Beeson redefines the above definition of collinearity to: a≠b ∧ ¬(¬B(p,a,b) ∧ ¬B(a,p,b) ∧ ¬B(a,b,p) ∧ a≠p ∧ b≠p) - the double negation of Tarski's definition.

There are a few other subtle changes Beeson makes from Tarski's system in order to create a constructive theory. Beeson restricts Tarski's fourth axiom of segment extension so that the given points must be distinct. Beeson changed Tarski's Identity for Betweenness from T(a,b,a)⇒ a=b, to ¬B(a,b,a). Beeson adds constraints on Tarski's inner-Pasch axiom, using strict betweenness for points a, p, and c (see here for reference) and adding the property that points a, b, and c are not colinear. Beeson adds symmetry and inner transitivity of betweenness, two properties that Tarski didn't explicitly define in his axiom system. His definition of collinearity replaces Tarski's in each axiom it is used. Beeson uses what he calls two-point line-circle continuity, instead of Tarski's segment-circle continuity. Two-point line-circle is different from segment-circle in its quantifications and adding the additional constraints of distinct points. Finally, Beeson adds the stability axioms (E(a,b,c,d) is defined as ab=cd):

¬¬B(a,b,c) → B(a,b,c)
¬¬E(a,b,c,d) → E(a,b,c,d)
¬a≠b → a=b.

It is after these adjustments to Tarski's system that we have a constructive theory of geometry from which we can formalize Euclid's propositions.

Relationship to Homotopy Type Theory

The growth of geometry from Euclid to homotopy theory has been driven by expanding the notion of when two geometric objects are "the same." Our goal is to tell parts of that story through the formal mathematics in the Nuprl library. Brouwer demonstrated that his "intuitionistic" approach to understanding such fundamental notions as point and line lead to a more computational approach to mathematics generally. The Nuprl system is grounded in many insights from Brouwer, Poincaré, and other constructively inclined mathematicians and computer scientists.

We believe that this line of inquiry has become richer and more productive over the years, and we expect that new computational insights will arise from this "geometry inspired" line of research. We would like to formalize in constructive type theory important landmarks along this line of research and contribute to elaborating and extending it. Already at the very start, with Euclid, there are deep challenges that our development will highlight. It might even be possible that some of the new ideas emerging from our constructive formalization of homotopy theory will shed new light on the important landmarks.