Formalizing the logic and proofs of Book I of Euclid's \textit{Elements}: some examples
History of Greek and Roman mathematics (01A20) History of mathematical logic and foundations (03-03) Philosophical and critical aspects of logic and foundations (03A05) Subsystems of classical logic (including intuitionistic logic) (03B20) Foundations of classical theories (including reverse mathematics) (03B30) History of geometry (51-03)
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.
This page was built for publication: Formalizing the logic and proofs of Book I of Euclid's \textit{Elements}: some examples
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6962006)
