Positive first-order logic on words.

I will present FO+, a restriction of first-order logic where letters are required to appear positively, and the alphabet is partially ordered (for instance by inclusion order if letters are sets of atoms). Restricting predicates to appear positively is for instance very natural when considering logics with fixpoints. Here we will ask a syntax versus semantics question: FO+-definable languages are monotone in the letters, but can every FO-definable monotone language be defined in this way? On general structures, Lyndon's theorem gives such a syntax/semantics equivalence for monotone first-order formulas, but it is known to fail on finite structures. We will see that it also fails on finite words, giving a much simpler proof for the failure of Lyndon's theorem on finite structures. Finally we will look at whether FO+-definability is decidable for regular languages.