[The talk will take place in room M7 411, 4th floor, turn left when you exit the elevator.]

We will investigate the gap between syntactically and semantically positive first-order logic formulas.

A formula is syntactically positive if it does not contain negated predicates, while it is semantically positive when the class of structures it defines is monotone, i.e. closed under making the predicates true on more tuples.

Starting with finite words, I will present the logic FO+, 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 on the same position x of the word. We will ask a syntax versus semantics question: FO+-definable languages are monotone in the letters, 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 already 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.

We will also study the problem on finite graphs: if a class of finite graphs is FO-definable and closed under edge addition, can it be defined with a negation-free formula ? To our knowledge this was an open question, which we can answer negatively via a suitable encoding of our counter-example language.

Finally, if time permits, we will go back to regular languages of finite words and see that FO+-definability is surprisingly undecidable in this framework.

This talk is based on work published in LICS 2021, with a full version currently submitted to a special issue of LMCS, available on Arxiv.