To appear in Hystory and Philosophy of Logic

Jon Barwise and John Etchemendy, Hyperproof for the Macintosh. Stanford CA: CSLI Publications (CSLI Lecture Notes No. 42), 1994. xvii+255 pp., including a Macintosh disk. US $ 24.95.

Reviewed by

Simone Martini, Università di Udine Dipartimento di Matematica e Informatica, Via delle Scienze 206, I-33100 Udine, Italy.

‘Hyperproof is a system for teaching the basic principles of analytical reasoning’ (p. xiii). Seldom the incipit of a book has been so informative and truthful. First, Hyperproof is a system—a computer program (for Apple Macintosh) and a book—whose components would not be of much use separately. Second, Hyperproof has been developed for teaching. It talks to students, not to their instructors, taking them step by step through worked out examples and almost 300 exercises, trying to anticipate their questions and problems. Third, Hyperproof teaches the basics of analytical reasoning, through the language of formal (first order) logic, but without confining itself to just a formal system for provability. And this is its major novelty.

The Hyperproof project stems out of the work of the authors on the program Tarski’s World and its companion book The Language of First Order Logic (reviewed in issue …, pp. 146–47, of this journal). In Tarski’s World a simple world with blocks of several shapes and sizes is simulated, and the user is asked to check whether some formal statements are satisfied in a certain world, or to build a world satisfying certain statements. Its companion book is an introductory logic text, with a strong semantical flavor backed by the frequent reference to the program. The book introduces a Ficht-style formal system for provability, but formal proofs are not supported by the program. Hyperproof maintains and develops the semantical approach of its predecessor. Instead of complete worlds, it also allows partially specified situations (attributes of blocks—e.g size, or shape—may be left unspecified). The program presents the user with some initial information (the givens of the problem), in the form of a graphic representation of a situation and a list of formal sentences. It then asks the user to establish some goals, varying from consequence, to non-consequence, to inconsistency (chosen from 27 different types of possible goals). The user has to build a proof satisfying the goal, and the program will check both the correctness of the proof and the eventual satisfaction of the assigned goals.

The book is devoted to teaching the students how to develop such proofs. The general structure of a proof is a Ficht-style diagram, but Hyperproof ’s distinguishing trait is that pictorial information (i.e. a situation) may appear as a step. Consequently, there are proof-rules allowing to transfer information from pictorial to sentential representation (“observe”) and vice-versa (“apply”), licensing a powerful form of “diagrammatic reasoning.” Assuming a basic working knowledge of the language of first order logic (the introduction suggests to use the book together with The Language of First Order Logic), the book starts introducing simple proof-rules that check sentential information against the givens (getting either a proof of consequence or inconsistency). Among the rules we find a powerful (semi-)checker of logical consequence. The second part (‘Diagrammatic Reasoning’) discusses at length the crucial “apply” rule, proof by cases, and extraction of common consequences from hypothetical subproofs. At the end the student should be able to establish fairly sophisticated goals, e.g. independence (something cannot be determined by the givens), constrained independence, or non-consequence goals. The third part (‘Sentential Reasoning’) deals with explicit introduction and elimination rules for connectives and quantifiers. The treatment here is more conventional, and this part (of the book and of the program) could be used as a proof-checker for The Language of First Order Logic. The last chapter discusses the relations between diagrammatic and sentential reasoning, showing how some goal may be established by diagrammatic reasoning (where we exploit knowledge on the actual structure of a model) but not by pure sentential reasoning (where we reason only up to elementary equivalence).

If the book is clearly written and offer a wealth of interactive examples and exercises, the program is a little gem, well designed and engineered. I especially liked the shrinking of the picture at the shrinking of the window, the change in the keyboard abbreviations depending on the context of use, and the use of color.

The message Hyperproof conveys is simple, and almost trivial for most working mathematicians: we can teach formal reasoning without a formalistic attitude. The wealth of examples, the careful choice of proof-rules, the intertwining between the description of the rules and the tactics (and the goals) in which they are usually used, the insistence on diagrammatic reasoning, make this message clear and effective.

My only criticism is the lack of a complete integration between The Language of First Order Logic (as representative of any introduction to the formal language of logic) and the Hyperproof book. Indeed, the book is much more than a manual for the program, yet not a complete and self-contained essay on formal reasoning. Even the authors seem to admit this, if in the Preface they feel the need to announce they are ‘developing a full-sized textbook [...] to analytical reasoning’, which however will not be ready before ‘several years’ (p. xv). For the time being, Hyperproof sets the standards for any analogous enterprise.

(February 1996)