Book review of

The classical Decision Problem

by

E. Börger, E. Grädel and Y. Gurevich

Review by Maarten Marx

October 23, 1998

This book is about --as its title suggests-- the classical decision problem, also known as Hilbert's Entscheidungsproblem. The preface promises a comprehensive modern treatment of the subject; indeed it does, in a very thorough but still, I think, to most of the intended audience (logicians, computer scientists, mathematicians and philosophers of science) rather accessible manner. The book contains an enormous wealth of techniques, tricks and methods for showing decidability or undecidability of logics, and, in the decidable cases, also methods to establish the exact complexity of the decision algorithms. I guess that not a lot of people would want to read it in one go. Browsing through it might be a dangerous experience though: on several occasions I was, without realising it, drawn deeply into it and the hours had flown by.
For everyone with an interest in decidability or complexity questions related to logic this book is a valuable reference which you will always want to have within reach. As a guide to the literature in the field the book is highly useful. Each chapter ends with a pleasantly written section containing historical remarks (having the additional advantage of not cluttering up the places where real work is to be done). The bibliography is an outstanding achievement. In more than 50 pages, 549 annotated references are given. The annotations not only contain a short abstract of the work, they also often make connections with other works or with the text itself.
Any attempt to faithfully describe the contents of this book in a review is doomed to fail. Here I will concentrate on the main line: the decision problem, its transformation into the classification problem, and the way it is solved. After that I will add some remarks concerning tiling problems, other fragments of first order logic, and end with some personal remarks.

The classical decision problem can be formulated in several equivalent ways. Here we give one which is most in the spirit of this book

The satisfaction problem Given a first order sentence, decide whether it has a model. Hilbert made this problem into a central problem of mathematical logic. He writes together with Ackermann:

The Entscheidungsproblem is solved when we know a procedure that allows for any given logical expression to decide by finitely many operations its validity or satisfiability. (. . . ) The Entscheidungsproblem must be considered the main problem of mathematical logic. [Translation given in the book, page 3]
They were not alone in their appreciation of the importance of this problem as some nice quotes in the book indicate. We can sharpen Hilbert's question to a yes/no question: Does there exists an algorithm that decides for any first order sentence whether it has a model? The hard problem logicians were facing at that time can be paraphrased as follows:
"Suppose I believe the answer is no. How on earth am I going to prove it? I can verify if something can rightly be called an algorithm (that is, it is a mechanical procedure which is guaranteed to terminate on any of its specified inputs), but who am I to give a precise mathematical definition of an algorithm."
It took someone as Alan Turing to make the bold step. He took the word "mechanical" literally and created his now famous Turing Machines. He then boldly stated that a function from strings of symbols to strings of symbols is computable if and only if it is computable by a Turing Machine. He then showed that no Turing Machine could decide the satisfaction problem for first order sentences and declared the decision problem solved. Independently Church showed that no recursive function could solve the satisfaction problem. He made a similar bold statement now known as Church's Thesis. It was quickly established that both Turing's and Church's Theses were equivalent. (Since then many more alternative theses have been put forward, all equivalent to the Church-Turing Thesis.) The classical decision problem was solved.
For one thing, the solution showed that mathematicians need not worry about their jobs, or indeed that they would be forced to work in the mechanical manner described by the would-be algorithm. But the logicians did not let their decision problem be solved just like that. At the time of Church and Turing's discovery several fragments of first order logic were already shown to be decidable, and others to be as hard to decide as the whole language. This naturally led to the

classification problem Which fragments are decidable for satisfiability, and which are undecidable?

Stated like this, this question would indeed generate quite a lot of work since there are just too many fragments. Traditionally the focus was on formulas in prenex form and eventually the decision problem evolved into the classification problem for these traditional fragments. (Note that other traditions may lead to very different types of fragments, see e.g., the guarded fragment coming from the modal tradition below.)
To specify a prefix vocabulary class in a language without nullary predicate and function symbols, one has to set three parameters:

  1. the allowed prefixes, i.e., strings in the alphabet { A, E } [where A, resp. E, denotes the universal, resp. existential, first order quantifier]

  2. for each arity n, the number of n-ary predicate symbols

  3. for each arity n, the number of n-ary function symbols.
