rafpaf / prove-ethics

Checking Spinoza's demonstrations

The goal of this quixotic project is to reconstruct the demonstrations in Spinoza's Ethics (1677) so as to find new pieces of internal evidence that bear on interpretation and help me better understand the arguments.

The "steps" directory contains my attempts to translate various propositions into a version of first-order logic called "Prover9" (http://www.cs.unm.edu/~mccune/prover9/). A more expressively powerful logic is clearly needed, so this is just a start.

Try running "qed". When it stalls, press Ctrl-C to continue.

You can see a short tour of the code at https://youtu.be/2tVx4vjRWyo.

Maybe with your help we can write "the true codes, according to which all singular things come to be, and are ordered..." (Treatise on the Emendation of the Intellect)... :-)

Reminders

• Don't forget periods at the end of formulae.
• Use -(exists a ( ... )), not -exists a ( ... )

The demonstrations file

Start a line with '#' to omit it, '+' if it's supposed to be valid, and '-' if it's supposed to be invalid. (The last option is good for testing to see whether the conclusion follows just from the vocabulary file misc or from a subset of the premises, which might show that you've coded a proof incorrectly or that Spinoza was more circuitous than he needed to be.)