UP

Philosophy and Formal Methods

This is a two way street.

Formal Methods for Philosophy

Principia Mathematica

The first large scale application of formal methods was the formalisation of Mathematics undertaken by Bertrand Russell and Alfred North Whitehead in Principia Mathematica. A fuller account of the Philosophical basis for this work is found in The Principles of Mathematics, though this precedes some of the necessary technical innovations. The publication of Principia Mathematica was the culmination of a period of revolutionary advance in Logic, which had for two millenia remained as systematised by Aristotle.

These advances in logic, though stimulated by the need to improve the rigour of mathematics, were seen to have fundamental philosophical consequences. They played a central role in the development of analytic philosophy during the twentieth century. While in the second half of this century the view that philosophy is intimately related to logic was supplanted by methods based on the analysis of ordinary language, and doctrines which rejected any other role for philosophy, we are now seeing a revival of interested in the kind of analytic philosophy which grew from the advances in formal techniques.

Two books of relevance here are:

both of which provide valuable philosophical background for anyone wishing to understand the scope and significance of formal methods in the broadest sense.

Philosophy for Formal Methods

Foundations

Some of the work in theoretical computer science which is motivated, at least in part, by providing suitable foundations for formal methods raises interesting philosophical issues.

Formal methods are generally thought of as essentially mathematical in nature. Mathematicians this century have, by and large, found it possible to do their work in the context of classical set theory without much concern for the fine details of how this system is formalised, or for whether this foundation can or should be improved.

In computer science, set theory has not achieved this kind of status. Where mathematical methods have been adopted without concern for foundations or for formality they are often conducted in a manner consistent with the classical set theoretic context. However, where theoreticians have taken an interest in foundations, they have often adopted and/or advocated radical alternatives to classical set theory. Constructive systems have often been adopted, and there is considerable interest in the use of category theory in a variety of ways, including as a basis for new foundations for computer science and for mathematics.

The stimulus provided by these tendencies in theoretical computing lends interest to philosophical studies which might contribute to objective evaluation of the technical alternatives available.

The Philosophy of Logic has a general relevance. See also logic and the foundations of mathematics.


UP HOME ©RBJ created 1995/4/13 modified 1997/6/16