n + 1 nested k-ary fixed point operators are more expressive than n. This holds on finite structures for all sublogics of partial fixed point logic PFP that can express conjunction, existential quantification and deterministic transitive closure of binary relations using at most k-ary fixed point operators and that are closed against subformulas. Among those are a lot of popular fixed point logics.

We show that the loosely guarded and packed fragments of first-order logic have the finite model property. We use a construction of Herwig and Hrushovski. We point out some consequences in temporal predicate logic and algebraic logic.

In this paper we prove that thek-ary fragment of transitive closure logic is not contained in the extension of the (k−1)-ary fragment of partial fixed point logic by all (2k−1)-ary generalized quantifiers. As a consequence, the arity hierarchies of all the familiar forms of fixed point logic are strict simultaneously with respect to the arity of the induction predicates and the arity of generalized quantifiers.Although it is known that our theorem cannot be extended to the sublogic deterministic transitive closure logic, (...) we show that an extension is possible when we close this logic under congruence. (shrink)