Existential second-order logic and modal logic with quantified accessibility relations

详细信息    查看全文

• 作者：Lauri Hella¹ ; ^{lauri.hella@uta.fi" class="auth_mail" title="E-mail the corresponding author} ; Antti Kuusisto ; ^{antti.j.kuusisto@gmail.com" class="auth_mail" title="E-mail the corresponding author}
• 关键词：Existential second-order logic ; Modal logic ; Finite model theory
• 刊名：Information and Computation
• 出版年：2016
• 出版时间：April 2016
• 年：2016
• 卷：247
• 期：Complete
• 页码：217-234
• 全文大小：489 K

文摘

This article investigates the role of arity   of second-order quantifiers in existential second-order logic, also known as 33c6ea47edb2">${\mathrm{\Sigma }}_1^1$. We identify fragments L of 33c6ea47edb2">${\mathrm{\Sigma }}_1^1$ where second-order quantification of relations of arity k>1$k>1$ is (nontrivially) vacuous in the sense that each formula of L can be translated to a formula of (a fragment of) monadic  33c6ea47edb2">${\mathrm{\Sigma }}_1^1$. Let polyadic Boolean modal logic with identity   (c8096c91708cd4f7a8c4556305ae4" title="Click to view the MathML source">PBML⁼${\mathrm{PBML}}^{=}$) be the logic obtained by extending standard polyadic multimodal logic with built-in identity modalities and with constructors that allow for the Boolean combination of accessibility relations. Let ${\mathrm{\Sigma }}_1^1({\mathrm{PBML}}^{=})$ be the extension of c8096c91708cd4f7a8c4556305ae4" title="Click to view the MathML source">PBML⁼${\mathrm{PBML}}^{=}$ with existential prenex quantification of accessibility relations and proposition symbols. The principal result of the article is that ${\mathrm{\Sigma }}_1^1({\mathrm{PBML}}^{=})$ translates into monadic  33c6ea47edb2">${\mathrm{\Sigma }}_1^1$. As a corollary, we obtain a variety of decidability results for multimodal logic. The translation can also be seen as a step towards establishing whether every property of finite directed graphs expressible in ${\mathrm{\Sigma }}_1^1({\mathrm{FO}}^2)$ is also expressible in monadic 33c6ea47edb2">${\mathrm{\Sigma }}_1^1$. This question was left open in the 1999 paper of Grädel and Rosen in the 14th Annual IEEE Symposium on Logic in Computer Science.