Ever since rst-order logic (FOL) was found to have an undecidable satis ability problem, researchers have attempted to identify expressive yet decidable fragments of FOL and pinpoint their complexity. In many cases, such fragments embed propositional modal logic as well as many description logics. Two of the most prominent examples in this regard are FO2 (the two-variable fragment ) and GF (the guarded fragment ). For FO2, decidability is retained through reducing the number of available variables to 2, essentially restricting expressivity to independent pairwise interactions between domain elements. Its satis ability problem is NExpTime-complete [5]. For GF, which owes its decidability to the restricted \guarded" use of quanti ers, the problem is 2ExpTime-complete [4]. Both FO2 and GF possess the nite model property (FMP), meaning that any satis able sentence has a nite model. For satis able FO2 sentences, models of at most exponential size in the sentence exist [5]; for GF, the tight bound on the size of minimal models is doubly exponential [1]. In an attempt to unify FO2 and GF toward an even more expressive decidable FOL fragment, the triguarded fragment (TGF) was introduced [9], extending prior results [6]. TGF brings a new quality, as it allows one to express properties expressible in neither FO2 nor GF. In particular it embeds Godel's class, consisting of prenex sentences of the shape 9x8y1y29z' (formally we need to replace the variables from x by constants and add a dummy guard for 9z). Thus, the price to pay for retaining decidability is that equality needs to be disallowed, as Godel's class with equality is undecidable [2]. Checking satis ability of TGF is N2ExpTime-complete, dropping to 2ExpTime when disallowing constants { as opposed to FO2 and GF, where presence or absence of constants does not make a di erence, complexity-wise { and to NExpTime if the arity of predicates is bounded. One central question left wide open in the original work on TGF [9] is if TGF has the FMP. In that paper, it is noted that neither technique used for establishing the FMP for FO2 and GF seems to directly lend itself for solving the question for TGF, yet it is conjectured that the FMP holds. Indeed, one of our core contributions is to answer this open question in the positive. Let us brie y outline our approach.
For convenience, we work with the equivalent logic GFU, the guarded fragment with universal role. We assume that signatures for GFU always contain the distinguished binary relation symbol U. GFU sentences are then de ned precisely like GF sentences, but the set of admissible models is restricted to those which interpret U as the universally true relation. Structures interpreting U in this way will be called U-biquitous structures. It is not di cult to see that TGF and GFU have the same expressive power modulo the extra predicate U.
As typical for decidable fragments of rst-order logic we introduce a normal
form for TGF formulas, similar to those used, e.g., for GF [
Given a satis able GFU normal form sentence ', we take its (possibly in nite) U-biquitous model A and construct a nite U-biquitous model A0 of ' as follows (for simplicity, we consider here the case without constants; adding them is routine): 1. Extend ' by conjuncts saying that: exactly the 1-types from A are realized; for any two 1-types from A, there are U-connected representatives; U holds between any pair of elements co-occurring in any relation. The resulting normal form sentence ' is still guarded and still satis es A j= ' . 2. Use the FMP for GF to obtain a nite (yet non-ubiquitous) model C of ' . 3. Obtain A0 j= ' as 125 jCj2-fold disjoint union of C with itself. View A0 as a 5jCj 5jCj table whose each cell contains a copy of the 5-fold disjoint union of C with itself. The elements in each cell are numbered from 1 to 5jCj. 4. U-saturation: Obtain A1; A2; : : : by iteratively picking a pair a; b of yet nonU-connected elements, connecting them, and adjoining them to one of the copies of C. This is done using an appropriate pair of connected elements as template (hence maintaining ' -modelhood). Designing a strategy allowing one to perform this step without con icts is quite challenging. In our solution, the numbers of a and b in their cells B0, B00 determine a cell B, and the coordinates of B0 and B00 in the table are used to choose a particular copy of C in B to which a and b are adjoined. 5. As the number of elements remains constant, the procedure terminates and yields a U-biquitous An = A0.
We also consider a scenario where some distinguished binary symbols have to
be interpreted as transitive relations, capturing this way, e.g., some description
logics from the family S. One needs to be careful here, since both FO2 and GF
become undecidable under this scenario [
Results for the nite model case are less extensive: so far, only nite
satisability of the two-variable variant GF2+TG of GF with transitive guards was
shown to be decidable and 2ExpTime-complete [
In the current paper we are able to show that (at least in the absence of
constants) the nite satis ability problems for GF and TGF with transitive
guards are decidable. Our approach incorporates some ideas from the
abovedescribed nite model construction for satis able TGF sentences and some other
concepts, in particular calling as a subprocedure the small-model construction
for GF2+TG from [
All our results come with tight complexity bounds and tight bounds on the size of minimal models. Summarising: Theorem 1. TGF has the nite model property; every satis able TGF sentence has a nite model of size bounded doubly exponentially in its length. Hence, satis ability and nite satis ability for TGF coincide and are N2ExpTimecomplete if constants are admitted and 2 ExpTime-complete otherwise. Theorem 2. Every nitely satis able sentence in (constant-free) GF or TGF with transitive guards has a model of size bounded doubly exponentially in its length. The nite satis ability problems for (constant-free) GF and TGF with transitive guards are 2 ExpTime-complete.
Decidability and complexity of nite satis ability of GF and TGF with transitive guards with constant is left open.