# One-dimensional guarded fragments

## TL;DR

This paper introduces one-dimensional restrictions of the guarded fragment and tri-guarded fragment, analyzing their model properties and computational complexity, showing that these restrictions lead to more tractable decision problems.

## Contribution

It defines and studies GF1 and TGF1, new fragments with restricted quantification, establishing their decidability, model properties, and complexity results, extending the understanding of guarded fragments.

## Key findings

- GF1 has an exponential model property.
- Satisfiability for GF1 is NExpTime-complete.
- TGF1 is decidable with TwoExpTime-complete satisfiability.

## Abstract

We call a first-order formula one-dimensional if its every maximal block of existential (universal) quantifiers leaves at most one variable free. We consider the one-dimensional restrictions of the guarded fragment, GF, and the tri-guarded fragment, TGF, the latter being a recent extension of GF in which quantification for subformulas with at most two free variables need not be guarded, and which thus may be seen as a unification of GF and the two-variable fragment, FO2. We denote the resulting formalisms, resp., GF1, and TGF1. We show that GF1 has an exponential model property and NExpTime-complete satisfiability problem (that is, it is easier than full GF). For TGF1 we show that it is decidable, has the finite model property, and its satisfiability problem is TwoExpTime-complete (NExpTime-complete in the absence of equality). All the above-mentioned results are obtained for signatures with no constants. We finally discuss the impact of their addition, observing that constants do not spoil the decidability but increase the complexity of the satisfiability problem.