Implementing Euclid's straightedge and compass constructions in type theory (Q2631963)

The article illustrates how to formalise Euclid's constructions by straightedge and compass in a variant of constructive type theory. The core of the work presents a set of axioms implemented in the Nuprl proof assistant, to encode the fundamental constructions of Euclidean geometry in the plane. The Euclidean plane is rendered by the type of points equipped with four relations: \textit{congruence}, to express when two segments have the same length; \textit{betweenness} to say when a point lies between two other points; \textit{apartness} to model when two points are separated; and \textit{leftness} to declare when a point is on the left of an oriented segment from a point to another one. Using these primitives, the three fundamental constructions can be readily expressed: given two segment suitably placed in the plane, they intersect and the point of intersection is identified as a term in type theory; given a segment and a circle suitably placed in the plane, the segment can be extended to a new one whose endpoints, identified as terms in type theory, intersect the circle; finally, given two circles suitably placed in the plane, their intersections are identified as terms in type theory. In addition, it is postulated that, fixed two separated points, every point \(P\) in the plane is separated from one of them: the postulate also identifies which point is separated from \(P\). On this basis, the work shows how the initial propositions of Euclid's \textit{Elements} can be deduced. Finally, the paper discusses which kind of models are admissible for these axioms, considering the constructive nature of the system. The contribution is well written and very clear. It also provides a brief but comprehensive set of references to other formalisations in the same line. The proper scientific content is accessible also to non experts with a little effort, while the paper still provides insights and ideas to the specialist.