Science-Philosophical Issues:
Import of Mechanized Deduction for Philosophy of Science
The very idea of mechanized (automated) deduction influenced philosophy
of science before it could have been accomplished with computers. For
instance, the Leibnizian "Calculemus" was meant as a paradigm for every
science, while Turing's (as well as those of G&#del;del, Church etc) results
revealed surprising limitations of Leibniz's programme (as later precised by
Hilbert).
Although in another way, the idea of unity of science, as cherished by
the Vienna Circle and akin trends, appealed to the same hope for progress to
come with strictly formalized deduction (and formalization is potential
automation, which materializes when required physical devices become
available).
It was not until the thirties in this century that people started
to see how utopian that paradigm was. However, this does not put aside the
question of how much of that paradigm can be saved in spite of the
discovered limitations. To attack this problem is a task for this
Section.
Another problem is how the use of automated deduction in mathematics
changes its very nature and makes it more similar to experimental science.
There is an inspiring literature on this subject which should be critically
examined to gain a perspective on an expected evolution of science and
appropriate policies in the knowledge organization and management.
LogBank Main Menu