License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CSL.2016.36
URN: urn:nbn:de:0030-drops-65765
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2016/6576/
Go to the corresponding LIPIcs Volume Portal

Kolodziejczyk, Leszek Aleksander ; Michalewski, Henryk ; Pradic, Pierre ; Skrzypczak, Michal

The Logical Strength of Büchi's Decidability Theorem

pdf-format:
LIPIcs-CSL-2016-36.pdf (0.6 MB)

Abstract

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.

BibTeX - Entry

@InProceedings{kolodziejczyk_et_al:LIPIcs:2016:6576,
  author =	{Leszek Aleksander Kolodziejczyk and Henryk Michalewski and Pierre Pradic and Michal Skrzypczak},
  title =	{{The Logical Strength of B{\"u}chi's Decidability Theorem}},
  booktitle =	{25th EACSL Annual Conference on Computer Science Logic (CSL 2016)},
  pages =	{36:1--36:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-022-4},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{62},
  editor =	{Jean-Marc Talbot and Laurent Regnier},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2016/6576},
  URN =		{urn:nbn:de:0030-drops-65765},
  doi =		{10.4230/LIPIcs.CSL.2016.36},
  annote =	{Keywords: nondeterministic automata, monadic second-order logic, B{\"u}chi's theorem, additive Ramsey's theorem, reverse mathematics}
}

Keywords: nondeterministic automata, monadic second-order logic, Büchi's theorem, additive Ramsey's theorem, reverse mathematics
Collection: 25th EACSL Annual Conference on Computer Science Logic (CSL 2016)
Issue Date: 2016
Date of publication: 29.08.2016

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI