Journal of Logic, Language and Information 8: 387–390, 1999.
387
Book Review
Logical Reasoning with Diagrams, Gerard Allwein and Jon Barwise, eds., Studies in Logic and Computation, Oxford University Press, New York, 1996. Price: $55.00/£36.00, xvi + 270 pages, ISBN: 0-19-510427-7. In early 1986, as an undergraduate student, I had my first encounter with a Macintosh computer. I was overwhelmed, to put it mildly. This was the future. This was the 20th century way to organize and manipulate information. Forget about command-line interfaces or Hilbert-style proof systems. Now, well over a decade later, the Macintosh interface has been copied widely, the internet has taken off in a big way due to the availability of graphical interfaces and fast network connections, and visual programming and development tools abound. Scientifically, the visual revolution has led to novel research initiatives in logic and computing. The book under review documents some of the work carried out as part of one of the most significant of these initiatives: the Visual Inference Laboratory at Indiana University. This laboratory is a multi-disciplinary institute devoted to the study of the logical and cognitive properties of diagrams in reasoning, and to the development of computational tools to facilitate such reasoning. Most of the chapters in the book were written by members or former members of the laboratory. The book’s editors hope that its appearance will encourage scientists and mathematicians to be more up front about the use of diagrams in their own reasoning, teachers of logic to use them in their teaching, and future logicians to contribute to the development of the logic of diagrams. The book is divided into three parts: Theoretical Issues, Case Studies, and Heterogeneous Systems. Here is a chapter-by-chapter breakdown of the individual chapters. Part A, on Theoretical Issues, opens with a reprint of Barwise and Etchemendy’s classic paper (1991) on visual information and valid reasoning. This paper is still a pleasure to read, and an excellent choice for an opening chapter. In it the authors argue that visual forms of representation can be important, not just as heuristic and pedagogic tools, but as legitimate elements of mathematical proofs. A number of examples to this effect are given, and the authors also discuss the Hyperproof computer program for teaching basic reasoning skills to students in a way that makes crucial use of visualization of information. In the final section of this chapter the authors discuss why it is that visual representation can be so useful for mathematical discovery, proof and pedagogy. The second chapter of the book, by Shimojima, deals with the process in which a reasoner applies operations to diagrams and in which diagrams come to encode new information through these operations. Briefly, the hypothesis advocated by the author is that there exists a set of operational constraints that govern the process in which a reasoner constructs diagrams. The notions of free ride and overdetermined alternatives are introduced to help explain the way in which such constraints intervene in the process of reasoning. The use of non-linear notations naturally raises the question whether the diagrammatic calculi we are working with can still be called logics. The main concern of the third chapter, co-authored by Barwise and Hammer, is to come up with a sufficiently general notion of logical system that will capture aspects common to traditional logics and diagrammatic calculi. The thesis underlying the chapter is that logical systems are meant to serve as mathematical models of informal inference
388
BOOK REVIEW
practices and pre-theoretic consequence relations behind these practices. Particular systems arise not only from the inference practice being modeled, but also from what idealizations are made about it. The authors argue that the diversity of logical systems arising from taking both of these variables into consideration is not handled well by means of standard accounts of what constitutes a logical system. Part B of the book is devoted to four case studies of specific diagrammatic systems. The first of these, Chapter 4, is a re-print of a 1991 paper by Shin. It gives a semantic analysis for the Venn diagrammatic representation system. A formal system is developed, together with a syntax and (situationtheoretic) semantics, and traditional logical issues such as soundness and (finite) completeness are settled. In Chapter 5, by Hammer and Danner, Shin’s finite completeness result for Venn diagrams is extended to the general case: if 1 is any set of diagrams, D is a diagram, and D is a logical consequence of 1, then D is provable from 1. The authors achieve the added generality by moving away from Shin’s situation-theoretic semantics, and using a more traditional set-based semantics instead. As is well known, C.S. Peirce was one of the first logicians to recognize and stress the importance of a visually perspicuous notation. Peirce’s work has gained a strong following in the knowledge representation community, due especially to the work of John Sowa. In Chapter 6, Hammer gives a modern analysis of Peirce’s diagrammatic version of propositional logic. He addresses a number of logical features of Peirce’s alpha system, including strong completeness. The proof of the latter result follows a pattern that is well known from completeness results in standard logics. The starting point for Chapter 7 is the observation that despite the fact that there is a clear empirical justification for the use of diagrams in mathematics, we do not usually have an analytical justification. Luengo argues that the problem is not with diagrams, but with having bad semantics and syntax. To support this claim, the author takes a small fragment of Euclidean geometry and shows that a diagrammatic system with a clear syntax and semantics can be built for it, thus making fallacies less likely. The main formal results are a soundness and an incompleteness result. Part C of the book consists of three chapters, each focussing on heterogeneous systems. In the first of these – “Heterogeneous Logic” by Barwise and Etchemendy – the authors argue against the idea of a universal diagrammatic system, and against the idea that systems with multiple forms of representation need some underlying “interlingua” to tie the representations together. More positively, it is shown how to get a rigorous justification without any such interlingua for some of the rules of the (heterogeneous) Hyperproof computer program for teaching elementary logic courses. The main lessons learned from Hyperproof can be summarized as follows. First, finding the best representation of a problem domain is usually the most important step in problem solving, and diagrams come into play here because they are efficient representational schemes. Second, heterogeneous systems such as Hyperproof are able to integrate the strengths of different types into a complete system. And finally, Hyperproof shows the need for a “hyperstructure” where proofs are given using a mixture of various formalisms and representations. One of my favorite chapters of the book, Chapter 9, takes the above lessons from Hyperproof as its starting point, and describes the Circuitproof pilot study. One of the aims of this project is to develop a suit of integrated reasoning tools which are useful in circuit-design applications. The heterogeneous environment proposed by the authors (Johnson, Barwise and Allwein) contains finite state diagrams, circuit schematics, timing diagrams, and second-order logic. Plenty of important research issues are being raised in this chapter, ranging from useability issues to purely logical concerns, but the main ideological message is that we should “put to rest the idea that only formulas can be used in formal reasoning about hardware” (p. 202). The theme of developing heterogeneous hardware logics is taken up again in the tenth and final chapter of the book. As with the logic developed in Chapter 9, this chapter’s logic mixes diagrams, machines and second-order logic. The bulk of the chapter is devoted to a rigorous definition of the logic, but by far the most interesting section of the chapter is the one where the flexibility of the logic
BOOK REVIEW
389
is demonstrated on an example, the island traffic light controller. Although additional work is needed before a tool based upon the logic can be constructed – e.g., there is no support for abstraction – the approach seems very promising, especially because of its highly modular nature. At the end of the day, what is the main achievement of the book? Clearly, many interesting and important lines of research in the general area of reasoning with diagrams are being pursued throughout the book. But does the goal of encouraging logicians to “contribute to the development of the logic of diagrams” which it has set itself on page viii? I think it does, but I also think that it could have done a better job. A little more editorial work – both contentwise and at the level of copy-editing? – could have turned this valuable book into an even more valuable book. The third part of the book nicely illustrates what I mean. Its chapters are well structured and have clear messages – if not mission statements – on where reasoning with diagrams should go, and the issues they address are attractive and novel mixtures of traditional logical concerns (such as expressive power) in a novel setting and of themes peculiar to heterogeneous systems (such as efficacy). Unfortunately, the first two parts of the book do not really reach this level of presentation. Moreover, the book lacks a proper editorial introduction, and the chapters in Part B all treat fairly traditional logical issues, with only a fairly superficial diagrammatic flavor. Despite these misgivings, I think the book is an excellent buy and a must-have for anyone who is interested in formal aspects of reasoning with diagrams. Let me conclude with a quote from Chapter 9, by Johnson, Barwise and Allwein. It is a statement that neatly sums up the view of standard, text-based proof systems that I have held ever since I first sat down behind a Mac: “The standard idea of a formal system seems frozen in the information technology of Frege’s time; it is decidedly quaint in the presence of today’s desk-top computer.” I could not agree more, and I think that the book contains many inspiring examples of alternative modern formal systems.
Reference Barwise, J. and Etchemendy, J., 1991, “Visual information and valid reasoning,” pp. 9–24 in W. Zimmerman and S. Cunningham, eds., Visualization in Teaching and Learning Mathematics, Washington: MAA. Maarten de Rijke ILLC University of Amsterdam Plantage Muidergracht 24 1018 TV Amsterdam The Netherlands E-mail:
[email protected]
? E.g., there is a spurious page break on page 193, lots of chapters lack a proper conclusion, and
the bibliography would have benefited from a clean-up.