On Finite Satisfiability of the Guarded Fragment with Equivalence or Transitive Guards

摘要

The guarded fragment of first-order logic, GF, enjoys the finite model property, so the satisfiability and the finite satisfiability problems coincide.We are concerned with two extensions of the two-variable guarded fragment that do not possess the finite model property, namely, GF~2 with equivalence and GF~2 with transitive guards. We prove that in both cases every finitely satisfiable formula has a model of at most double exponential size w.r.t. its length.To obtain the result we invent a strategy of building finite models that are formed from a number of multidimensional grids placed over a cylindrical surface. The construction yields a 2Nexptime-upper bound on the complexity of the finite satisfiability problem for these fragments. For the case with equivalence guards we improve the bound to 2Exptime.