Hyperproof for the Macintosh. Program by Gerard Allwein, Mark Greaves, and Michael Lenz. Incl. 1 disk. (English) Zbl 0860.03004

Barwise, Jon; Etchemendy, John

CSLI Lecture Notes. 42. Stanford, CA: CSLI, Center for the Study of Language and Information. xvii, 255 p. (1994).

Can teaching logic be fun? Starting from Lewis Carroll (and even earlier), many nice logical puzzles have been proposed (or at least puzzles that can be solved by using logic). However, many of these puzzles and problems use pictures. It is definitely possible to re-formulate these pictures in standard logical form (i.e., as sentences), but part of the fun disappears in this translation. The authors of the book describe a formal language for pictures and thus, manage to combine the fun (and the pictures) with mathematical exactness. They started doing so in their previous program, Tarski’s World. In that program, to form a world, blocks of three different shapes (cube, tetrahedron, and dodecahedron) and three different sizes (small, medium, and large) were placed on different cells of a finite 2-D grid. The main goal of Tarski’s World was to check whether a given logical statement is true or not in a given world. The new program allows incomplete information: we can have blocks of known shape but unknown size, blocks of known size but unknown shape, and blocks of known size and shape but unknown location. Cute graphical conventions are used to visualize this incomplete information. Blocks can also be happy or not, and blocks can like or dislike each other. In situations with incomplete information, a given statement can be not only true or false, but also unknown. The main goal of Hyperproof is to generate proofs (and thus, to teach the students how to use and design proofs). The initial information is provided by means of a pictorial situation, usually complemented by one or several logical statements. Steps in the proof are either formulas or new situations obtained by using one of the rules. The book starts with examples of proofs of consequence (that a certain statement \(Q\) follows from the initial information) and of nonconsequence (that \(Q\) does not follow). Correspondingly, three types of queries are allowed: “prove \(Q\)”, “show that \(Q\) does not follow”, and (an open-question query) “does \(Q\) follow?”. An important new feature of Hyperproof pictures is that they can contain inconsistent partial information. Checking inconsistency is covered in Chapter 4. Chapter 7 handles another important logical notion: logical independence. Independence proofs are presented. In Parts I and II, only propositional statements were allowed. In Part III, the logic is extended to statements with quantifiers. To make the formal language closer to the common sense use of logic, the authors introduce “numerical quantifiers” of the type “at least \(k\) different objects have the property \(P(x)\)”. It turns out that these extra quantifiers clarify the formulas a lot, while their addition, luckily, does not make the programs seriously slower. Along the way, the authors handle lots of interesting logical results: for example, Russell’s barber paradox is illustrated by a theory in which a block likes those and only those blocks that do not like themselves. This book is not for simply reading: it is rather a (nicely written) instruction manual for an attached Macintosh program. The user must be already familiar with the material of one of the authors’ previous books: The language of first-order logic, including the Macintosh version of Tarski’s World, 3rd ed. (1993; Zbl 0858.03002).

Reviewer: V.Ya.Kreinovich (El Paso)

MSC:

03-01	Introductory exposition (textbooks, tutorial papers, etc.) pertaining to mathematical logic and foundations
03-04	Software, source code, etc. for problems pertaining to mathematical logic and foundations
03B10	Classical first-order logic

Keywords:

first-order logic; logic textbook; Hyperproof; formal language for pictures; incomplete information; proofs; consequence; nonconsequence; inconsistency; logical independence; Russell’s barber paradox; Macintosh program

Citations:

Zbl 0858.03002

Software:

Hyperproof