1 Search Results for "Kolodziejczyk, Leszek Aleksander"

Document
DOI: 10.4230/LIPIcs.CSL.2016.36
The Logical Strength of Büchi's Decidability Theorem

Authors: Leszek Aleksander Kolodziejczyk, Henryk Michalewski, Pierre Pradic, and Michal Skrzypczak

Published in: LIPIcs, Volume 62, 25th EACSL Annual Conference on Computer Science Logic (CSL 2016)

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.
Cite as

Leszek Aleksander Kolodziejczyk, Henryk Michalewski, Pierre Pradic, and Michal Skrzypczak. The Logical Strength of Büchi's Decidability Theorem. In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 62, pp. 36:1-36:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{kolodziejczyk_et_al:LIPIcs.CSL.2016.36,
  author =	{Kolodziejczyk, Leszek Aleksander and Michalewski, Henryk and Pradic, Pierre and Skrzypczak, Michal},
  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 =	{Talbot, Jean-Marc and Regnier, Laurent},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.36},
  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}
}
  • Refine by Author
  • 1 Kolodziejczyk, Leszek Aleksander
  • 1 Michalewski, Henryk
  • 1 Pradic, Pierre
  • 1 Skrzypczak, Michal

  • Refine by Classification

  • Refine by Keyword
  • 1 Büchi's theorem
  • 1 additive Ramsey's theorem
  • 1 monadic second-order logic
  • 1 nondeterministic automata
  • 1 reverse mathematics

  • Refine by Type
  • 1 document

  • Refine by Publication Year
  • 1 2016

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact