|By Witold Marciszewski & Roman Murawski
Amsterdam-Atlanta, GA: Rodopi, 1995
Throughout the whole history of logic since Plato, logic was meant as a device (organon) to assist human cognitive endeavors, and a remedy to cure deficiencies of human minds (“medicina mentis”, as called by some Cartesians). This was Descartes’ and Leibniz’s ultimate goal, but Leibniz envisaged the route which led through an intermediate stage (decidedly rejected by Descartes), viz. the stage of mechanized reasoning as a thread to guide our thoughts (“filum cogitationis”). In that perspective which is put by our present stage of civilization, the attainment of that auxiliary facility has proved the greatest success of logic, in spite of its failing (so far) to reach the intended final result. The same perspective affects our views on what has proved most important in the development of logic before Leibniz and after him.
There are two preparatory steps necessary for mechanization of reasoning with the help of computers, viz. its formalization and algebraization. The former was initiated in the Middle Ages (appreciated and continued by Leibniz), the latter was done in the English algebra of logic in the 19th century.
In the book, therefore, the chapter on the 17th century is preceded by one concerned with the Middle Ages. That chapter praises the nominalistic trend in logic (as looking for an algorithmic method of finding the middle term for a syllogism), and dispels the legend of Ramon Lullus, unduly regarded as an author of the idea of mechanized reasoning. The chapter on the 18th century does not pretend to show all the attempts at algebraizing logic as made in that period. However, it reveals that the ignorance of Leibniz’s algebraic approach to logic (not removed until Couturat’s archival discoveries) did not prevent later authors to develop this approach independently — up to the historical success of Boole and his colleagues. Their story is told in an extensive chapter dealing with Boole, De Morgan, Jevons, and Venn.
Boole’s algebra was but a tool which required inventive skillful masters to take the final advantages. The story narrated in the subsequent chapter, “The 20th century way to formalization and mechanization”, deals with the use of algebra made to create propositional logic, with the parallel process of its formalization, and with the methods of “reducing” formalized predicate logic to the algebraic form — the methods due to Skolem, Hilbert, Herbrand, Gentzen, Beth, etc.
Due to those achievements, the time became ripe to devise procedures for automated theorem-proving as well as computer-assisted proof verification. This is the subject for the chapter to happily end the volume. Under the title “Mechanized deduction systems”, the last chapter discusses the unification and resolution methods, and related topics.
The authors hope to enjoy comments from benevolently critical Readers. For the purposes of the discussion hoped for, here are the authors’ addresses:
Department of Logic, Methodology and Philosophy of Science
Warsaw University in Bialystok
ul. Liniarskiego 4
15-420 Bialystok, Poland
Department of Mathematical Logic
Faculty of Mathematics and Computer Science
ul. Matejki 48/49
60-769 Poznan, Poland