THE EHRENFEUCHT-FRAISSE GAMES FOR TRANSITIVE CLOSURE

We present in this paper Ehrenfeucht-Fraisse games for the transitive closure logics DTC, TC and ATC. Although the existence of such games for logics with generalized quantifiers was known before, the exact formulation of these games for the predicate transformers arising from various transitive-closure-like operations is new. The games are sound and complete both for finite and infinite models. Combined with well known theorems of Fagin and Immerman these games shed new light on a model theoretic interpretation of the separability of the complexity classes L, NL, P and NP. We discuss this perspective in detail with two examples CLIQUE and HAMILTONIAN by showing that considered as ordered graphs neither of these is definable in monadic second order logic, and hence also not in any transitive closure logic where the predicate transformers are restricted to binary relations.