Geometry in Nuprl
We define our Euclidean structure as a dependent record type that defines the basic types and operations of Beeson's constructive version of Tarski's geometry. The first field of the record is the type "Point", for which all other fields depend on. We define the congruence relation ab=cd, both the strict and non-strict betweenness relation a-b-c and a_b_c respectively, and colinearity, which is a needed concept for the operators 'extend', 'inner-pasch', 'line-circle', and 'middle'.We then use the defined primitives of the Euclidean structure to define the 12 axioms that give Beeson's constructive version of Tarki's axioms. Tarski's formalization of synthetic geometry consisted of 13 axioms that were defined using only two predicates over points: the betweenness relation and the equidistance relation.
Having defined the Euclidean structure and Euclidean axioms, we can define the Euclidean plane. The Euclidean plane is defined simply as a Euclidean structure that adheres to the Euclidean axioms.
Definitions
The definitions below are those that define the Euclidean structure. This includes points, from which everything else is constructed, segments, congruency, betweenness- strict "B".(a-b-c) and non-strict "T".(a_b_c), and so on. The definiton of eu-O, eu-X, eu-seg1, eu-seg2, and
eu-length are included here although they're not primitive definitions of the structure, they are necessary in the definition of eu-extend.
The following definitions, and the majority of the definitions of the Nuprl geometry theory, are defined on the Euclidean plane.
Triangles.
We think of triangles are three distinct points, rather than perhaps three line segments.
Congruent triangles are defined as two triangles having all respective sides equal by a length relation.
Triangles are incorporated in almost every one of Euclid's propositions in Book 1.
Angles.
Defining angles is tricky because we don't want to impose measurements such as radians or degrees.
Euclid defines angles in terms of right angles: a right angle is the intersection of two lines such that the angles they create are equal, an obtuse angle is greater than a right angle, and an acute angle is smaller than a right angle.
He doesn't give an explicit definition of angle equality though; he uses a more intuitive notion. In his proof of the SAS property, Proposition 4, he
'applies' one triangle to the other in order to prove the angles are congruent. Euclid doesn't give any precise explanation of his triangle application argument.
Since Euclid's definition of angle equality is not constructive we used Beeson's definition. If we want to show that angle ABC is equal to XYZ then we extend BA by BC and BC by BA, call the new segments BA' and BC'. We do the same to the respective sides of XYZ, extend YX by YZ and extend YZ by YX, and get YX' and YZ'. By doing this we ensure that BA'=BC' and YX'=YZ'. Now to show that the angles are equal we have to show that A'C'=X'Z'. Essentially, we construct triangles from the angles we wish to compare, and if we can show that the triangles are equivalent then the angles will be equivalent.
Lemmas
The lemmas chosen to be highlighted here, amongst the many other lemmas in this theory, are foundational to proving Euclid's propositions constructively.
ColinearityWhen considering colinearity of points a,b, and c we could consider whether a is between b and c, or if b is between a and c, or if c is between
a and b.
However, instead of posing the theorem as (b-a-c) ∨ (a-b-c) ∨ (a-c-b), which is a decidability problem, we pose the lemma as
(¬b-a-c) ∧ (¬a-b-c) ∧ (¬a-c-d). This says that it isn't possible for
each of point to between the other two, therefore only one
of the points has to be between the other two.
Inner-Pasch Property
Hilbert's fourth betweenness axiom was sometimes referred to as Pasch's axiom because it was first studied by Pasch. Tarski considered two restricted versions of Pasch's axioms - inner and outer Pasch. The inner-Pasch property says that if you have a triangle ACQ and a point B such that C-Q-B, then extending a line segment from any point P on AC (such that A-P-C) to B will result in an intersection point X on the opposite side of that which P is on.
Five-Segment Theorem
The five-segment theorem was Tarski's replacement for Hilbert's fourth and fifth congruence axiom. This lemma was crucial for the constructive proof of the SAS theorem. It states that if we have congruent triangles, ADB and EFH, and congruent line segments BC and HG such that A-B-C and E-H-G, then DC and FG will be equal as well.
Three-Segment Theorem
This theorem says that two lines are equal if their respective partitions are equal (sometimes called the betweenness theorem for points, or the partition property), i.e. AC=ac if ab=AB and bc=BC.
Inner Five-Segment Theorem
This is a variation of the five-segment theorem; instead of trying to prove that DC=FG we want to prove DB=FH. This says that if we have two congruent triangles, and we have points B and H such that A-B-C and E-H-G and AB=EH and BC=HG then we can say that DB=FH.
Inner Three-Segment Theorem
This is a variation of the three-segment theorem. Whereas the three-segment theorem states that two lines are equal if the partitions that make up the line segment are equal, the inner three-segment theorem states that respective partitions of two line segments are equal if their wholes are equal and if the remaining partitions are equal. So instead of adding two equal parts to get equal wholes, we are taking the whole and subtracting equal partitions to say that the remaining respective partitions are equal.
Line-Circle Continuity
This lemma is important because it allows us to extract intersection points between a line and a circle, which is helpful in proving some of the propositions. Line-circle continuity says that if a line passes through a point that is inside a circle then the line will intersect the circle at 2 points.
We draw three circles at center A with radii AX, AB, and AY such that A_X_B and A_B_Y. This ensures that we have a point X inside the circle defined by AB and a point Y outside the circle defined by AB. Then we can take two more points, one point on the circle defined by AX and one on the circle defined by AY, such that AP=AX and AQ=AY. If we extend a line that goes through both P and Q, we will get two intersection points with the circle defined by AB, Z and W, such that AW=AB and AZ=AB (since they are all on the same circle), and Z_P_Q and P_W_Q.
Circle-Circle Continuity
The circle-circle continuity principle is necessary to prove Proposition 1 and subsequently other propositions that rely on Proposition 1. The circle-circle continuity principle says that if a point on the circle K is strictly inside another circle H, and another point on K is strictly outside of H then the circles intersect at two points.
We draw this similar to the line-circle continuity in that we draw three circles using the radii AX, AB, and AZ such that A_X_B and A_B_Z to ensure that the circle defined by radius AB is between the circles defined by AX and AZ. We can take a point P on the circle defined by AX, which is inside the circle H (the dotted circle), therefore we have AP=AX. In a similar fashion, we can get a point Q on the circle defined by AZ, so that Q is outside circle H and AQ=AZ. Then if we construct a circle K that goes through both of these points, we will get two intersection points on circle H, Z1 and Z2.
Index