Positive and monotone fragments of FO and LTL

TL;DR

This paper explores the expressive power of positive fragments of first-order logic and linear temporal logic on finite words, establishing equivalences and limitations of definability within these logical frameworks.

Contribution

It refines previous work by establishing new equivalences between positive FO and LTL fragments, and demonstrates limitations of FO2-definability for certain monotone languages.

Findings

FO+ is equivalent to LTL+ on finite words

FO2+ with/without successor is equivalent to UTL+ with/without next

Certain FO-definable monotone languages are not FO+-definable

Abstract

We study the positive logic FO+ on finite words, and its fragments, pursuing and refining the work initiated in [Kuperberg 2023]. First, we transpose notorious logic equivalences into positive first-order logic: FO+ is equivalent to LTL+ , and its two-variable fragment FO2+ with (resp. without) successor available is equivalent to UTL+ with (resp. without) the "next" operator X available. This shows that despite previous negative results, the class of FO+-definable languages exhibits some form of robustness. We then exhibit an example of an FO-definable monotone language on one predicate, that is not FO+-definable, refining the example from [Kuperberg 2023] with 3 predicates. Moreover, we show that such a counter-example cannot be FO2-definable.