
Our concern is the completeness problem for spilogics, 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, spilogics have two natural semantics:
meetsemilattices with monotone operators providing Birkhoffstyle calculi, and
firstorder 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 spilogic.

We investigate the satisfiability problem for Horn fragments of the
HalpernShoham 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 twovariable
firstorder 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 twovariable firstorder 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
insertionerror 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.

Firstorder temporal logics are notorious for their bad computational
behaviour. It is known that even the twovariable monadic fragment is highly
undecidable over various linear timelines, and over branching time even
onevariable fragments might be undecidable. However, there have been several
attempts on finding wellbehaved fragments of firstorder temporal logics and
related temporal description logics, mostly either by restricting the available
quantifier patterns, or considering subBoolean languages. Here we analyse
seemingly `mild' extensions of decidable onevariable fragments with counting
capabilities, interpreted in models with constant, decreasing, and expanding
firstorder 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 byproduct, 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 gridlike 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 firstorder
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.