In [1], Yuri Gurevich discusses the achievements of mathematical logic and states that “logic grows more relevant to computer science than any other part of mathematics.” He goes on to argue that applications in computer science require new formalizations that are related to the “finiteness” and the “dynamic” characters of the computer. The authors of this paper carry on in this spirit. The main result established is that if a first order formula &fgr; ( P ) is monotone in a predicate symbol P over finite structures it is not necessarily positive in P. (A formula &fgr; ( P ) is said to be monotone in P if P ⊆ Q logically implies &fgr; ( P ) ⊆ &fgr; ( Q ) ; a formula is said to be positive if it is equivalent to a formula without any negation signs.) The authors construct a monotone formula in P that is not positive in P. This example is used to establish a related result about monotone Boolean circuits and positive Boolean circuits, which provides a basis for a study of the lower bounds on the complexity of Boolean circuits.

With the exception of a few bothersome typographical errors the paper is well written, and the proof of the main theorem is impressive. However, its contents will only be accessible to someone with a knowledge of first order logic and some familiarity with the literature in the field.