Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

The Finite Satisfiability Problem for Two-Variable, First-Order Logic with one Transitive Relation is Decidable

Ian Pratt-Hartmann

TL;DR

The paper resolves the finite satisfiability problem for the two-variable first-order logic with a single distinguished transitive relation by a sequence of reductions that progressively replace the transitive predicate with a structure of partial orders. First, it analyzes the unary fragment with a single partial order, establishing a doubly exponential finite-model property and a $2-\\text{NExpTime}$ bound. It then extends the result to the full two-variable logic with one partial order, using spread normal form to reduce to the unary fragment and obtain a $2-\\text{NExpTime}$ upper bound. Finally, it handles the general transitive relation by compressing cliques into a diatom framework, reducing to a $\\mathcal{L}^21\hbox{PO}$ problem with an exponential blowup in the signature, which yields a triply exponential bound for FinSat($\\mathcal{L}^21\hbox{T}$). Together, these results place tight complexity bounds on finite satisfiability for the main logics studied and give a roadmap for related two-variable fragments with semantic constraints.

Abstract

We consider the two-variable fragment of first-order logic with one distinguished binary predicate constrained to be interpreted as a transitive relation. The finite satisfiability problem for this logic is shown to be decidable, in triply exponential non-deterministic time. The complexity falls to doubly exponential non-deterministic time if the distinguished binary predicate is constrained to be interpreted as a partial order.

The Finite Satisfiability Problem for Two-Variable, First-Order Logic with one Transitive Relation is Decidable

TL;DR

The paper resolves the finite satisfiability problem for the two-variable first-order logic with a single distinguished transitive relation by a sequence of reductions that progressively replace the transitive predicate with a structure of partial orders. First, it analyzes the unary fragment with a single partial order, establishing a doubly exponential finite-model property and a bound. It then extends the result to the full two-variable logic with one partial order, using spread normal form to reduce to the unary fragment and obtain a upper bound. Finally, it handles the general transitive relation by compressing cliques into a diatom framework, reducing to a problem with an exponential blowup in the signature, which yields a triply exponential bound for FinSat(). Together, these results place tight complexity bounds on finite satisfiability for the main logics studied and give a roadmap for related two-variable fragments with semantic constraints.

Abstract

We consider the two-variable fragment of first-order logic with one distinguished binary predicate constrained to be interpreted as a transitive relation. The finite satisfiability problem for this logic is shown to be decidable, in triply exponential non-deterministic time. The complexity falls to doubly exponential non-deterministic time if the distinguished binary predicate is constrained to be interpreted as a partial order.

Paper Structure

This paper contains 9 sections, 37 theorems, 59 equations, 5 figures.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Unary two-variable logic with one partial order
  4. Basic formulas
  5. Factorizations
  6. Reducing the number of blocks
  7. Reducing the size of blocks
  8. Two-variable logic with one partial order
  9. Two-variable logic with one transitive relation

Key Result

Lemma 1

Let $\varphi$ be an $\mathcal{L}^2$-formula. There exists a standard normal-form $\mathcal{L}^2$-formula $\varphi'$ such that: (i)$\models \varphi' \rightarrow \varphi$; (ii) every model of $\varphi$ can be expanded to a model of $\varphi'$; and (iii)$\lVert \varphi' \rVert$ is bounded by a polynomi

Figures (5)

  • Figure 1: A linear order on the elements satisfying $p$, and an anti-chain on the elements satisfying $q$.
  • Figure 2: Factorization of a finite typed partial order over 1-types $\pi_1, \dots, \pi_N$, with cut $\chi$, showing $\mathbf{B}^\times$ (thick lines), and $F^+(\chi)$ and $F^-(\chi)$ (shading).
  • Figure 3: Proof of Lemma \ref{['lma:cutBlockOrderPreserve']}: the claim that $A \approx^* B'$ in the case where $A$ is below $\chi$.
  • Figure 4: Construction of the structure $\mathfrak{A}_{i+1}$ (Lemma \ref{['lma:betterCopyLemma']}), where $a \in B_{i+1}$, $b \in B_j$, and $j \leq i$.
  • Figure 5: The function $\kappa$ mapping $\hat{a} \cup \hat{a}'$ to the reference diatom $\mathfrak{D} = \mathfrak{D}_{\hat{a},\hat{a}'}$. The construction of $\kappa$ composes the function $\iota$ mapping $\hat{a}$ and $\hat{a}'$ to their respective reference cells $\mathfrak{C} = \mathfrak{C}_{\hat{a}}$ and $\mathfrak{C}' = \mathfrak{C}_{\hat{a}'}$ with the functions $\epsilon: \mathbf{C} \rightarrow \mathbf{E}$ and $\epsilon': \mathbf{C} \rightarrow \mathbf{E}'$.

Theorems & Definitions (70)

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