Visual Information and Valid Reasoning

Psychologists have long been interested in the relationship between visualization and the mechanisms of human reasoning. Mathematicians have been aware of the value of diagrams and other visual tools both for teaching and as heuristics for mathematical discovery. As the chapters in this volume show, such tools are gaining even greater value, thanks in large part to the graphical potential of modern computers. But despite the obvious importance of visual images in human cognitive activities, visual representation remains a second-class citizen in both the theory and practice of mathematics. In particular, we are all taught to look askance at proofs that make crucial use of diagrams, graphs, or other nonlinguistic forms of representation, and we pass on this disdain to our students. In this chapter, we claim that visual forms of representation can be important, not just as heuristic and pedagogic tools, but as legitimate elements of mathematical proofs. As logicians, we recognize that this is a heretical claim, running counter to centuries of logical and mathematical tradition. This tradition finds its roots in the use of diagrams in geometry. The modern attitude is that diagrams are at best a heuristic in aid of finding a real, formal proof of a theorem of geometry, and at worst a breeding ground for fallacious inferences. For example, in a recent article, the logician Neil Tennant endorses this standard view: . . . [The diagram] is only an heuristic to prompt certain trains of inference; . . . it is dispensable as a proof-theoretic device; indeed, . . . it has no proper place in the proof as such. For the proof is a syntactic object consisting only of sentences arranged in a finite and inspectable array (Tennant [1984]). . . . It is this dogma that we want to challenge. We are by no means the first to question, directly or indirectly, the logocentricity of mathematics arid logic. The mathematicians Euler and Venn are well known for their development of diagrammatic tools for solving mathematical problems, and the logician C. S. Peirce developed an extensive diagrammatic calculus, which he intended as a general reasoning tool.

Towards a Model Theory of Venn Diagrams

One of the goals of logical analysis is to construct mathematical models of various practices of deductive inference. Traditionally, this is done by means of giving semantics and rules of inference for carefully specified formal languages. While this has proved to be an extremely fruitful line of analysis, some facets of actual inference are not accurately modeled by these techniques. The example we have in mind concerns the diversity of types of external representations employed in actual deductive reasoning. Besides language, these include diagrams, charts, tables, graphs, and so on. When the semantic content of such non-linguistic representations is made clear, they can be used in perfectly rigorous proofs. A simple example of this is the use of Venn diagrams in deductive reasoning. If used correctly, valid inferences can be made with these diagrams, and if used incorrectly, they can be the source of invalid inferences; there are standards for their correct use. To analyze such standards, one might construct a formal system of Venn diagrams where the syntax, rules of inference, and notion of logical consequence have all been made precise and explicit, as is done in the case of first-order logic. In this chapter, we will study such a system of Venn diagrams, a variation of Shin’s system VENN formulated and studied in Shin [1991] and Shin [1991a] (see Chapter IV of this book). Shin proves a soundness theorem and a finite completeness theorem (if ∆ is a finite set of diagrams, D is a diagram, and D is a logical consequence of ∆ , then D is provable from ∆ ). We extend Shin’s completeness theorem to the general case: if ∆ is any set of diagrams, D is a, diagram, and D is a logical consequence of ∆. then D is provable from ∆. We hope that the fairly simple diagrammatic system discussed here will help motivate closer study of the use of more complicated diagrams in actual inference.

Situation-Theoretic Account of Valid Reasoning with Venn Diagrams

Venn diagrams are widely used to solve problems in set theory and to test the validity of syllogisms in logic. Since elementary school we have been taught how to draw Venn diagrams for a problem, how to manipulate them, how to interpret the resulting diagrams, and so on. However, it is a fact that Venn diagrams are not considered valid proofs, but heuristic tools for finding valid formal proofs. This is just a reflection of a general prejudice against visualization which resides in the mathematical tradition. With this bias for linguistic representation systems, little attempt has been made to analyze any nonlinguistic representation system despite the fact that many forms of visualization are used to help our reasoning. The purpose of this chapter is to give a semantic analysis for a visual representation system—the Venn diagram representation system. We were mainly motivated to undertake this project by the discussion of multiple forms of representation presented in Chapter I More specifically, we will clarify the following passage in that chapter, by presenting Venn diagrams as a formal system of representations equipped with its own syntax and semantics:. . . As the preceding demonstration illustrated, Venn diagrams provide us with a formalism that consists of a standardized system of representations, together with rules of manipulating them. . . . We think it should be possible to give an informationtheoretic analysis of this system, . . . . In the following, the formal system of Venn diagrams is named VENN. The analysis of VENN will lead to interesting issues which have their ana logues in other deductive systems. An interesting point is that VENN, whose primitive objects are diagrammatic, not linguistic, casts these issues in a different light from linguistic representation systems. Accordingly, this VENN system helps us to realize what we take for granted in other more familiar deductive systems. Through comparison with symbolic logic, we hope the presentation of VENN contributes some support to the idea that valid reasoning should be thought of in terms of manipulation of information, not just in terms of manipulation of linguistic symbols.

