The existential fragment of S1S over element and successor is the co-Buchi languages

Buchi's theorem, in establishing the equivalence between languages definable in S1S over element and < and the omega-regular languages also demonstrated that S1S over element and < is no more expressive than its existential fragment. It is also easy to see that S1S over element and < is equi-expressive with S1S over element and successor. However, it is not immediately obvious whether it is possible to adapt Buchi's argument to establish equivalence between expressivity in S1S over element and successor and its existential fragment. In this paper we show that it is not: the existential fragment of S1S over element and successor is strictly less expressive, and is in fact equivalent to the co-Buchi languages.