Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

The Fluted Fragment with Transitive Relations

Ian Pratt-Hartmann, Lidia Tendera

TL;DR

The paper analyzes the satisfiability of the fluted fragment $\mathcal{FL}$ extended by transitive relations, clarifying how the finite model property behaves under these extensions. It establishes decidability for the case of a single transitive relation with equality, with complexity bounds that scale with the number of variables ($m$) as $m$-$\text{NExpTime}$ for $\mathcal{FL}^{m}_{=1}T$ and $ (m+1)$-$\text{NExpTime}$ for finite satisfiability, yielding a Tower-complete overall complexity. By contrast, it proves undecidability for two transitive relations with equality ($\mathcal{FL}^{2}_{=2}T$) and for three transitive relations without equality ($\mathcal{FL}^{2}_{}3T$), via grid-tiling reductions that simulate $\mathbb{N}^2$ within the logics. The results illuminate how flutedness interacts with transitivity, delineating a boundary between decidable and undecidable fragments and suggesting directions for future work on the remaining open cases, such as the ${\mathcal{FL}^{2}_{=2}T}$ boundary without equality.

Abstract

We study the satisfiability problem for the fluted fragment extended with transitive relations. The logic enjoys the finite model property when only one transitive relation is available and the finite model property is lost when additionally either equality or a second transitive relation is allowed. We show that the satisfiability problem for the fluted fragment with one transitive relation and equality remains decidable. On the other hand we show that the satisfiability problem is undecidable already for the two-variable fragment of the logic in the presence of three transitive relations (or two transitive relations and equality).

The Fluted Fragment with Transitive Relations

TL;DR

The paper analyzes the satisfiability of the fluted fragment extended by transitive relations, clarifying how the finite model property behaves under these extensions. It establishes decidability for the case of a single transitive relation with equality, with complexity bounds that scale with the number of variables () as - for and - for finite satisfiability, yielding a Tower-complete overall complexity. By contrast, it proves undecidability for two transitive relations with equality () and for three transitive relations without equality (), via grid-tiling reductions that simulate within the logics. The results illuminate how flutedness interacts with transitivity, delineating a boundary between decidable and undecidable fragments and suggesting directions for future work on the remaining open cases, such as the boundary without equality.

Abstract

We study the satisfiability problem for the fluted fragment extended with transitive relations. The logic enjoys the finite model property when only one transitive relation is available and the finite model property is lost when additionally either equality or a second transitive relation is allowed. We show that the satisfiability problem for the fluted fragment with one transitive relation and equality remains decidable. On the other hand we show that the satisfiability problem is undecidable already for the two-variable fragment of the logic in the presence of three transitive relations (or two transitive relations and equality).

Paper Structure

This paper contains 13 sections, 29 theorems, 48 equations, 7 figures, 2 tables.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Variable-free syntax for fluted formulas
  4. Loss of the finite model property
  5. Fluted types and cliques
  6. The decidability of fluted logic with one transitive relation and equality
  7. Basic formulas in ${\mathcal{FL}^{2}_=1\hbox{\rm T}^{u}}$
  8. The logic ${\mathcal{FL}^{2}_={1}\hbox{\rm T}}$
  9. The logic ${\mathcal{FL}^{m}_={1}\hbox{\rm T}}$
  10. Fluted Logic with more Transitive Relations
  11. The case of two transitive relations
  12. The case of three transitive relations
  13. Conclusions

Key Result

Lemma 3

Let $\Gamma$ be a set of fluted $m$-clauses, and $\tau$ a fluted $m$-type over the signature of $\Gamma^\circ$. If $\Gamma^\circ \cup \{\tau\}$ is consistent, then there exists a fluted type $\tau^+$ over the signature of $\Gamma$ such that $\tau^+ \supseteq \tau$ and $\Gamma \cup \{\tau^+\}$ is co

Figures (7)

  • Figure 1: The 'lining up' of variables in the fluted formulas \ref{['eq:eg1']} and \ref{['eq:eg2']}; all quantification is executed on the right-most available column.
  • Figure 2: Infinite chain in models of $\varphi_2$ from Example \ref{['ex:two']}. Pairs $(a_{i},a_{i+1})$ are neither in $\color{blue}{T_1}$ nor in $\color{red}{T_2}$; depicted by dotted lines. Blue and red arrows depict pairs belonging to the transitive relations $\color{blue}{T_1}$ and $\color{red}{T_2}$.
  • Figure 3: Construction of the domain $A$ of $\mathfrak{A}(\mathcal{C})$ for $\mathcal{C}$ a certificate.
  • Figure 4: Intended expansion of the ${\mathbb N}\times{\mathbb N}$ grid with two transitive relations $T_1$ and $T_2$. Edges without arrows represent connections in both direction. Nodes are marked by the indices of the $c_{ij}$s they satisfy.
  • Figure 5: Intended expansion of the ${\mathbb N} \times {\mathbb N}$ grid and the boustrophedon order (thick gray path).
  • ...and 2 more figures

Theorems & Definitions (53)

  • Example 1
  • proof
  • Example 2
  • proof
  • Lemma 3
  • proof
  • Lemma 4
  • Lemma 5
  • proof
  • Lemma 6
  • ...and 43 more