Formalizing the logic and proofs of Book I of Euclid's \textit{Elements}: some examples (Q6962006)

The authors' aim is to study from a formal point of view Euclid's plane geometry, of which only the first three postulates, the common notions, and the first three propositions of Book I of the \textit{Elements} are actually formalized in this paper.\N\NTo this end, they introduce a new formal language, each term of the language standing only for one object, the object being of a certain sort (with \textit{points}, \textit{segments}, and \textit{circles} as the elementary sorts), as well as a new system of rules, aimed at providing ``a faithful reconstruction of Euclid's proof practice.'' The inference rules are unlike those encountered in traditional logical systems, as they deal with geometric objects and their relations, in the absence of logical symbols such as connectives or quantifiers.