Voir le projet sur GitHub

Baruch Spinoza

Baruch Spinoza (1632-1677)

Charles Jarrett

Charles Jarrett, auteur de "The Logical Structure of Spinoza's Ethics, Part I" (1978)

Ce projet est une formalisation en Coq des propositions du Livre I de l’Éthique de Spinoza, selon la formalisation logique proposée par Charles Jarrett dans son article “The Logical Structure of Spinoza’s Ethics, Part I” (1978).

Le PDF des preuves en Coq !

Mise en garde

Ces démonstrations reposent sur une interprétation philosophique (puisque c’est une formalisation) de l’Ethique, et donc sont responsabilité partagée de Spinoza et de Charles Jarrett.

Contenu du projet

Le fichier principal De_Deo.v contient :

  • Les définitions formelles des opérateurs modaux (nécessité logique, possibilité, nécessité naturelle), qui sied à la philosophie de Spinoza
  • Le lexique des prédicats unaires, binaires et ternaires correspondant aux concepts spinozistes
  • Les axiomes modaux fondamentaux
  • Les définitions de Spinoza (causa sui, substance, attribut, mode, Dieu, etc.)
  • Les axiomes proposés par Spinoza et complétés par Jarrett
  • Les démonstrations formelles des 36 propositions du Livre I (excepté la P33 et la P36 qui sont indérivable du système)

Prérequis

Pour exécuter ce projet, vous aurez besoin de :

  1. Coq (version 8.13 ou supérieure recommandée)
  2. Un IDE compatible avec Coq comme CoqIDE ou Proof General pour Emacs

Installation

  1. Installez Coq en suivant les instructions sur le site officiel
  2. Clonez ce dépôt : 
    git clone https://github.com/l-pommeret/Projet-Spinoza.git
cd Projet-Spinoza

Exécution

Avec CoqIDE

  1. Ouvrez CoqIDE
  2. Ouvrez le fichier De_Deo.v
  3. Utilisez le bouton “Step forward” ou la combinaison de touches Ctrl+Right pour avancer pas à pas dans la preuve

Avec Proof General (Emacs)

  1. Ouvrez Emacs
  2. Ouvrez le fichier De_Deo.v
  3. Utilisez C-c C-n pour avancer d’une étape dans la preuve ou C-c C-Enter pour avancer jusqu’au curseur

En ligne de commande

Pour compiler le projet sans interface graphique :

coqc De_Deo.v

Remerciements

  • Charles Jarrett pour sa formalisation logique de l’Éthique
  • L’équipe de développement de Coq pour cet assistant de preuve
  • Claude 3.5, le LLM qui m’a beaucoup aidé à réaliser ce projet, parfois étonnamment fort en démonstrations.