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.