1. Why were you initially drawn to formal methods?
My undergraduate education was at an engineering college, where I was a mathematics major. While there I took some philosophy courses, and one of them was on symbolic logic. It was very tedious and detailed, but near the end of it there was a brief presentation of modal logic, done in the historic style of C. I. Lewis. It was at this point that I realized I liked manipulating the symbols. This sounds a bit facile, but I think something deeper was going on. My calculus courses, for instance, were vast in scope, involving the nature of the real number system, limits, sequences, differential equations, applications to physics, to three dimensional geometry, and so on. Such an array of concepts historically took hundreds of years to develop and sort out. And at that point in my education, calculus applications necessarily involved the intuitive use of fuzzily understood techniques. It was all impressively powerful, yet disquieting in its mixture of vagueness and proved certainty. Modal logic was something quite different. Its scope was narrow and precisely delineated. Within that scope the rules were sharp and clear. The problem it set out to address, the distinction between necessary truth and truth, was of significant philosophical interest and much might be said about it, but the Lewis approach involved little discussion. More or less, it just said: here are formal statements involving necessity; you might argue which are correct, but if you accept these, you are committed to these others. This provided a sharp analysis that, while not solving the problem, made important aspects of the problem unmistakably clear in a way that endless discussion would not. I think this is what I mean by saying I liked manipulating the symbols.
I think that when formal methods have been most successful they have dealt with small, compact, and isolatable problems. Bertrand Russell’s “On Denoting” is a good example. One might describe it as an examination of the logic of the word “the.” (It’s rather broader than this, but what I wrote is near enough for this discussion.) The “the” problem is complex enough to be of interest to generation after generation, yet sharp enough to be addressed using a mathematically precise methodology whose outlines are intuitively clear to us. By contrast, Montague’s formal semantics of natural language is not widely popular despite its genuine successes—its scope is too broad for that. A formalization of natural language may be needed someday if we are to talk with computers, but in its entirety it would be rather overwhelming and under-enlightening. There is a nice illustration of this point by Lewis Carroll, in his relatively unknown book Sylvie and Bruno, from which I quote.
“That’s another thing we’ve learned from your Nation,” said Mein Herr, “map-making. But we’ve carried it much further than you. What do you consider the largest map that would be really useful?”
“About six inches to the mile.”
“Only six inches!” exclaimed Mein Herr. “We very soon got to six yards to the mile. Then we tried a hundred yards to the mile. And then came the grandest idea of all! We actually made a map of the country, on the scale of a mile to the mile!”
“Have you used it much?” I enquired.
“It has never been spread out, yet,” said Mein Herr: “the farmers objected; they said it would cover the whole country, and shut out the sunlight! So we now use the country itself, as its own map, and I assure you it does nearly as well.”
At the heart of formal methods are formal metaphors.
Even when successful, formal methods do not end discussion. There remains the issue of how well a particular formal method captures the essential features of a problem. Eubulides of Miletus prompted centuries of discussion with his liar paradox, and not surprisingly solutions have been given using formal methods. But there are several solutions, and they are largely incompatible. Following Tarski, one might conclude that natural language is not formal in the technical sense, because it contains its own truth predicate and formal languages cannot do this. Following Kripke, not all sentences of natural language involving the truth predicate have truth values. Following the fuzzy logicians, perhaps the liar sentence is a bit true and a bit not. Following the paraconsistent logicians, perhaps the liar sentence is both true and false, and so what? In each case the formal methods are meticuously developed. The conclusions vary because the premises vary. Formal methods make it clear what we get with the purchase of a philosophical position; they cannot of themselves tell us which position to buy.
Applications of formal methods that are considered successful have a common feature that, perhaps, we might not like to admit: they make us believe we understand the problem being addressed better than we did before. This is not an essential characteristic of formal methods—basically they just say “you are committed to this if you accept these principles.” Belief that our understanding has been improved is a different thing. For example, modal logics have both algebraic and relational (possible world, Kripke) semantics. Algebraic semantics is older, and provides suitable mathematical machinery for proving things about modal logics, yet the introduction of relational semantics revolutionized the subject. Why? Because people believed that relational semantics provided insights into the way modal operators “really” worked—possible worlds were more than a metaphor, instead they formalized what we were actually doing on some level. It’s hard for Boolean algebras with operators to compete with that. An analogous treatment of relevance logic, using a ternary relation, did not have anything like the same impact, probably because people did not feel it enlightened, and not because of its lack of mathematical utility. It is a matter of aesthetics, but something more is involved. Some things just resonate more than others. Still it’s probably worth asking, from time to time, whether the enlightenment provided by some particular formal methodology is real or spurious. One should not ask such a question too soon, of course. One should enjoy the heady days, the rush, the excitement. But when the tumult and shouting has died, it’s appropriate for nagging doubts to surface. All applications of formal methods have a philosophical story at their heart—they are philosophical metaphors, and that should not be forgotten.