Résumé | I will present FO+, a restriction of first-order logic on words, where letter predicates are required to appear positively. The words considered here are on a "powerset alphabet": predicates a(x) and b(x) can be true simultaneously. We will ask a syntax versus semantics question: FO+-definable languages are monotone in the letters (with respect to inclusion), but can every FO-definable monotone language be expressed in FO+ ? On general structures, Lyndon's theorem gives a positive answer to this question, but it is known to fail on finite structures. We will see that it also fails on finite words, by giving a simple counter-example language. This gives a new proof for the failure of Lyndon's theorem on finite structures, that is much more elementary than previous proofs. Finally we will see that surprisingly, FO+-definability is undecidable for regular languages. |