Spinoza en Coq

L’É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.

Cette conférence est organisée dans le cadre de l’axe Fondements politiques et culturels de l’éducation de la Fédération de recherche EDUC. Elle fait partie du séminaire « Philosophie, mathématiques, neurosciences ».

Baptiste Mélès est chargé de recherche au CNRS, rattaché aux Archives Henri-Poincaré de Nancy et associé au laboratoire Philosophies et rationalités de Clermont-Ferrand.