Finite Model Theory 1000-2M13TSK

Finite model theory is a branch of theoretical computer science combining various aspects of computational complexity, logic and database theory.

The connection to computational complexity stems from an observation that numerous complexity classes (like LogSpace, P, NP, etc.) can be characterized with certain logics. For instance, each property of ordered graphs that can be tested in polynomial time, can be expressed with a formula of first order logic extended with the fixpoint operators. A typical question we will consider in class is: what is the logical characterisation of a given complexity class?

The connection with computational complexity leads naturally to the questions: What can be expressed in a given logic? Is it true that the two logics can express the same properties? In class we will learn several tools that can be used to distinguish the expressive power of logics: Ehrenfeucht-Fraisse games, zero-one laws, and locality theorems.

The connection to databases is what makes finite model theory useful. A finite model is simply a mathematical formalisation of the concept of database. To run a query on a database (eg. in SQL) is simply to evaluate a formula of some logic in a given model. That is why most problems in database theory (e.g., complexity of query evaluation, deciding if a query is nontrivial, etc.) can be seen as problems in finite model theory. We will see how such problems can be solved using the finite model theory toolbox.