Tinko Tinchev

We examine the definability and correspondence problems between the first-order language of order and the propositional language when given intuitionistic Kripke semantics. Our results are concerning classes of frames for the superintuitionistic logic $$LC = K + (p \rightarrow q) \vee (q \rightarrow p)$$. The frames for _LC_ are those partial orders in which every principal upper cone is linearly ordered – we call such orders postlinear and denote by _PL_ the class of all postlinear orders. We prove that the monadic second-order theory of the class of countable postlinear orders is decidable and consequently that the definability and correspondence problems modulo finitely axiomatizable subclasses of _PL_ are decidable.

In this paper we investigate several extensions of the first order-language with finitely many binary relations. The most interesting of the studied extensions appears to be the monadic second-order one. We show that the extended languages have the same expressive power as the first-order language over the class of all relational structures of equivalence relations in local agreement by providing appropriate translation of formulae. The decidability of the considered extensions over the above mentioned class of structures is also shown.

The aim of this paper is to give new kinds of modal logics suitable for reasoning about regions in discrete spaces. We call them dynamic logics of the region-based theory of discrete spaces. These modal logics are linguistic restrictions of propositional dynamic logic with the global diamond E. Their formulas are equivalent to Boolean combinations of modal formulas like E(A ∧ ⟨α⟩ B) where A and B are Boolean terms and α is a relational term. Examining what we can say about dynamic models when we use formulas to describe them, we successively address the axiomatization/completeness issue and the decidability/complexity issue of our dynamic logics of the region-based theory of discrete spaces.