首页    期刊浏览 2024年11月24日 星期日
登录注册

文章基本信息

  • 标题:The Logical Strength of Büchi's Decidability Theorem
  • 本地全文:下载
  • 作者:Leszek Aleksander Kolodziejczyk ; Henryk Michalewski ; Pierre Pradic
  • 期刊名称:LIPIcs : Leibniz International Proceedings in Informatics
  • 电子版ISSN:1868-8969
  • 出版年度:2016
  • 卷号:62
  • 页码:36:1-36:16
  • DOI:10.4230/LIPIcs.CSL.2016.36
  • 出版社:Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
  • 摘要:We study the strength of axioms needed to prove various results related to automata on infinite words and Büchi's theorem on the decidability of the MSO theory of (N, less_or_equal). We prove that the following are equivalent over the weak second-order arithmetic theory RCA: 1. Büchi's complementation theorem for nondeterministic automata on infinite words, 2. the decidability of the depth-n fragment of the MSO theory of (N, less_or_equal), for each n greater than 5, 3. the induction scheme for Sigma^0_2 formulae of arithmetic. Moreover, each of (1)-(3) is equivalent to the additive version of Ramsey's Theorem for pairs, often used in proofs of (1); each of (1)-(3) implies McNaughton's determinisation theorem for automata on infinite words; and each of (1)-(3) implies the "bounded-width" version of König's Lemma, often used in proofs of McNaughton's theorem.
  • 关键词:nondeterministic automata; monadic second-order logic; B{\"u
国家哲学社会科学文献中心版权所有