Heterogeneous Logic

A major concern to the founders of modern logic—Frege, Peirce, Russell, and Hilbert—was to give an account of the logical structure of valid reasoning. Taking valid reasoning in mathematics as paradigmatic, these pioneers led the way in developing the accounts of logic which we teach today and that underwrite the work in model theory, proof theory, and definability theory. The resulting notions of proof, model, formal system, soundness, and completeness are things that no one claiming familiarity with logic can fail to understand, and they have also played an enormous role in the revolution known as computer science. The success of this model of inference led to an explosion of results and applications. But it also led most logicians—and those computer scientists most influenced by the logic tradition—to neglect forms of reasoning that did not fit well within this model. We are thinking, of course, of reasoning that uses devices like diagrams, graphs, charts, frames, nets, maps, and pictures. The attitude of the traditional logician to these forms of representation is evident in the quotation of Neil Tennant in Chapter I, which expresses the standard view of the role of diagrams in geometrical proofs. One aim of our work, as explained there, is to demonstrate that this dogma is misguided. We believe that many of the problems people have putting their knowledge of logic to work, whether in machines or in their own lives, stems from the logocentricity that has pervaded its study for the past hundred years. Recently, some researchers outside the logic tradition have explored uses of diagrams in knowledge representation and automated reasoning, finding inspiration in the work of Euler, Venn, and especially C. S. Peirce. This volume is a testament to this resurgence of interest in nonlinguistic representations in reasoning. While we applaud this resurgence, the aim of this chapter is to strike a cautionary note or two. Enchanted by the potential of nonlinguistic representations, it is all too easy to overreact and so to repeat the errors of the past.

Peircean Graphs for Prepositional Logic

The contributions of C.S. Peirce to the early history of prepositional and predicate logic are well known. Much less well known, however, is Peirce’s subsequent work (for more than ten years) on diagrammatic versions of prepositional and predicate logic. This work was considered by Peirce himself to be his most important contribution to logic. From his experience with chemistry and other parts of science, Peirce had become convinced that logic needed a more visually perspicuous notation, a notation that displayed the compound structure of propositions the way chemical diagrams displayed the compound structure of molecules. Peirce’s graphs for prepositional sentences are built up from sentence letters by the operations of enclosing a graph within a closed figure (interpreted as its negation) and juxtaposing two or more graphs on separate parts of the page (interpreted as their conjunction). For example, a graph like would be interpreted as “If A and B, then C” or “It is false that A and B and not-CV’ A graph such as would be read as “If A then B, but not C.” This chapter gives a modern analysis of Peirce’s diagrammatic version of the propositional calculus from the ground up. In particular, it is an investigation of just what is involved in formulating precisely the syntax, semantics, and proof theory of Peirce’s graphical approach to propositional logic. The project is interesting for several reasons. First, given Peirce’s importance in the history of .logic and his own opinion of the value of his work on graphs, it seems of historical interest to see to what his suggestions amounted. Second, Peirce’s work has gained a following in the computer science community, due especially to the work of Sowa [1984], whose system of conceptual graphs is modeled after Peirce’s work on diagrammatic approaches to prepositional and predicate logic. Third, in reconstructing Peirce’s graphical system we will confront a number of features characteristic of “visual” or “diagrammatic” inference, that is, inference that employs various forms of graphical representations in addition to, or in place of, sentences.

Diagrams and the Concept of Logical System

