Positive First-order Logic on Words and Graphs

TL;DR

This paper investigates the properties of positive first-order logic on words and graphs, revealing limitations in definability, the failure of Lyndon's theorem on finite structures, and undecidability results for FO+ language classification.

Contribution

It introduces FO+ as a positive fragment of first-order logic, demonstrates its limitations, and extends the analysis to finite graphs, providing new insights into definability and decidability issues.

Findings

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

Failure of Lyndon's preservation theorem on finite structures

Undecidability of FO+ definability for regular languages

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 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 lift this example language to finite graphs, thereby providing a new result of independent interest for FO-definable graph classes: negation might be needed even when the class is closed under addition of edges. We finally show that the problem of whether a given regular language of finite words is definable in FO+ is undecidable.