Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Positive and monotone fragments of FO and LTL

Denis Kuperberg, Quentin Moreau

TL;DR

An example of an FO-definable monotone language on one predicate, that is not FO+-definable, is exhibited, refining the example from [Kuperberg 2023] with 3 predicates, and it is shown that such a counter-example cannot be FO2-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.

Positive and monotone fragments of FO and LTL

TL;DR

An example of an FO-definable monotone language on one predicate, that is not FO+-definable, is exhibited, refining the example from [Kuperberg 2023] with 3 predicates, and it is shown that such a counter-example cannot be FO2-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.

Paper Structure

This paper contains 22 sections, 20 theorems, 16 equations.

Table of Contents

  1. Introduction
  2. FO and LTL
  3. First-order logics
  4. Temporal logics
  5. Logical equivalences
  6. Equivalences to FO+
  7. Equivalences in fragments of FO+
  8. Characterisation of monotonicity
  9. Characterisation by monoids
  10. An algorithm to decide monotonicity
  11. Semantic and syntactic monotonicity
  12. Refinement of the counter-example in the general case
  13. Using the between predicate
  14. Only one unary predicate
  15. Stability through monotone closure
  16. ...and 7 more sections

Key Result

Proposition 8

$\mathrm{FO}^+$ formulas are monotone in unary predicates, i.e. if a model $(u,\nu)$ satisfies a formula $\varphi$ of $\mathrm{FO}^+$, and $u \leq_{(\Sigma)^*} v$, then $(v,\nu)$ satisfies $\varphi$.

Theorems & Definitions (53)

  • Definition 1
  • Definition 2
  • Example 3
  • Remark 4
  • Definition 5
  • Definition 6
  • Definition 7
  • Proposition 8: PFO
  • Definition 9
  • Example 10
  • ...and 43 more