Spinoza en Coq : démonstration complète des premières propositions de l’Éthique

National audienceL’Éthique de Spinoza est un traité philosophique écrit « à la manière des géomètres » : les théorèmes y sont démontrés à partir de définitions et d’axiomes initialement posés. Peut-on garantir la validité de démonstrations de Spinoza, et si oui, à quelles conditions ?La tâche a été entreprise « à la main » par l’historien de la philosophie Martial Gueroult au tournant des années 1970. Pour emporter l’adhésion, ce travail devrait être vérifié ligne à ligne par un lecteur parfaitement rigoureux, hélas inexistant. Or depuis quelques décennies, les « assistants à la démonstration » tels que Coq sont des logiciels qui permettent de produire des démonstrations mathématiques complètes et certifiées. Nous présenterons donc la démonstration en Coq des premières propositions de l’Éthique de Spinoza.Cette méthode présente un réel intérêt pour l’historien de la philosophie : elle permet non seulement de montrer certains détours « inutiles » dans les démonstrations de Spinoza, mais aussi de mettre au jour certains axiomes implicites de l’Éthique. Ces axiomes n’ayant métaphysiquement rien de trivial, on gagnerait à les expliciter. Par ce cas concret, on verra une fois de plus ce que les sciences formelles peuvent apporter à l’histoire « structurale » de la philosophie, qui, dans la lignée de Martial Gueroult et de Jules Vuillemin, travaille à reconstituer l’architecture interne des systèmes philosophiques