Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Positive First-order Logic on Words and Graphs

Denis Kuperberg

TL;DR

This work analyzes the positive fragment FO^+ of first-order logic on finite words, showing that Lyndon’s preservation theorem fails for finite structures by constructing a monotone, FO-definable language K that is not FO^+-definable. The authors develop FO^+-specific Ehrenfeucht-Fraïssé games (EF^+), prove FO^+-definability for K via multiple viewpoints (minimal DFA, syntactic monoid, and explicit FO formulas), and demonstrate how K can be encoded in finite graphs to obtain new results about FO-definable graph classes that are monotone under edge addition but require negation in some edge relations. They further establish undecidability of FO^+-definability for regular languages by a reduction from the Turing Machine Mortality problem, constructing languages L_M whose FO^+-definability exactly mirrors whether a given TM is mortal. Overall, the paper advances understanding of positive logical fragments, delineates the expressive gap between FO and FO^+ on finite structures, and connects automata/theory of regular languages with model-theoretic preservation theorems.

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.

Positive First-order Logic on Words and Graphs

TL;DR

This work analyzes the positive fragment FO^+ of first-order logic on finite words, showing that Lyndon’s preservation theorem fails for finite structures by constructing a monotone, FO-definable language K that is not FO^+-definable. The authors develop FO^+-specific Ehrenfeucht-Fraïssé games (EF^+), prove FO^+-definability for K via multiple viewpoints (minimal DFA, syntactic monoid, and explicit FO formulas), and demonstrate how K can be encoded in finite graphs to obtain new results about FO-definable graph classes that are monotone under edge addition but require negation in some edge relations. They further establish undecidability of FO^+-definability for regular languages by a reduction from the Turing Machine Mortality problem, constructing languages L_M whose FO^+-definability exactly mirrors whether a given TM is mortal. Overall, the paper advances understanding of positive logical fragments, delineates the expressive gap between FO and FO^+ on finite structures, and connects automata/theory of regular languages with model-theoretic preservation theorems.

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.
Paper Structure (28 sections, 30 theorems, 11 equations, 8 figures)

This paper contains 28 sections, 30 theorems, 11 equations, 8 figures.

Table of Contents

  1. Introduction
  2. Monotonicity on words
  3. Ordered alphabet
  4. Monotone languages
  5. Positive first-order logic
  6. Syntax and semantics
  7. Properties of $\mathrm{FO}^+$
  8. Ordered Ehrenfeucht-Fraïssé games
  9. A counter-example language
  10. The language $K$
  11. FO-definability of $K$
  12. Syntactic monoid for the language $K$
  13. Defining an FO formula for the language $K$
  14. Undefinability of $K$ in $\mathrm{FO}^+$
  15. Lyndon's Theorem
  16. ...and 13 more sections

Key Result

Lemma 2.4

Given an NFA $\mathcal{B}$, we can compute in time $O(|\mathcal{B}|\cdot|A|)$ an NFA $\mathcal{B}^\uparrow$ for the monotone closure of $L(\mathcal{B})$.

Figures (8)

  • Figure 1: The minimal DFA $\mathcal{A}$ of $K$
  • Figure 2: The syntactic monoid $M$ of $K$
  • Figure 3: A visualization of anchors
  • Figure 4: An example of Duplicator's strategy for $n=3$.
  • Figure 5: A graph of $\mathcal{G}_w$
  • ...and 3 more figures

Theorems & Definitions (76)

  • Definition 2.1
  • Example 2.2
  • Definition 2.3
  • Lemma 2.4
  • proof
  • Theorem 2.5
  • proof
  • Example 3.1
  • Remark 3.2
  • Example 3.3
  • ...and 66 more