Positive First-order Logic on Words

Denis Kuperberg (1, 2, 3, 4)

1 CNRS - Centre National de la Recherche Scientifique
2 LIP - Laboratoire de l'Informatique du Parallélisme
3 ENS de Lyon - École normale supérieure de Lyon
4 PLUME - Preuves et Langages

We study FO + , a fragment of first-order logic on finite words, where monadic predicates can only appear positively. We show that there is an FO-definable language that is monotone in monadic predicates but not definable in FO +. This provides a simple proof that Lyndon's preservation theorem fails on finite structures. We additionally show that given a regular language, it is undecidable whether it is definable in FO + .

Domaines: Logique en informatique [cs.LO]; Logique [math.LO]

Denis Kuperberg. Positive First-order Logic on Words. 2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), Jun 2021, Rome, France. pp.1-13, ⟨10.1109/LICS52264.2021.9470602⟩. ⟨hal-03375096⟩