Model theory is concerned mainly, although not exclusively, with infinite structures. In recent years, finite structures have risen to greater prominence, both within the context of mainstream model theory, e.g., in work of Lachlan, Cherlin, Hrushovski, and others, and with the advent of finite model theory, which incorporates elements of classical model theory, combinatorics, and complexity theory. The purpose of this survey is to provide an overview of what might be called the model theory of finite structures. Some topics in (...) finite model theory have strong connections to theoretical computer science, especially descriptive complexity theory. In fact, it has been suggested that finite model theory really is, or should be, logic for computer science. These connections with computer science will, however, not be treated here.It is well-known that many classical results of ‘infinite model theory’ fail over the class of finite structures, including the compactness and completeness theorems, as well as many preservation and interpolation theorems. The failure of compactness in the finite, in particular, means that the standard proofs of many theorems are no longer valid in this context. At present, there is no known example of a classical theorem that remains true over finite structures, yet must be proved by substantially different methods. It is generally concluded that first-order logic is ‘badly behaved’ over finite structures.From the perspective of expressive power, first-order logic also behaves badly: it is both too weak and too strong. Too weak because many natural properties, such as the size of a structure being even or a graph being connected, cannot be defined by a single sentence. Too strong, because every class of finite structures with a finite signature can be defined by an infinite set of sentences. Even worse, every finite structure is defined up to isomorphism by a single sentence. In fact, it is perhaps because of this last point more than anything else that model theorists have not been very interested in finite structures. Modern model theory is concerned largely with complete first-order theories, which are completely trivial here. (shrink)

We investigate properties of propositional modal logic over the classof finite structures. In particular, we show that certain knownpreservation theorems remain true over this class. We prove that aclass of finite models is defined by a first-order sentence and closedunder bisimulations if and only if it is definable by a modal formula.We also prove that a class of finite models defined by a modal formulais closed under extensions if and only if it is defined by a -modal formula.

Provability, Computability and Reflection.

In this dissertation, I investigate some questions about the model theory of finite structures. One goal is to better understand the expressive power of various logical languages, including first-order logic , over this class. A second, related, goal is to determine which results from classical model theory remain true when relativized to the class, ${\cal F}$, of finite structures. As it is well-known that many such results become false, I also consider certain weakened generalizations of classical results. ;I prove some (...) basic results about the languages $L\sp{k}$ and $L\sbsp{\infty\omega}{k},$ the existential fragments of the finite variable logics $L\sp{k}$ and $L\sbsp{\infty\omega}{k}$. I show that there are finite models whose $L\sp{k}$-theories are not finitely axiomatizable. I also establish the optimality of a normal form for $L\sbsp{\infty\omega}{k},$ and separate certain fragments of this logic. I introduce a notion of a 'generalized preservation theorem', and establish certain partial positive results. I then show that existential preservation fails for the language $L\sbsp{\infty\omega}{k}$, both over ${\cal F}$ and over the class of all structures. I also examine other preservation properties, e.g. for classes closed under homomorphisms. ;In the final chapter, I investigate the finite model theory of propositional modal logic. I show that, in contrast to more expressive logics, modal logic is 'well-behaved' over ${\cal F}$. In particular, I establish that various theorems that are true over the class of all structures also hold over ${\cal F}$. I prove that, over ${\cal F}$, a class of models is FO-definable and closed under bisimulations iff it is defined by a modal FO sentence. In addition, I prove that, over ${\cal F}$, a class is defined by a modal sentence and closed under extensions iff it is defined by a D-modal sentence. (shrink)

The model-checking problem for a logic L on a class C of structures asks whether a given L-sentence holds in a given structure in C. In this paper, we give super-exponential lower bounds for fixed-parameter tractable model-checking problems for first-order and monadic second-order logic. We show that unless PTIME=NP, the model-checking problem for monadic second-order logic on finite words is not solvable in time f·p, for any elementary function f and any polynomial p. Here k denotes the size of the (...) input sentence and n the size of the input word. We establish a number of similar lower bounds for the model-checking problem for first-order logic, for example, on the class of all trees. (shrink)