In attempting to analyze the notion of a logical system, there are various approaches that could be taken. One would be to look at the things people have called logical systems and try to develop a natural framework which would encompass most or many of these, and then explore the consequences of the framework, seeing what else falls under the framework and what the consequences of the general notion happen to be. This was basically the approach taken, for example, in Barwise [1974], one of the early attempts to develop such a framework. This approach has much to recommend it, but it also has at least two serious drawbacks. It is too dependent on accidents of history, that is, on what particular systems of logic people happened to have developed. There is at least the theoretical possibility that biases of precedent and fashion have played a significant role in the way things have gone. If so, the abstraction away from practice has the danger of codifying these historicallycontingent biases, making them appear like necessary features of a logical system. The flip side of this problem is that there may well be some unnatural logical systems which contort the framework. But how else could one proceed in an attempt to get a principled notion of logical system? Another approach, the one we take here, is to look at the existing logical systems that people happened to have developed and to try to see what they were up to in more general terms. Our hope is to find some interesting natural phenomenon lurking behind these systems, a “natural kind,” if you will. If there is such a natural phenomenon, it could be used to guide the formulation of an abstract notion of logical system. If a characterization of logical systems could be found using this approach, it would have potentially two significant advantages over the more orthodox approach. First, it would provide a basis from which one could give a principled critique of existing systems claimed to be logical systems. Second, though, it would point out gaps, that is, logical systems which have yet to be developed.

Exploiting the Potential of Diagrams in Guiding Hardware Reasoning

. . .Formal methods offer much more to computer science than just “proofs of correctness” for programs and digital circuits. Many of the problems in software and hardware design are due to imprecision, ambiguity, incompleteness, misunderstanding, and just plain mistakes in the statement of top-level requirements, in the description of intermediate designs, or in the specification of components and interfaces. Rushby [1993] . . .Desire for correctness proofs of systems spawned the research area known as “formal methods”. Today’s systems are of sufficient complexity that testing is infeasible, both computationally and financially. As an alternative, formal methods promote mathematical analysis of a system as a means of locating inconsistencies and other design errors. Techniques used can range from writing system descriptions in a formal notation to verification that the designed system satisfies a particular behavioral specification. A good general introduction to formal methods appears in Rushby [1993]. Ideally, using formal methods increases our assurance in and understanding of our designs. Assurance results from proof, while understanding results from the process of producing the proof. Successful use of formal methods therefore requires powerful proof techniques and clear logical notations. The verification research community has paid considerable attention to the former. Current techniques, many of which can be fully automated, handle sufficiently complex systems that formal methods are now being adopted (albeit slowly) in industry. In our drive to provide powerful proof methods, however, we have overlooked the latter requirement. Research has focused on proof without paying sufficient attention to reasoning. Current tools are often criticized as too hard to use, despite their computational power. Most designers, not having been trained as logicians, find the methodologies and notations very unnatural. Industrial sites, starting out with formal methods, must often rely on external verification professionals to help them use these tools effectively (NASA [1995]). Tools that are not supportive of reasoning therefore fail to provide the full benefits of formal methods. We can augment our current methodologies to address this problem, but we first need to understand reasoning and its role in hardware design.

Toward The Rigorous Use Of Diagrams In Reasoning About Hardware

The logician’s conventional notion of proof has grown increasingly anachronistic through the twentieth century as computing capabilities have advanced. classical proof theory provides a partial model of actual mathematical reasoning. when we move away from mathematics toward reasoning in engineering and computation, its limitations are even more pronounced. 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. contrary to formalists’ dogma, experience suggests that pictures, diagrams, charts, and graphs are important tools in human reasoning, not mere illustrations as traditional logic would have us believe. nor is the computer merely an optimized turing machine. the computer’s graphical capabilities have advanced to the point that diagrams can be manipulated in sophisticated ways, and it is time to exploit this capability in the analysis of reasoning, and in the design of new reasoning aids. in this chapter, we propose a new understanding of the role of various sorts of diagrams in the specification and design of computational hardware. this proposal stems from a larger project, initiated by barwise and etchemendy [1991a], the goals of which are to develop a mathematical basis from which to understand the substantive logical relationships between diagrams and sentences, and to develop a new generation of automated reasoning tools from that basis. microelectronic cad systems are among the supreme examples of visualized reasoning environments. their tools are highly oriented toward diagrams, are quite sophisticated, and are comparatively well integrated. these systems also integrate logical and physical design, providing a strong coherence between specification and implementation views. formalized reasoning meshes poorly with these working frameworks. although it provides needed rigor for today’s highly complex design challenges, its preoccupation with formulas at the expense of diagrams is simply too cumbersome. we should attempt to draw lessons from these advanced design environments, making the reasoning rigorous without subverting their character. this chapter is built around a simple design example, a synchronizing circuit. our purposes are, first, to illustrate heterogeneous use of pictoral “formalisms” in design, and second, to expose basic questions for the logical analysis that follows. we will develop a mathematical basis in which the example can be analyzed. these are admittedly modest beginnings, but we hope that they start to put to rest the idea that only formulas can be used in formal reasoning about hardware.

