<p>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 <InlineEquation ID="IEq1"> <EquationSource Format="TEX">\(LC = K + (p \rightarrow q) \vee (q \rightarrow p)\)</EquationSource> <EquationSource Format="MATHML"><math> <mrow> <mi>L</mi> <mi>C</mi> <mo>=</mo> <mi>K</mi> <mo>+</mo> <mo stretchy="false">(</mo> <mi>p</mi> <mo stretchy="false">→</mo> <mi>q</mi> <mo stretchy="false">)</mo> <mo>∨</mo> <mo stretchy="false">(</mo> <mi>q</mi> <mo stretchy="false">→</mo> <mi>p</mi> <mo stretchy="false">)</mo> </mrow> </math></EquationSource> </InlineEquation>. The frames for <i>LC</i> are those partial orders in which every principal upper cone is linearly ordered – we call such orders postlinear and denote by <i>PL</i> 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 <i>PL</i> are decidable.</p>

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Correspondence Problems for Classes of Postlinear Orders

  • Grigor Kolev,
  • 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)\) L C = K + ( p q ) ( q 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.