We here examine the expressive power of first order logic with generalized quantifiers over finite ordered structures. In particular, we address the following problem: Given a family Q of generalized quantifiers expressing a complexity class C, what is the expressive power of first order logic FO(Q) extended by the quantifiers in Q? From previously studied examples, one would expect that FO(Q) captures L C , i.e., logarithmic space relativized to an oracle in C. We show that this is not always (...) true. However, after studying the problem from a general point of view, we derive sufficient conditions on C such that FO(Q) captures L C . These conditions are fulfilled by a large number of relevant complexity classes, in particular, for example, by NP. As an application of this result, it follows that first order logic extended by Henkin quantifiers captures L NP . This answers a question raised by Blass and Gurevich [Ann. Pure Appl. Logic, vol. 32, 1986]. Furthermore we show that for many families Q of generalized quantifiers (including the family of Henkin quantifiers), each FO(Q)-formula can be replaced by an equivalent FO(Q)-formula with only two occurrences of generalized quantifiers. This generalizes and extends an earlier normal-form result by I. A. Stewart [Fundamenta Inform. vol. 18, 1993]. (shrink)

The often observed complexity gap between the expressiveness of a logical formalism and its exponentially harder expression complexity is proven for all logical formalisms which satisfy natural closure conditions. The expression complexity of the prefix classes of second-order logic can thus be located in the corresponding classes of the weak exponential hierarchies; further results about expression complexity in database theory, logic programming, nonmonotonic reasoning, first-order logic with Henkin quantifiers and default logic are concluded. The proof method illustrates the significance of (...) quantifier-free interpretations in descriptive complexity theory. (shrink)

We start with a simple proof of Leivant's normal form theorem for ∑11 formulas over finite successor structures. Then we use that normal form to prove the following:1. over all finite structures, every ∑21 formula is equivalent to a ∑21 formula whose first-order part is a Boolean combination of existential formulas, and2. over finite successor structures, the Kolaitis-Thakur hierarchy of minimization problems collapses completely and the Kolaitis-Thakur hierarchy of maximization problems collapses partially.The normal form theorem for ∑21 fails if ∑21 (...) is replaced with ∑11 or if infinite structures are allowed. (shrink)

We consider the problem of obtaining logical characterisations of oracle complexity classes. In particular, we consider the complexity classes LOGSPACENP and PTIMENP. For these classes, characterisations are known in terms of NP computable Lindström quantifiers which hold on ordered structures. We show that these characterisations are unlikely to extend to arbitrary structures, since this would imply the collapse of certain exponential complexity hierarchies. We also observe, however, that PTIMENP can be characterised in terms of Lindström quantifers , though it remains (...) open whether this can be done for LOGSPACENP. (shrink)

It was conjectured by Halpern and Kapron (Annals of Pure and Applied Logic, vol. 69, 1994) that frame satisfiability of propositional modal formulas is incomparable in expressive power to both Σ 1 1 (Ackermann) and Σ 1 1 (Bernays-Schonfinkel). We prove this conjecture. Our results imply that Σ 1 1 (Ackermann) and Σ 1 1 (Bernays-Schonfinkel) are incomparable in expressive power, already on finite graphs. Moreover, we show that on ordered finite graphs, i.e., finite graphs with a successor, Σ 1 (...) 1 (Bernays-Schonfinkel) is strictly more expressive than Σ 1 1 (Ackermann). (shrink)

This book constitutes the refereed proceedings of the 5th Kurt Gödel Colloquium on Computational Logic and Proof Theory, KGC '97, held in Vienna, Austria, in August 1997. The volume presents 20 revised full papers selected from 38 submitted papers. Also included are seven invited contributions by leading experts in the area. The book documents interdisciplinary work done in the area of computer science and mathematical logics by combining research on provability, analysis of proofs, proof search, and complexity.