Directed Reachability: From Ajtai-Fagin to Ehrenfeucht-Fraïssé Games

Abstract

In 1974 Ronald Fagin proved that properties of structures which are in $\mathcal{N}\mathcal{P}$are exactly the same as those expressible by existential second order sentences, that is sentences of the form $\exists \vec P\phi$, where $\vec P$is a tuple of relation symbols. and φ is a first order formula. Fagin was also the first to study monadic $\mathcal{N}\mathcal{P}$: the class of properties expressible by existential second order sentences where all quantified relations are unary. In their very difficult paper [AF90] Ajtai and Fagin show that directed reachability is not in monadic $\mathcal{N}\mathcal{P}$.

In [AFS97] Ajtai, Fagin and Stockmeyer introduce closed monadic $\mathcal{N}\mathcal{P}$: the class of properties which can be expressed by a kind of monadic second order existential formula, where the second order quantifiers can interleave with first order quantifiers. Among other results they show that directed reachability is expressible by a formula of the form $x$φ, where P and P₁ are unary relation symbols and f is first order. They state the question if this property is in the positive first order closure of monadic $\mathcal{N}\mathcal{P}$, that is if it is expressible by a sentence of the form $\vec Qx\exists \vec P\phi$, where $\vec Qx$is a tuple of first order quantifiers and $\vec P$is a tuple of unary relation symbols.

In this paper we give a negative solution to the problem.