Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Alternating Quantifiers in Uniform One-Dimensional Fragments with an Excursion into Three-Variable Logic

Oskar Fiuk, Emanuel Kieronski

TL;DR

AUF$_1$ extends UF$_1$ by permitting mixed quantifier blocks, and the paper identifies two equality-free subfragments AUF$_1^{-}$ and AUF$_1^{3}$ with the exponential model property and NExpTime-complete satisfiability. It develops satisfaction forests as a core combinatorial tool and provides both constructive and probabilistic proofs of finite models, then extends the three-variable analysis to FO$^3_{-}$, preserving decidability and exponential model bounds. The work clarifies the boundary between decidability and undecidability for higher-arity logics, supplies practical complexity results, and offers techniques potentially useful for extensions of modal and description logics to richer relational contexts.

Abstract

The uniform one-dimensional fragment of first-order logic was introduced a few years ago as a generalization of the two-variable fragment to contexts involving relations of arity greater than two. Quantifiers in this logic are used in blocks, each block consisting only of existential quantifiers or only of universal quantifiers. In this paper we consider the possibility of mixing both types of quantifiers in blocks. We show the finite (exponential) model property and NExpTime-completeness of the satisfiability problem for two restrictions of the resulting formalism: in the first we require that every block of quantifiers is either purely universal or ends with the existential quantifier, in the second we restrict the number of variables to three; in both equality is not allowed. We also extend the second variation to a rich subfragment of the three-variable fragment (without equality) that still has the finite model property and decidable, NExpTime-complete satisfiability.

Alternating Quantifiers in Uniform One-Dimensional Fragments with an Excursion into Three-Variable Logic

TL;DR

AUF extends UF by permitting mixed quantifier blocks, and the paper identifies two equality-free subfragments AUF and AUF with the exponential model property and NExpTime-complete satisfiability. It develops satisfaction forests as a core combinatorial tool and provides both constructive and probabilistic proofs of finite models, then extends the three-variable analysis to FO, preserving decidability and exponential model bounds. The work clarifies the boundary between decidability and undecidability for higher-arity logics, supplies practical complexity results, and offers techniques potentially useful for extensions of modal and description logics to richer relational contexts.

Abstract

The uniform one-dimensional fragment of first-order logic was introduced a few years ago as a generalization of the two-variable fragment to contexts involving relations of arity greater than two. Quantifiers in this logic are used in blocks, each block consisting only of existential quantifiers or only of universal quantifiers. In this paper we consider the possibility of mixing both types of quantifiers in blocks. We show the finite (exponential) model property and NExpTime-completeness of the satisfiability problem for two restrictions of the resulting formalism: in the first we require that every block of quantifiers is either purely universal or ends with the existential quantifier, in the second we restrict the number of variables to three; in both equality is not allowed. We also extend the second variation to a rich subfragment of the three-variable fragment (without equality) that still has the finite model property and decidable, NExpTime-complete satisfiability.
Paper Structure (28 sections, 14 theorems, 40 equations)

This paper contains 28 sections, 14 theorems, 40 equations.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Fragments of logic
  4. Notation, outer-structures and outer-types
  5. Normal form of AUF$_{\mathbf{1}}$.
  6. Diminished alternating uniform one-dimensional fragment
  7. Satisfaction forests
  8. Extracting a satisfaction forest from a model
  9. Satisfaction forests and the existence of finite models
  10. From a model to a satisfaction forest over a small finite domain
  11. Domain
  12. Some simple combinatorics: Extension functions
  13. Construction of a satisfaction forest
  14. Correctness
  15. Complexity of satisfiability
  16. ...and 13 more sections

Key Result

Lemma 2.1

Let $\sigma$ be a purely relational finite signature containing relational symbols of arity at most $\ell$, for some fixed $\ell$. Then the number of all possible $k$-outer-types, for $k \leqslant \ell$, is an exponential function of $|\sigma|$. This holds in particular for the number of $1$-types.

Theorems & Definitions (29)

  • Lemma 2.1
  • Lemma 2.2
  • Lemma 2.3
  • proof
  • Corollary 2.4
  • Theorem 3.1
  • Theorem 3.2
  • Claim 3.3
  • proof
  • Lemma 3.4
  • ...and 19 more