There are two known general results on the finite model property of commutators [L0,L1]. If L is finitely axiomatizable by modal formulas having universal Horn first-order correspondents, then both [L,K] and [L,S5] are determined by classes of frames that admit filtration, and so they have the fmp. On the negative side, if both L0 and L1 are determined by transitive frames and have frames of arbitrarily large depth, then [L0,L1] does not have the fmp. In this paper we show that (...) commutators with a “weakly connected” component often lack the fmp. Our results imply that the above positive result does not generalize to universally axiomatizable component logics, and even commutators without “transitive” components such as [K3,K] can lack the fmp. We also generalize the above negative result to cases where one of the component logics has frames of depth one only, such as [S4.3,S5] and the decidable product logic S4.3×S5. We also show cases when already half of commutativity is enough to force infinite frames. (shrink)

We show that—unlike products of ‘transitive’ modal logics which are usually undecidable—their ‘expanding domain’ relativisations can be decidable, though not in primitive recursive time. In particular, we prove the decidability and the finite expanding product model property of bimodal logics interpreted in two-dimensional structures where one component—call it the ‘flow of time’—is • a finite linear order or a finite transitive tree and the other is composed of structures like • transitive trees/partial orders/quasi-orders/linear orders or only finite such structures expanding (...) over time. The decidability proof is based on Kruskal’s tree theorem, and the proof of non-primitive recursiveness is by reduction of the reachability problem for lossy channel systems. The result is used to show that the dynamic topological logic interpreted in topological spaces with continuous functions is decidable if the number of function iterations is assumed to be finite. (shrink)

In this paper we shall introduce a simple temporal logic suitable for reasoning about the temporal aspects of parallel universes, parallel processes, distributed systems, or multiple agents. We will use a variant of the mosaic method to prove decidability of this logic. We also show that the logic does not have the finite model property. This shows that the mosaic method is sometimes a stronger way of establishing decidability.

In the propositional modal treatment of two-variable first-order logic equality is modelled by a ‘diagonal’ constant, interpreted in square products of universal frames as the identity relation. Here we study the decision problem of products of two arbitrary modal logics equipped with such a diagonal. As the presence or absence of equality in two-variable first-order logic does not influence the complexity of its satisfiability problem, one might expect that adding a diagonal to product logics in general is similarly harmless. We (...) show that this is far from being the case, and there can be quite a big jump in complexity, even from decidable to the highly undecidable. Our undecidable logics can also be viewed as new fragments of first-order logic where adding equality changes a decidable fragment to undecidable. We prove our results by a novel application of counter machine problems. While our formalism apparently cannot force reliable counter machine computations directly, the presence of a unique diagonal in the models makes it possible to encode both lossy and insertion-error computations, for the same sequence of instructions. We show that, given such a pair of faulty computations, it is then possible to reconstruct a reliable run from them. (shrink)

Spatio-temporal logic is a variant of branching temporal logic where one of the so-called causal relations on spacetime plays the role of a time flow. Allowing only rational numbers as space and time co-ordinates, we prove that a first-order spatio-temporal theory over this flow is recursively enumerable if and only if the dimension of spacetime does not exceed 2. The situation is somewhat different compared to the case of real co-ordinates, because we establish that even dimension 2 does not permit (...) recursive enumerability in this case. The proof of the result on rational spacetime involves a more deeper portion of spacetime geometry than the corresponding, more evident result for the real co-ordinates. (shrink)

We solve a major open problem concerning algorithmic properties of products of ‘transitive’ modal logics by showing that products and commutators of such standard logics as K4, S4, S4.1, K4.3, GL, or Grz are undecidable and do not have the finite model property. More generally, we prove that no Kripke complete extension of the commutator [K4,K4] with product frames of arbitrary finite or infinite depth (with respect to both accessibility relations) can be decidable. In particular, if.

We present an extension of the mosaic method aimed at capturing many-dimensional modal logics. As a proof-of-concept, we define the method for logics arising from the combination of linear tense operators with an “orthogonal” S5-like modality. We show that the existence of a model for a given set of formulas is equivalent to the existence of a suitable set of partial models, called mosaics, and apply the technique not only in obtaining a proof of decidability and a proof of completeness (...) for the corresponding Hilbert-style axiomatization, but also in the development of a mosaic-based tableau system. We further consider extensions for dealing with the case when interactions between the two dimensions exist, thus covering a wide class of bundled Ockhamist branching-time logics, and present for them some partial results, such as a non-analytic version of the tableau system. (shrink)