The logical strength of Büchi's decidability theorem
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,≤). We prove that the following are equivalent over the weak second-order arithmetic theory RCA0: (1) the induction scheme for Σ0...
| Main Authors: | , , , |
|---|---|
| Format: | Journal article |
| Published: |
Logical Methods in Computer Science
2019
|
| _version_ | 1797081469592535040 |
|---|---|
| author | Kolodziejczyk, L Michalewski, H Pradic, P Skrzypczak, M |
| author_facet | Kolodziejczyk, L Michalewski, H Pradic, P Skrzypczak, M |
| author_sort | Kolodziejczyk, L |
| collection | OXFORD |
| description | 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,≤). We prove that the following are equivalent over the weak second-order arithmetic theory RCA0: (1) the induction scheme for Σ02 formulae of arithmetic, (2) a variant of Ramsey's Theorem for pairs restricted to so-called additive colourings, (3) Büchi's complementation theorem for nondeterministic automata on infinite words, (4) the decidability of the depth-n fragment of the MSO theory of (N,≤), for each n≥5. Moreover, each of (1)-(4) implies McNaughton's determinisation theorem for automata on infinite words, as well as the "bounded-width" version of König's Lemma, often used in proofs of McNaughton's theorem. |
| first_indexed | 2024-03-07T01:14:45Z |
| format | Journal article |
| id | oxford-uuid:8e44d86c-8de3-4938-8b00-d08f2194fe41 |
| institution | University of Oxford |
| last_indexed | 2024-03-07T01:14:45Z |
| publishDate | 2019 |
| publisher | Logical Methods in Computer Science |
| record_format | dspace |
| spelling | oxford-uuid:8e44d86c-8de3-4938-8b00-d08f2194fe412022-03-26T22:56:31ZThe logical strength of Büchi's decidability theoremJournal articlehttp://purl.org/coar/resource_type/c_dcae04bcuuid:8e44d86c-8de3-4938-8b00-d08f2194fe41Symplectic Elements at OxfordLogical Methods in Computer Science2019Kolodziejczyk, LMichalewski, HPradic, PSkrzypczak, MWe 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,≤). We prove that the following are equivalent over the weak second-order arithmetic theory RCA0: (1) the induction scheme for Σ02 formulae of arithmetic, (2) a variant of Ramsey's Theorem for pairs restricted to so-called additive colourings, (3) Büchi's complementation theorem for nondeterministic automata on infinite words, (4) the decidability of the depth-n fragment of the MSO theory of (N,≤), for each n≥5. Moreover, each of (1)-(4) implies McNaughton's determinisation theorem for automata on infinite words, as well as the "bounded-width" version of König's Lemma, often used in proofs of McNaughton's theorem. |
| spellingShingle | Kolodziejczyk, L Michalewski, H Pradic, P Skrzypczak, M The logical strength of Büchi's decidability theorem |
| title | The logical strength of Büchi's decidability theorem |
| title_full | The logical strength of Büchi's decidability theorem |
| title_fullStr | The logical strength of Büchi's decidability theorem |
| title_full_unstemmed | The logical strength of Büchi's decidability theorem |
| title_short | The logical strength of Büchi's decidability theorem |
| title_sort | logical strength of buchi s decidability theorem |
| work_keys_str_mv | AT kolodziejczykl thelogicalstrengthofbuchisdecidabilitytheorem AT michalewskih thelogicalstrengthofbuchisdecidabilitytheorem AT pradicp thelogicalstrengthofbuchisdecidabilitytheorem AT skrzypczakm thelogicalstrengthofbuchisdecidabilitytheorem AT kolodziejczykl logicalstrengthofbuchisdecidabilitytheorem AT michalewskih logicalstrengthofbuchisdecidabilitytheorem AT pradicp logicalstrengthofbuchisdecidabilitytheorem AT skrzypczakm logicalstrengthofbuchisdecidabilitytheorem |