Finite Model Theory of the Triguarded Fragment and Related Logics

TL;DR

This paper investigates the finite model property of the Triguarded Fragment (TGF), establishing tight bounds and complexity results, and extends these findings to related guarded fragments with transitive guards.

Contribution

It proves the finite model property for TGF with a tight doubly exponential bound and determines the complexity of finite satisfiability for related guarded fragments.

Findings

TGF has the finite model property with a tight doubly exponential bound.

Finite satisfiability of TGF is N2ExpTime-complete.

Finite satisfiability of guarded fragments with transitive guards is 2ExpTime-complete.

Abstract

The Triguarded Fragment (TGF) is among the most expressive decidable fragments of first-order logic, subsuming both its two-variable and guarded fragments without equality. We show that the TGF has the finite model property (providing a tight doubly exponential bound on the model size) and hence finite satisfiability coincides with satisfiability known to be N2ExpTime-complete. Using similar constructions, we also establish 2ExpTime-completeness for finite satisfiability of the constant-free (tri)guarded fragment with transitive guards.