Positive first-order logic on words

In this ongoing work, we investigate a fragment of first-order logic (FO) on words, called positive first-order logic (FO+). This fragment is designed to define only upwards-closed languages with respect to a given partial order on letters, by restricting the letter symbols to appear positively in the formula. It is not clear whether the converse holds: can any FO-definable upwards-closed language be defined in FO+? We show that this is not the case, by giving a counter-example. This example can be used to show that Lyndon’s theorem fails on finite words. Lyndon’s theorem states that on general structures, any FO formula defining a class of structures closed under surjective morphisms is equivalent to a FO+ formula. This theorem was known to fail on finite structures, but our proof strenghtens this result and simplifies its proof, using only finite words instead of a more complex signature. This is joint work with Thomas Colcombet, Amina Doumane, and Sam Van Gool.

Authors

• Denis Kuperberg

Keywords

No keywords are indexed for this paper.