Positive first-order logic on words

I will present FO+, a restriction of first-order logic where the alphabet is partially ordered, and letters are required to appear positively. 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 FO+? On general structures, Lyndon’s theorem gives such a characterization for monotone FO, 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 see that FO+-definability is undecidable for regular languages on ordered alphabets.

Authors

• Denis Kuperberg

Keywords

No keywords are indexed for this paper.