A formal exploration of constructive geometry
Main page

## Proposition 1

On a given finite straight line to construct an equilateral triangle.

This proposition simply states that given a finite straight line (i.e a line segment: two distinct points) it is possible to construct an equilateral triangle. If we wanted to write this using logical expressions we would state: for all a and b distinct points (of the Euclidean plane), there exists another point c, such that ab=ac=bc. This is exactly the goal that we prove in Nuprl below. The diagram below constructs this relation between points a, b, and c, such that following these steps, we are always gauranteed an equilateral triangle. Nuprl's procedure for proving this correct closely follows Euclid's construction for this proposition; this is not be the case for all of the propositions proved in Nuprl.

Points A and B below can be moved and will subsequently affect the circles and intersection points.

 div.scroll { overflow: scroll; width:350px; height:500px; overflow-x: hidden; } .tooltip1 { position: relative; display: inline-block; border-bottom: 1px dotted black; } .tooltip1 .tooltiptext1 { visibility: hidden; width: 120px; background-color: white; color: black; text-align: center; border-radius: 3px; padding: 5px .5px; border-style: solid; border-color: black; border-width: 1px; /* Position the tooltip */ position: absolute; z-index: 1; } .tooltip1:hover .tooltiptext1 { visibility: visible; } Let AB be the given finite straight line. Thus it is required to construct an equilateral triangle on the straight line AB. With centre A and distance AB let the circle BCD be described; [Post. 3]To describe a circle with any centre and distance. Again, with centre B and distance BA let the circle ACE be described; [Post. 3]To describe a circle with any centre and distance. And from the point C, in which the circles cut one another, to the points A, B let the straight lines CA, CB be joined. [Post. 1]To draw a straight line from any point to any point. Now, since the point A is the centre of the circle CDB, AC is equal to AB. [Def. 15]A circle is a plane figure contained by one line such that all the straight lines falling upon it from one point among those lying within the figure are equal to one another. Again, since the point B is the centre of the circle CAE, BC is equal to BA. [Def. 15]A circle is a plane figure contained by one line such that all the straight lines falling upon it from one point among those lying within the figure are equal to one another. But CA was also proved equal to AB; therefore each of the straight lines CA, CB is equal to AB. And things which are equal to the same thing are also equal to one another; [C.N.1]Things which are equal to the same thing are also equal to one another. therefore CA is also equal to CB. Therefore the three straight lines CA, AB, BC are equal to one another. Therefore the triangle ABC is equilateral; and it has been constructed on the given finite straight line AB. (Being) what it was required to do.

### Proof in Nuprl

Index

Website feedback
PRL Project   |   Computer Science Department   |   Cornell University
nuprl@cs.cornell.edu   |   320 Gates Hall, Ithaca, NY 14853   |   © 2014 Cornell University
site admin | Prof Constable's Library | PRL SourceForge Project Page