Christopher Hampson

Undecidable products involving the logic of 'elsewhere'

(Joint work with Agi Kurucz)

The modal logic of 'elsewhere', or the difference operator, Diff is known to be Kripke complete with respect to the class of symmetric, pseudo-transitive frames; frames not too dissimilar to equivalence relations. Indeed the validity problems for both Diff and S5 are in co-NP.

Products logics of the form L x S5 are usually decidable and S5 x S5 even enjoys the finite model property. In contrast, we present some cases where the transition from L x S5 to L x Diff not only increasing the complexity of the validity problem, but in fact introduces undecidability. In addition, we also show that Diff x Diff lacks the finite model property.

The strategy we use for demonstrating undecidability involves a reduction from the non-halting problem for 2-counter Minsky machines, whereas typically, previous strategies in this area have involved Turing machines or grid-tiling problems.