Decidable and undecidable problems for modal definability and first-order definability

The core of our talk will be Chagrova's Theorem about modal definability of given elementary conditions. Its proof is based on the undecidability of a variant of the halting problem concerning Minsky machines. It cannot be easily repeated for showing that, with respect to different classes of frames, the problem of deciding the modal definability of given elementary conditions is undecidable too. We will give a new proof of Chagrova's Theorem. We will also give the proofs of new variants of Chagrova's Theorem. In particular, we will study modal correspondence theory in the class of all Euclidean frames by showing that with respect to this class of frames, every modal formula is first-order definable and the problem of deciding the modal definability of given elementary conditions is undecidable. Finally, we will study modal correspondence theory in the class of all partitions by showing that with respect to this class of frames, every modal formula is first-order definable and the problem of deciding the modal definability of given elementary conditions is PSPACE-complete.