## Abstract

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.

%

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.

Original language | English |
---|---|

Title of host publication | Advances in Modal Logic |

Publication status | Accepted/In press - 26 Aug 2018 |

### Publication series

Name | Advances in Modal Logic |
---|---|

Publisher | College Publications |