• Our concern is the completeness problem for spi-logics, that is, sets of implications between strictly positive formulas built from propositional variables, conjunction and modal diamond operators. Originated in logic, algebra and computer science, spi-logics have two natural semantics: meet-semilattices with monotone operators providing Birkhoff-style calculi, and first-order relational structures (aka Kripke frames) often used as the intended structures in applications. Here we lay foundations for a completeness theory that aims to answer the question whether the two semantics define the same consequence relations for a given spi-logic.
  • We investigate the satisfiability problem for Horn fragments of the Halpern-Shoham interval temporal logic depending on the type (box or diamond) of the interval modal operators, the type of the underlying linear order (discrete or dense), and the type of semantics for the interval relations (reflexive or irreflexive). For example, we show that satisfiability of Horn formulas with diamonds is undecidable for any type of linear orders and semantics. On the contrary, satisfiability of Horn formulas with boxes is tractable over both discrete and dense orders under the reflexive semantics and over dense orders under the irreflexive semantics, but becomes undecidable over discrete orders under the irreflexive semantics. Satisfiability of binary Horn formulas with both boxes and diamonds is always undecidable under the irreflexive semantics.
  • In the propositional modal (and algebraic) treatment of two-variable first-order logic equality is modelled by a `diagonal' constant, interpreted in square products of universal frames as the identity (also known as the `diagonal') 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.
  • First-order temporal logics are notorious for their bad computational behaviour. It is known that even the two-variable monadic fragment is highly undecidable over various linear timelines, and over branching time even one-variable fragments might be undecidable. However, there have been several attempts on finding well-behaved fragments of first-order temporal logics and related temporal description logics, mostly either by restricting the available quantifier patterns, or considering sub-Boolean languages. Here we analyse seemingly `mild' extensions of decidable one-variable fragments with counting capabilities, interpreted in models with constant, decreasing, and expanding first-order domains. We show that over most classes of linear orders these logics are (sometimes highly) undecidable, even without constant and function symbols, and with the sole temporal operator `eventually'. We establish connections with bimodal logics over 2D product structures having linear and `difference' (inequality) component relations, and prove our results in this bimodal setting. We show a general result saying that satisfiability over many classes of bimodal models with commuting linear and difference relations is undecidable. As a by-product, we also obtain new examples of finitely axiomatisable but Kripke incomplete bimodal logics. Our results generalise similar lower bounds on bimodal logics over products of two linear relations, and our proof methods are quite different from the proofs of these results. Unlike previous proofs that first `diagonally encode' an infinite grid, and then use reductions of tiling or Turing machine problems, here we make direct use of the grid-like structure of product frames and obtain undecidability by reductions of counter (Minsky) machine problems.
  • There are two known general results on the finite model property (fmp) of commutators [L,L'] (bimodal logics with commuting and confluent modalities). If L is finitely axiomatisable 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 have the fmp. On the negative side, if both L and L' are determined by transitive frames and have frames of arbitrarily large depth, then [L,L'] 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 generalise to universally axiomatisable component logics, and even commutators without `transitive' components such as [K.3,K] can lack the fmp. We also generalise 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.3xS5. We also show cases when already half of commutativity is enough to force infinite frames.