Spinoza in Coq

A.s. donderdag zal er in Besançon een seminar worden gehouden over 'Spinoza in Coq’: een volledig uitgewerkte bewijsvoering van de eerste stellingen van de Ethica. [Cf.]

Er zitten lacunes in de geometrische bewijsvoering die Spinoza in de Ethica aanreikt. Vaak is door bestrijders gewezen op onjuistheden in die bewijsvoering. De historicus van de filosofie Martial Gueroult trachtte in de eerste 1970-iger jaren door zorgvuldige lezing Spinoza’s bewijsvoering a.h.w. ‘met de hand en uit het geheugen’ te vervolledigen. Een helse klus. Tegenwoordig zou zulk werk preciezer uitgevoerd kunnen worden met het computerprogramma Coq.

In computer science, Coq is an interactive theorem prover. It allows the expression of mathematical assertions, mechanically checks proofs of these assertions, helps to find formal proofs, and extracts a certified program from the constructive proof of its formal specification. Coq works within the theory of the calculus of inductive constructions, a derivative of the calculus of constructions. Coq is not an automated theorem prover but includes automatic theorem proving tactics and various decision procedures. [en.wikipedia]

Baptiste Mélès, research fellow bij CNRS, verbonden aan het Laboratoire d'Histoire des Sciences et de Philosophie Archives Henri-Poincaré te Nancy [cf.], zal de eerste resultaten van dit werk a.s. donderdag presenteren. Hij zou niet alleen enige minder belangrijke achterwege gelaten stapjes in de bewijsvoeringen laten zien, maar ook een aantal impliciete axioma's van Spinoza’s Ethica hebben bloot weten te leggen.

Een minpuntje vind ik dat de aankondiging vergezeld gaat van een flauwiteit: Spinoza is op zijn 'Wolfenbütteler-portret' voorzien van een hanenkam [cf.] - ha, ha, ha, le coq, ja...

____________________

NB. In de rechterkolom van dit blog is al geruime tijd de link te vinden naar de zgn. "SpinozaBase" van Baptiste Mélès.