Existential least fixed-point logic and its relatives
Martin Grohe · Journal of Logic and Computation · 1997
The main objects of our interest are the existential fragment 9LFP of least xed{point logic, stratied xed point logic SFP, which is the smallest regular logic containing 9LFP, and transitive closure logic TC. The main result of the rst part of this paper is a normal form for 9LFP, which transfers to SFP to a certain extent. We study some of the consequences of this normal form and show that TC can be seen as a natural fragment of SFP. The second part of the paper is concerned with separating the logics under consideration. Furthermore, it shows that the existential preservation theorem fails for TC and SFP (both on nite and arbitrary structures) . The method used to show this also yields a negative answer to a question posed by Rosen and Weinstein [RW95] concerning rst{order sentences preserved under extensions of nite structures. 1 Introduction Inductive denitions by positive existential formulae have rst been studied in generalized recursion theory (see e.g. [Acz77]). Chand...