A Diagrammatic Subsystem of Hilbert's Geometry

In the last few years there has been an increasing interest in the visual representation of mathematical concepts. The fact that computers can help us perform graphical tasks very easily has been translated into an increasing interest in diagrammatic representations in general. Several experiments have shown that diagrammatic reasoning plays a main role in the way in which experts in several areas solve problems (Gobert and Freferiksen [1992] and Kindfield [1992]). Two kinds of explanations have been given for the advantages of visual representations over linguistic ones. The first kind of explanation is psychological. It has been argued that visual representations are easier to use because they resemble the mental models hurnans build to solve problems Stenning and Oberlander [1991], Johnson-Laird and Byrne [1991], arid Tverski [1991]. The second kind of explanation is related to computational efficiency. Larkin and Simon [1987] have argued that diagrammatic representations are computationally more efficient than sentential representations because the location of each element in the diagram corresponds to the spatial or topological properties of the objects they represent. However, the efficiency of the use of diagrams is not enough justification for their use in analytical areas of knowledge. Mathematical discoveries often have been made using visual reasoning, but those very same discoveries were not justified by the visual reasoning. Diagrams are associated with intuitions and illustrations, not with rigorous proofs. Visual representations are allowed in the context of discovery, not in the context of justification. Many authors have considered diagrams in opposition to deductive systems. Lindsay [1988], for instance, has claimed that the main feature of visual representations is that they correspond to a non-deductive kind of inference system. Koedinger and Anderson [1991] have related diagrammatic reasoning in geometry to informal, inductive strategies to solve problems. Thus, though we have an empirical justification for the use of diagrams in mathematics (people use them and they work!) we do not usually have an analytical justification. In fact, the history of mathematics, and especially the history of geometry, is full of mistakes related to the use of diagrams.

Operational Constraints in Diagrammatic Reasoning

Diagrammatic reasoning is reasoning whose task is partially taken over by operations on diagrams. It consists of two kinds of activities: (i) physical operations, such as drawing and erasing lines, curves, figures, patterns, symbols, through which diagrams come to encode new information (or discard old information), and (ii) extractions of information diagrams, such as interpreting Venn diagrams, statistical graphs, and geographical maps. Given particular tasks of reasoning, different types of diagrams show different degrees of suitedness. For example, Euler diagrams are superior in handling certain problems concerning inclusion and membership among classes and individuals, but they cannot be generally applied to such problems without special provisos. Diagrams make many proofs in geometry shorter and more intuitive, while they take certain precautions of the reasoner’s to be used validly. Tables with particular configurations are better suited than other tables to reason about the train schedule of a station. Different types of geographical maps support different tasks of reasoning about a single mountain area. Mathematicians experience that coming up with the “right” sorts of diagrams is more than half-way to the solution of most complicated problems. Perhaps many of these phenomena are explained with reference to aspect (ii) of diagrammatic reasoning because some types of diagrams lets a reasoner retrieve a kind of information that others do not. or lets the reasoner retrieve it more “easily” than others. In fact, this is the approach that psychologists have traditionally taken. In this chapter, we take a different path and focus on aspect (i) of diagrammatic reasoning. Namely, we look closely at the process in which a reasoner applies operations to diagrams and in which diagrams come to encode new information through these operations. It seems that this process is different in some crucial points from one type of diagrams to another, and that these differences partially explain why some types of diagrams are better suited than others to particular tasks of reasoning.