Skip to main content
main-content
Top

About this book

Finite model theory is an area of mathematical logic that grew out of computer science applications. The main sources of motivational examples for finite model theory are found in database theory, computational complexity, and formal languages, although in recent years connections with other areas, such as formal methods and verification, and artificial intelligence, have been discovered. The birth of finite model theory is often identified with Trakhtenbrot's result from 1950 stating that validity over finite models is not recursively enumerable; in other words, completeness fails over finite models. The tech­ nique of the proof, based on encoding Turing machine computations as finite structures, was reused by Fagin almost a quarter century later to prove his cel­ ebrated result that put the equality sign between the class NP and existential second-order logic, thereby providing a machine-independent characterization of an important complexity class. In 1982, Immerman and Vardi showed that over ordered structures, a fixed point extension of first-order logic captures the complexity class PTIME of polynomial time computable propertiE~s. Shortly thereafter, logical characterizations of other important complexity classes were obtained. This line of work is often referred to as descriptive complexity. A different line of finite model theory research is associated with the de­ velopment of relational databases. By the late 1970s, the relational database model had replaced others, and all the basic query languages for it were es­ sentially first-order predicate calculus or its minor extensions.

Table of Contents

Frontmatter

1. Introduction

Abstract
Finite model theory studies the expressive power of logics on finite models. Classical model theory, on the other hand, concentrates on infinite structures: its origins are in mathematics, and most objects of interest in mathematics are infinite, e.g., the sets of natural numbers, real numbers, etc. Typical examples of interest to a model-theorist would be algebraically closed fields (e.g., 〈ℂ, +, •〉), real closed fields (e.g., 〈ℝ, +, •, <〉), various models of arithmetic (e.g., 〈ℕ, +, ·〉 or 〈ℕ, +〉), and other structures such as Boolean algebras or random graphs.
Leonid Libkin

2. Preliminaries

Abstract
The goal of this chapter is to provide the necessary background from mathematical logic, formal languages, and complexity theory.
Leonid Libkin

3. Ehrenfeucht-Fraïssé Games

Abstract
We start this chapter by giving a few examples of inexpressibility proofs, using the standard model-theoretic machinery (compactness, the Löwenheim-Skolern theorem). We then show that this machinery is not generally applicable in the finite model theory context, and introduce the notion of Ehrenfeucht-Fraïssé games for first-order logic. We prove the EhrenfeuchtFraïssé theorem, characterizing the expressive power of FO via games, and introduce the notion of types, which will be central throughout the book.
Leonid Libkin

4. Locality and Winning Games

Abstract
Winning games becomes nontrivial even for fairly simple examples. But often we can avoid complicated combinatorial arguments, by using rather simple sufficient conditions that guarantee a winning strategy for the duplicator. For first-order logic, most such conditions are based on the idea of locality, best illustrated by the example in Fig. 4.1.
Leonid Libkin

5. Ordered Structures

Abstract
We know how to prove basic results about FO; so now we start adding things to FO. One way to make FO more expressive is to include additional operations on the universe. For example, in database applications, data items stored in a database are numbers, strings, etc. Both numbers and strings could be ordered; on numbers we have arithmetic operations, on strings we have concatenation, substring tests, and so on. As query languages routinely use those operations, one may want to study them in the context of FO.
Leonid Libkin

6. Complexity of First-Order Logic

Abstract
The goal of this chapter is to study the complexity of queries expressible in FO. We start with the general definition of different ways of measuring the complexity of a logic over finite structures: these are data, expression, and combined complexity. We then connect FO with Boolean circuits and establish some bounds on the data complexity. We also consider the issue of uniformity for a circuit model, and study it via logical definability. We then move to the combined complexity of FO, and show that it is much higher than the data complexity. Finally, we investigate an important subclass of FO queries — conjunctive queries — which play a central role in database theory.
Leonid Libkin

7. Monadic Second-Order Logic and Automata

Abstract
We now move to extensions of first-order logic. In this chapter we introduce second-order logic, and consider its often used fragment, monadic second-order logic,or MSO, in which one can quantify over subsets of the universe. We study the expressive power of this logic over graphs, proving that its existential fragment expresses some NP-complete problems, but at the same time cannot express graph connectivity. Then we restrict our attention to strings and trees, and show that, over them, MSO captures regular string and tree languages. We explore the connection with automata to prove further definability and complexity results.
Leonid Libkin

8. Logics with Counting

Abstract
We continue dealing with extensions of first-order logic. We have seen that the expressive power of FO on finite structures is limited in a number of ways: it cannot express counting properties, nor is it capable of expressing properties that require iterative algorithms, as those typically violate locality.
Leonid Libkin

9. Turing Machines and Finite Models

Abstract
In this chapter we introduce the technique of coding Turing machines in various logics. It is precisely this technique that gave rise to numerous applications of finite model theory in computational complexity. We start by proving the earliest such result, Trakhtenbrot’s theorem, stating that finite satisfiability is not decidable. For the proof of Trakhtenbrot’s theorem, we code Turing machines with no inputs. By a refinement of this technique, we code nondeterministic polynomial time Turing machines in existential second-order logic (∃SO), proving Fagin’s theorem stating that∃SO-definable properties of finite structures are precisely those whose complexity is NP.
Leonid Libkin

10. Fixed Point Logics and Complexity Classes

Abstract
Most logics we have seen so far are not well suited for expressing many tractable graph properties, such as graph connectivity, reachability, and so on. The limited expressiveness of FO and counting logics is due to the fact that they lack mechanisms for expressing fixed point computations. Other logics we have seen, such as MSO, ∃SO, and ∀SO, can express intractable graph properties.
Leonid Libkin

11. Finite Variable Logics

Abstract
In this chapter, we introduce finite variable logics: a unifying tool for studying fixed point logics. These logics use infinitary connectives already seen in Chap. 8, but here we impose a different restriction: each formula can use only finitely many variables. We show that fixed point logics LFP, IFP, and PFP can be embedded in such a finite variable logic. Furthermore, the finite variable logic is easier to study: it can be characterized by games, and this gives us bounds on the expressive power of fixed point logics; in particular, we show that without a linear ordering, they fail to capture complexity classes. We then study definability and ordering of types in finite variable logics, and use these techniques to relate separating complexity classes to separating sonic fixed point logics over unordered structures.
Leonid Libkin

12. Zero-One Laws

Abstract
In this chapter we show that properties expressible in many logics are almost surely true or almost surely false; that is, either they hold for almost all structures, or they fail for almost all structures. This phenomenon is known as the zero-one law. We prove it for FO, fixed point logics, and L ω ω . We shall also see that the “almost everywhere” behavior of logics is drastically different from their “everywhere” behavior. For example, while satisfiability in the finite is undecidable, it is decidable if a sentence is true in almost all finite models.
Leonid Libkin

13. Embedded Finite Models

Abstract
In finite model theory, we deal with logics over finite structures. In embedded finite model theory, we deal with logics over finite structures embedded into infinite ones.
Leonid Libkin

14. Other Applications of Finite Model Theory

Abstract
In this final chapter, we briefly outline three different application areas of finite model theory. In mathematical logic, finite models are used as a tool for proving decidability results for satisfiability of FO sentences. In the area of temporal logics and verification, one analyzes the behavior of certain logics on some special finite structures (Kripke structures). And finally, it was recently discovered that many constraint satisfaction problems can be reduced to the existence of a homomorphism between two finite structures.
Leonid Libkin

Backmatter

Additional information