* The classical Decision Problem *

by

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

October 23, 1998

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:

- the allowed prefixes, i.e., strings in the alphabet
{
**A**,**E**} [where**A**, resp.**E**, denotes the universal, resp. existential, first order quantifier] - for each arity n, the number of n-ary predicate symbols
- for each arity n, the number of n-ary function symbols.

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

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

I want to mention one open problem in the book which has a distinct modal flavour as well. Determine the exact complexity of C

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.

E. Brger , University of Pisa, Italy

E. Grdel , RWTH Aachen, Germany

Y. Gurevich , University of Michigan, Ann Arbor, MI, USAThe 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

science1997 . 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. )

- [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.