Document Open Access Logo

The Logical Strength of Büchi's Decidability Theorem

Authors Leszek Aleksander Kolodziejczyk, Henryk Michalewski, Cécilia Pradic, Michal Skrzypczak

PDF

File

Thumbnail PDF
PDF
LIPIcs.CSL.2016.36.pdf
  • Filesize: 0.59 MB
  • 16 pages

Document Identifiers

Subject Classification

Keywords
  • nondeterministic automata
  • monadic second-order logic
  • Büchi's theorem
  • additive Ramsey's theorem
  • reverse mathematics

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

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 Get BibTex

Leszek Aleksander Kolodziejczyk, Henryk Michalewski, Cécilia 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) https://doi.org/10.4230/LIPIcs.CSL.2016.36

Author Details

Leszek Aleksander Kolodziejczyk
Henryk Michalewski
Cécilia Pradic
Michal Skrzypczak

References

  1. Christoph Schulte Althoff, Wolfgang Thomas, and Nico Wallmeier. Observations on determinization of Büchi automata. Theor. Comput. Sci., 363(2):224-233, 2006. URL: http://dx.doi.org/10.1016/j.tcs.2006.07.026.
  2. Mikołaj Bojańczyk. Lecture notes on languages, automata and computations, University of Warsaw, 2015. URL: http://www.mimuw.edu.pl/~bojan/20152016-2/jezyki-automaty-i-obliczenia-2/mcnaughtons-theorem.
  3. J. Richard Büchi. On a decision method in restricted second order arithmetic. In Ernest Nagel, Patrick Suppes, and Alfred Tarski, editors, Logic, Methodology and Philosophy of Science. Proceeding of the 1960 International Congress, pages 1-11. Stanford University Press, 1962. Google Scholar
  4. Petr Hájek and Pavel Pudlák. Metamathematics of first-order arithmetic. Perspectives in Mathematical Logic. Springer-Verlag, Berlin, 1993. URL: http://dx.doi.org/10.1007/978-3-662-22156-3.
  5. Denis R. Hirschfeldt. Slicing the truth, volume 28 of Lecture Notes Series. Institute for Mathematical Sciences. National University of Singapore. World Scientific, 2015. Google Scholar
  6. Jeffry L. Hirst. Combinatorics in Subsystems of Second Order Arithmetic. PhD thesis, Pennsylvania State University, 1987. Google Scholar
  7. Carl G. Jockusch, Jr. Ramsey’s theorem and recursion theory. J. Symbolic Logic, 37:268-280, 1972. Google Scholar
  8. Detlef Kähler and Thomas Wilke. Complementation, disambiguation, and determinization of Büchi automata unified. In ICALP, pages 724-735, 2008. URL: http://dx.doi.org/10.1007/978-3-540-70575-8_59.
  9. Leszek Aleksander Kołodziejczyk and Henryk Michalewski. How unprovable is Rabin’s decidability theorem? (accepted@LICS 2016). CoRR, abs/1508.06780, 2015. URL: http://arxiv.org/abs/1508.06780.
  10. G. Kreisel. A variant to Hilbert’s theory of the foundations of arithmetic. British J. Philos. Sci., 4:107-129, 1953. Google Scholar
  11. Jiayi Liu. RT²₂ does not imply WKL₀. J. Symbolic Logic, 77(2):609-620, 2012. URL: http://dx.doi.org/10.2178/jsl/1333566640.
  12. Robert McNaughton. Testing and generating infinite sequences by a finite automaton. Information and Control, 9(5):521-530, 1966. URL: http://dx.doi.org/10.1016/S0019-9958(66)80013-X.
  13. David E. Muller and Paul E. Schupp. Simulating alternating tree automata by nondeterministic automata: New results and new proofs of the theorems of Rabin, McNaughton and Safra. Theoretical Computer Science, 141(1–2):69-107, 1995. URL: http://dx.doi.org/10.1016/0304-3975(94)00214-4.
  14. Dominique Perrin and Jean-Éric Pin. Infinite words : automata, semigroups, logic and games. Pure and Applied Mathematics. Elsevier, London, San Diego (Calif.), 2004. Google Scholar
  15. Alexander Rabinovich. On decidability of monadic logic of order over the naturals extended by monadic predicates. Information and Computation, 205(6):870-889, 2007. Google Scholar
  16. Saharon Shelah. The monadic theory of order. Ann. of Math. (2), 102(3):379-419, 1975. Google Scholar
  17. Stephen G. Simpson. Subsystems of second order arithmetic. Perspectives in Mathematical Logic. Springer-Verlag, Berlin, 1999. URL: http://dx.doi.org/10.1007/978-3-642-59971-2.
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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact