Euclid's propositions
We present Euclid's propositions 1, 2, 3, 4, 5, and 8 and their proofs formalized in Nuprl. The Nuprl proofs do not always reflect Euclid's since his reasoning was not always constructive. Propositions 6 and 7 are not formalized in Nuprl at the time of this writing because Euclid's proofs for these were by contradiction and not constructive, and the constructive proof was not obvious to the author. The author believes that the proof might be solved by applying some combination of the five-segment or inner five-segment, three-segment or inner three-segment, and perhaps the inner-Pasch property.
The propositions are stated as they are written in Euclid's Elements [7] at the top of each page, followed by a short elaboration, then the interactive diagram and the proof of the proposition as it's written in Elements. Under the diagrams are buttons to follow Euclid's step-by-step construction of the diagram. And then finally, the proof of the proposition in Nuprl. Refer here to learn how to step through a proof in Nuprl: /MathLibrary/MaximumSegmentSum/proof_howto.html. The labels on the points, line, circles, etc. coincide with Euclid's proof to the right and may not be exactly consistent with the variables use in Nuprl.
The statement of the propositions in Nuprl may slightly differ from Euclid's because we impose first-order logic onto his propositions and we only have points as primitives. Constructions are defined in terms of distinct points; a line segment is a pair of points, triangles and angles a triple of points, and a circle is defined by a center point and a radius (a pair of points). All points are defined over the Euclidean plane.
How to read Euclid. Euclid does not employ the use of quantifiers, and hardly uses any logical expressions ("every", "or", "if...then",..). Rather he makes assertions in sometimes seemingly incomplete sentences, using infinitives and passive imperative tense. For example, his first postulate states: "To draw a straight line from any point to any point."Proclus in his book [8] described that every theorem has the following elements: enunciation, setting-out, definition or specification, construction or machinery, proof, and conclusion. Enunciation states what is given and/or what is sought. Setting-out describes what primitives are given and their relationship to each other in the context of the propostion. Definition or specification distinctly states what particular goal is sought. Construction or machinery describes the steps necessary to acheive the goal, e.g. joining points, constructing lines or circles, etc. The proof uses the required inferences as evidence that the goal has been accomplished through the construction steps. The conclusion refers back to the enunciation, confirming what has been demonstrated. The principal components are the ennunciation, proof, and the conclusion; every theorem contains these elements. The other elements may not be as distinctly recognized sometimes because they are subsumed by one of the three principal components.
Euclid references postulates, definitions, common notions, and prior propositions when going through a proof. These have been included in the proofs with hover-over pop up definitions, to more easily follow Euclid's reasoning.
Index