The decision problem of modal product logics with a diagonal, and faulty counter machines

TL;DR

This paper investigates the complexity of product modal logics with a diagonal constant, revealing that adding such a diagonal can cause a shift from decidability to high undecidability, using counter machine encodings.

Contribution

It demonstrates that incorporating a diagonal in product modal logics can significantly increase complexity, including undecidability, and introduces a novel method using faulty counter machine computations.

Findings

Adding a diagonal can cause a jump from decidable to undecidable logics.

Faulty counter machine encodings can simulate reliable computations.

The approach links modal logic complexity with counter machine problems.

Abstract

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.