You are here

Kripke's Worlds

Olivier Gasquet, Andreas Herzig, Bilal Said and François Schwarzentruber
Publication Date: 
Number of Pages: 
Studies in Universal Logic
[Reviewed by
Russell Jay Hendel
, on

This is an excellent book to use — either as a stand-alone text or with another textbook — for an introductory undergraduate course in logic addressed to majors in the humanities, social sciences, computer science, or mathematics. Although the book is a bit different from other logic textbooks, precisely because of that it may be more suitable.

To understand this, note that very often an introductory logic course is a service course. Typically the purpose of the course is a) to prepare computer science majors for dealing with boolean propositions, b) to prepare mathematics majors for dealing with proofs of statements involving quantifiers, c) to prepare philosophy majors for formal systems which capture the essence of logical arguments or d) to fulfill a general education mathematics requirement. One problem with such service courses is that the traditional textbooks spend too much time on formal systems, manipulative exercises and verbal logic derivations which do not serve any purpose outside the course. Indeed, it takes only a few class days to teach boolean connectives, truth tables, and even quantifiers, including standard applications such as verbal logic derivations.

Wouldn’t it be nice if the instructor could spend the rest of the term dealing with challenging and engaging topics showing the very rich applicability of mathematics? And that is exactly what this short but well written book does: In addition to traditional topics such as atomic formulae, boolean connectives, formulas, subformulas, formula length, arity, parenthesis convention, and atomic formulae, this charming book deals with modality (necessity and possibility), temporality (always, sometimes, henceforth, eventually, next, until, since, before, and after), knowledge and belief, deontic concepts (obligation and permission) and motivation (goals and intentions).The material in this book also has application to artificial intelligence, computer program semantics, and the semantic web.

A basic unifying theme of the book is to construct models of possible worlds and to check formula satisfiability using graph-theoretic tableaux systems. Rather nicely, in the past quarter of a century there is a trend to implement tableaux systems on computers. The book comes with accompanying free software, LoTREC, the result of about a decade of Master’s and Ph.D theses studying how to create a simple, easy visual systems to build models and check satisfiability.

The book has many of the characteristics of good textbooks:

·         Sections: There are 47 sections (excluding the typically one-paragraph summary sections). This is just enough for a 15 week, 3-day a week course

·         Exercises: There are 84 exercises. Since these are not plug-ins but involve use of software, thinking and interpretation I believe this is adequate.

·         Software: It is always a plus when a modern textbook has accompanying software. The accompanying software, LoTREC, is not “off the shelf” software (which typically has many uncomfortable points). It was carefully developed and tested. Users comment on the simplicity and ease of using it.

·         Diagrams: The book is filled with user-friendly graphs and LoTREC code.

·         Bibliography: The book has 50 nice references (for the ambitious instructor who likes to assign journal readings as part of the course).

·         Length: Under 200 pages - it has the lean and lively look.

Those who are still unsure whether they want to base a course on the book can preview the LoTREC software at

Russell Jay Hendel (RHendel@Towson.Edu) holds a Ph.D. in mathematics and an Associateship from the Society of Actuaries. He teaches at Towson University. His interests include discrete number theory, applications of technology to education, problem writing, actuarial science and the interaction between mathematics, art and poetry.