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 p…
Read moreWe 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.
