Hierarchies in transitive closure logic, stratified Datalog and infinitary logic (Q1919531)

By results due to Immerman we know that the fragment FO(posTC) of transitive closure logic FO(TC) which only allows positive applications of the TC operator has the same expressive power as FO(TC) on ordered finite structures. The main theorem of the present paper implies that FO(posTC) is not closed under negation -- and hence is different from FO(TC) -- on arbitrary finite structures. This result is obtained by embedding FO(posTC) and FO(TC) in \(L^\omega_{\infty \omega}\) and by showing a hierarchy theorem for prefix classes \(L^\omega_{\infty \omega}\). (This is achieved by using appropriate extensions of the Ehrenfeucht-Fraïssé games.) Among further applications, the authors derive a hierarchy theorem for transitive closure logic.