View the project on GitHub

Baruch Spinoza

Baruch Spinoza (1632-1677)

Charles Jarrett

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

This project is a formalization in Coq of the propositions from Book I of Spinoza’s Ethics, according to the logical formalization proposed by Charles Jarrett in his article “The Logical Structure of Spinoza’s Ethics, Part I” (1978).

The PDF for the proofs in Coq!

Caveat

These demonstrations are based on a philosophical interpretation (since it’s a formalization) of the Ethics, and are therefore a shared responsibility of Spinoza and Charles Jarrett.

Project Content

The main file De_Deo.v contains:

  • Formal definitions of modal operators (logical necessity, possibility, natural necessity), which suit Spinoza’s philosophy
  • The lexicon of unary, binary and ternary predicates corresponding to Spinozist concepts
  • The fundamental modal axioms
  • Spinoza’s definitions (causa sui, substance, attribute, mode, God, etc.)
  • The axioms proposed by Spinoza and completed by Jarrett
  • The formal demonstrations of the 36 propositions of Book I (except P33 and P36 which are underivable from the system)

Requirements

To run this project, you will need:

  1. Coq (version 8.13 or higher recommended)
  2. A Coq-compatible IDE such as CoqIDE or Proof General for Emacs

Installation

  1. Install Coq by following the instructions on the official website
  2. Clone this repository: 
    git clone https://github.com/l-pommeret/Projet-Spinoza.git
cd Projet-Spinoza

Execution

With CoqIDE

  1. Open CoqIDE
  2. Open the file De_Deo.v
  3. Use the “Step forward” button or the Ctrl+Right key combination to advance step by step in the proof

With Proof General (Emacs)

  1. Open Emacs
  2. Open the file De_Deo.v
  3. Use C-c C-n to advance one step in the proof or C-c C-Enter to advance to the cursor

Command Line

To compile the project without a graphical interface:

coqc De_Deo.v

Acknowledgements

  • Charles Jarrett for his logical formalization of the Ethics
  • The Coq development team for this proof assistant
  • Claude 3.5, the LLM that helped me a lot with this project, sometimes surprisingly strong in demonstrations.