Нет обложки

In classical model theory first-order logic has always played an overwhelming role, whereas in finite model theory there has been an emphasis on the study of more expressive logics right from the start. A reason for this is that most classical results and methods fail in the scope of finite models, and first-order logic loses its distinguishing features such as the compactness theorem and the Lowenheim Skolem theorem.Furthermore, an important direction in finite model theory is the study of the connection between computational complexity and logical expressibility. It is evident that for this purpose the logics need to be able to describe recursion in an appropriate way which first-order logic is not.So it seems reasonable to strengthen first-order logic by a suitable recursion mechanism. A natural way to do this is to augment it by a fixed-point operator. In fact there are different ways to define such an operator which result in several well-known fixed-point logics such as partial fixed-point logic and least fixed-point logic.Logics with a fixed-point operator have already played a role in classical recursion theory as a way to formalize inductive definitions. In particular, Moschovakis devoted a monograph [Mos74] to the study of this subject. Many basic results that have later been applied in finite model theory were given there.