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.
