40

The aim of this article is to study Euclid’s plane geometry, relatively to Book I of the Elements, from a formal point of view. Instead of making appeal to some already existent logical framework, we introduce a new formal language, as well as a new system of rules, specifically tailored to give a faithful reconstruction of Euclid’s proof practice. Such a reconstruction shows that Euclid’s work can be understood as resting on a very peculiar inferential setting, involving much more mathematics than logic (understood as a general framework of reasoning): inference rules essentially deal with geometric objects and their relations, while no propositional connectives nor quantifiers are present.

L’objectif de cet article est d’étudier la géométrie plane d’Euclide, relativement au Livre I des Éléments, d’un point de vue formel. Au lieu de faire appel à un cadre logique préexistant, nous présentons un nouveau langage formel ainsi qu’un nouveau système de règles spécifiquement conçu pour reconstruire fidèlement la pratique démonstrative d’Euclide. Une telle reconstruction montre que le travail d’Euclide peut être compris comme reposant sur un cadre inférentiel très particulier, faisant intervenir les mathématiques plus que la logique (entendue comme cadre général de raisonnement): les règles d’inférence traitent essentiellement d’objets géométriques et de leurs relations, sans recours à aucun connecteur propositionnel ni quantificateur.