Fixed-point logics are a class of logics designed for formalising
recursive or inductive definitions. Being initially studied in
generalised recursion theory by Moschovakis and others, they have later
found numerous applications in computer science, in areas
such as database theory, finite model theory, and verification.
A common feature of most fixed-point logics is that they extend a basic
logical formalism such as first-order or modal logic by explicit
constructs to form fixed points of definable operators. The type of
fixed points that can be formed as well as the underlying logic
determine the expressive power and complexity of the resulting logics.
In this talk we will give a brief introduction to the various extensions
of first-order logic by fixed-point constructs and give some examples
for properties definable in the different logics. In the main part of
the talk we will concentrate on extensions of first-order
logic by least and inflationary fixed points. In particular, we
compare the expressive power and complexity of the resulting logics.
The main result will be to show that while the two logics have rather
different properties, they are equivalent in expressive power on the
class of all structures.