## 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