Decidable fragments of first-order temporal logics (Q1591203)

First-order temporal logic extends ordinary first-order logic by the binary temporal operators \({\mathcal S}\) (since) and \({\mathcal U}\) (until). The logic is interpreted using a strict linear order \((W,<)\) and for each \(w\in W\) a first-order structure \(I(w)\) where the underlying domain of the \(I(w)\) as well as the interpretations of constants are the same for each \(w\). The linear order \(W\) models the flow of time; \(I(w)\) varying with \(w\) reflects the idea that meanings of predicates may change over time. Given \(w\in W\) and a formula \(\phi\) with parameters from \(D\), one writes \(w\models \phi\) to mean that \(\phi\) is valid ``at time'' \(w\). One has in particular \(w\models \phi{\mathcal U}\psi\) iff there is \(v>w\) such that \(v\models \phi\) and \(u\models \psi\) for each \(w<u<v\). Likewise, \(w\models \phi{\mathcal S}\psi\) iff there is \(v<w\) such that \(v\models \phi\) and \(u\models \psi\) for each \(v<u<w\). For example, \(\diamondsuit\phi := \top{\mathcal U}\phi\) expresses that \(\phi\) holds at some later time, i.e., eventually, whereas \(\square\phi:=\neg\diamondsuit\neg\phi\) expresses that \(\phi\) holds at all later times, i.e., henceforth. Unfortunately, already the monadic fragment (only unary predicate symbols) as well as the 2-variable fragments (formulas contain at most two distinct variables) are not even recursively enumerable, i.e., there does not exist a recursive axiomatisation of the formulas that are true for some interpretation. This is proved by reduction to the recurrent tiling problem for \({\mathbf N}\times {\mathbf N}\). The situation does not change if one restricts attention to interpretation in finite domains (but over infinite time, e.g., \(W=({\mathbf N},<))\). Notice that the corresponding fragments of pure first-order logic are decidable. The contribution of the paper is that decidability of satisfiability can be regained if a) one restricts the purely first-order part to a decidable fragment and b) one allows at most one free variable in subformulas of temporal operators. For instance, the Barcan formula \(\exists x\diamondsuit\phi \Leftrightarrow\diamondsuit\exists x\phi\) belongs to this fragment. This result is all the more interesting as the considered fragments do not enjoy the finite model property, i.e., there are formulas that are satisfiable (over \((\mathbf N,<)\)) in models with infinite domain only; a case in point is the formula \(\square\exists x(P(x)\wedge\neg(\top {\mathcal S}P(x)))\) expressing that at any time \(P\) contains an element that was not there before (or in the authors' words: ``at every moment someone's starting to get old''). The proof of the decidability result proceeds using finitary descriptions of models (``quasimodels'') in which (the possibly infinite, see above) set of domain elements is replaced by a finite set of types, i.e., deductively closed sets of formulas in one free variable. The existence of quasimodels can be expressed in monadic second-order logic which is decidable by standard results of Büchi and Rabin.