(preliminary version)
Fixed Point Logics and Finite Model Theory
Anuj Dawar
For many applications of logic in the computational and cognitive
sciences, first order predicate logic and its variants hold a central
role, often solely for historical reasons. In many areas where
recursive or inductive definitions are important, a more appropriate
logic is obtained by allowing explicit fixed point constructions, and
such logics have found incresingly widespread use. Examples include
the study of inductive definitions in arithmetic, the least fixed
point logic that plays a central role in finite model theory and the
modal mu-calculus. The systematic study of fixed point logics, their
expressive power and their model theory has been undertaken, mainly in
the context of finite model theory. This course of lectures will
present an introduction to this study, by attempting a unified
treatment of fixed point logics, including model-theoretic and
proof-theoretic aspects, as well as their connections with models of
computation, computational complexity and logics of verification. The
course will also provide an introduction to finite model theory for
those not familiar with the subject. However, it will assume a sound
knowledge of logic, particluarly first order predicate logic, as might
be obtained in an introductory graduate course.