Positive first-order logic on words

TL;DR

This paper investigates a fragment of first-order logic on finite words with positive monadic predicates, revealing limitations in definability and undecidability issues, and illustrating the failure of Lyndon's preservation theorem on finite structures.

Contribution

It introduces the FO+ fragment, demonstrates its limitations, and proves the undecidability of FO+ definability for regular languages, highlighting fundamental logical constraints.

Findings

Existence of FO-definable languages monotone in predicates but not in FO+

Lyndon's preservation theorem fails on finite structures

Decidability of FO+ definability for regular languages is impossible

Abstract

We study FO+, a fragment of first-order logic on finite words, where monadic predicates can only appear positively. We show that there is a 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+.