In addition we can consider languages with or without equality (=). Most natural classes can be written succinctly. For example, the Gödel class of all first order formulas without function symbols and without equality with prefix E* A2 E*, meaning all prefixes have the form of an arbitrary number of existential, followed by at most two universal, followed again by an arbitrary number of existential quantifiers. In the notation of the book: [E* A2 E*, all, (0)] (the prefix, followed by a specification of the number of predicate symbols of each arity, followed by the same information but about function symbols). The class is decidable. In contrast to what Gödel claimed in the last line of his paper, his proof does not go though when equality is added to the language. In fact the class [E* A2 E*, (0, 1), (0)]=, that is the fragment with equality, the same quantifier prefix, but only one binary predicate symbol was shown to be undecidable by Goldfarb. (For references, see the book.)
Still there are very many different prefix classes. A guide to the research in the classification problem was provided by Gurevich' Classifiability Theorem, the main idea of which is as follows. The classes of prefix vocabulary classes of prenex formulas form a well partially ordered set, where the collection of positive classes (the decidable ones) is closed downward. It follows that there is a finite collection of minimal negative classes which dominates all negative classes. The number of maximal standard (see Definition 1.3.2) positive classes is finite as well. So Gurevich' Theorem tells us that a monograph which covers the complete solution of the classification problem thus restricted is at least possible. In fact the solution can be given in a finite table which fits on one page: there are 16 minimal undecidable standard classes and 7 maximal decidable standard ones.
The main bulk of the book consists of a thorough treatment of all these classes. In addition, the complexity of the satisfaction problem is determined for all but the very difficult Shelah class. Especially the undecidability proofs can involve some highly complex coding techniques. In essence the undecidability proof of first order logic using the domino or tiling problem is completely straightforward, as long as we allow ourselves enough relation symbols. The difficulties arise when we restrict the number of relation (or function) symbols to some fixed finite set. The two chapters on the decidable classes are divided by the classes with the finite model property and the ones without. Proving decidability via finite models is a natural route. This chapter contains a wealth of techniques which are also useful for say modal logicians. For the decidable cases without the finite model property, heavier machinery is needed. The proofs given rely on Rabin's result on the decidability of S2S, of which a complete simplified proof is provided as well.
This very briefly summarises the main topic of this book. In the remainder of this review I pick some gems that we meet on the way. One of the nice features of the book is its use of tiling problems to show undecidability and lower complexity bounds. This should attract the more LL-oriented readers of JoLLI since the problem and the reductions are often easy to understand and to visualise, and in my opinion to be preferred to Turing Machine encodings. The book contains an appendix by Cyril Allauzen and Bruno Durand which gives elementary proofs of the undecidability of several tiling problems. A very nice theorem concerning tilings and conservative reduction classes is Corollary 3.1.8. It prescribes a simple recipe for showing that a fragment of first order logic is a conservative reduction class by using the NxN tiling problem.
As said above, you can't do all, so the book focuses on the standard prefix vocabulary classes. That doesn't mean other classifications are neglected. To the contrary, we also see e.g., restrictions on the boolean part (Horn and Krom formulas) and restrictions of the number of variables (first order logic with two variables). Prenex formulas are not the main interest for modal logicians, for the simple reason that modal formulas do not translate into prenex classes. For them a classification along the so-called Guarded Fragments of Andréka, van Benthem and Németi [1, 2] gives more insight. Unfortunately these fragments are only briefly mentioned in the book. We can hardly blame the authors though, since the conception of these fragments and the publication of the book almost coincided.
I want to mention one open problem in the book which has a distinct modal flavour as well. Determine the exact complexity of C2 (first order logic with only two variables, no function symbols plus coordinate-wise counting). The satisfaction problem is decidable, but the known proofs only give the worst possible upper bounds. In a simplified form, the modal (or cylindric algebraic) counterpart of this problem is to determine the complexity of the product in the sense of Gabbay and Shehtman [4] of two difference operators. The complexity of the product of two universal modalities is known and equals that of L2: the satisfaction problem is NEXPTIME complete.
Let me finally consider the main question of any review: should one buy this book? There are several books on the same topic on the market, notably [3] on solvable cases and the complementary [5] on the undecidable ones. I bet that most researchers who possess these two volumes already have obtained the book presently under review. If you are interested in decision and complexity problems in logic, this book is highly recommended. For the novice in the field the book might be a bit intimidating. Unfortunately, a dependency diagram is missing (it contains a good one for Chapter 3). The table of contents gives a good overview though, but I can imagine the beginner still getting lost. The modular and clear organisation of the book makes it possible to organise several "Quick Guided Tours" of varying degree of difficulty through it. If ever a cheaper paperback edition will appear, it would be nice to add one or two of such tours.

Publishers Information

E. Brger , University of Pisa, Italy
E. Grdel , RWTH Aachen, Germany
Y. Gurevich , University of Michigan, Ann Arbor, MI, USA

The Classical Decision Problem

This is the most complete and comprehensive treatment
available in book form of the classical decision problem
of mathematical logic and its role in modern
computer science. A revealing analysis of the natural
order of decidable and undecidable cases is given,
and of particular interest to the reader will be the
complete classification of the solvable and
unsolvable standard cases of the classical decision
problem, the complexity analysis of the solvable
cases, the extremely comprehensive treatment of the
reduction method, and the model-theoretic analysis of
solvable cases. Many cases are treated here for the
first time, and a great number of simple proofs and
exercises have been included. The results and methods
of the book have been used in logic, computer science
& artifical intelligence.

Keywords: Decision Problem, Complexity,
Undecidability, Finite Models, First-Order
Logic.

Fields: Mathematical Logic and Set Theory;
Math. Appl. in Computer Science; Formal
Languages

Written for: Graduate students and researchers
in mathematical logic and theoretical computer
science

1997 . XII, 482 pp.
ISBN 3-540-57073-X
Hardcover DM 158,-
(Recommended Retail Price)
Available

Book category: Monograph Publication language English
(Perspectives in Mathematical Logic. Eds.: M. Lerman;
S. Feferman; W.A. Hodges; A.J. Macintyre; M.
Magidor; Y.N. Moschovakis. )

References

[1]
H. Andréka, J. van Benthem, and I. Németi. Back and forth between modal logic and classical logic. Bulletin of the Interest Group in Pure and Applied Logics, 3(3):685-720, 1995.

[2]
H. Andréka, J. van Benthem, and I. Németi. Modal languages and bounded fragments of predicate logic. Journal of Philosophical Logic, 27(3):217-274, 1998.
[3]
B. Dreben and W. Goldfarb. The Decision Problem: Solvabale Cases of Quantificational Formulas. Addison-Wesley, 1997.

[4]
D. Gabbay and V. Shehtman. Products of modal logics, Part 1. Logic Journal of the IGPL, 6(1):73-146, 1998.

[5]
H. Lewis. Unsolvable Classes of Quantificational Formulas. Addison-Wesley, 1997.