Application of automated theorem-proving to philosophical thought: Spinoza’s Ethics

Abstract

We have applied the automatic theorem-prover Prover9 to prove first eleven theorems of Part 1 of Benedict de Spinoza’s Ethics. We have used a previous formalization of that segment developed by Blum and Malinovich. We have found Prover9 to be very efficient, providing proofs in tens of miliseconds. It appears that the only, but fundamental, limitation for testing philosophical reasoning is related to the difficulty of unique formalization.