The bimodal logic of commuting difference operators is decidable
Christopher Hampson · Research Portal (King's College London) · 2018
In this paper, we show that the bimodal logic of two commuting difference operators [Diff,Diff] is decidable (in N2ExpTime), despite lacking the finite model property and thereby remaining impervious to standard filtration techniques. % The proof of decidability involves an exponential-time reduction from the satisfiability problem of the commutator [Diff,Diff] to that of the product logic Diff x Diff, via an intermediate quasimodel construction. % To the best of the author's knowledge, this marks the first example of a (non-trivial) reduction between a commutator [L_h,L_v] and its respective product logic L_h x L_v, where the two logics do not coincide. By adapting this same technique, we are able to establish the finite model property for [S5,Diff], without recourse to standard filtration techniques that break down for logics that are not Horn-axiomatizable, such as that of the difference operator.