(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.