No Cover Image

Conference Paper/Proceeding/Abstract 208 views 14 downloads

The logical strength of Büchi's decidability theorem

Leszek Aleksander Kolodziejczyk, Henryk Michalewski, Cécilia Pradic Orcid Logo, Michał Skrzypczak

25th EACSL Annual Conference on Computer Science Logic (CSL 2016), Volume: 62, Pages: 36:1 - 36:16

Swansea University Author: Cécilia Pradic Orcid Logo

  • 58112.pdf

    PDF | Version of Record

    © Leszek Kołodziejczyk, Henryk Michalewski, Pierre Pradic, and Michał Skrzypczak; licensed under Creative Commons Attribution 3.0 Unported license (CC-BY 3.0)

    Download (574.33KB)

Check full text

DOI (Published version): 10.4230/LIPIcs.CSL.2016.36

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 com...

Full description

Published in: 25th EACSL Annual Conference on Computer Science Logic (CSL 2016)
ISBN: 978-3-95977-022-4
ISSN: 1868-8969
Published: Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik 2016
Online Access: Check full text

URI: https://cronfa.swan.ac.uk/Record/cronfa58112
Tags: Add Tag
No Tags, Be the first to tag this record!
first_indexed 2021-10-25T09:26:51Z
last_indexed 2021-10-26T03:24:17Z
id cronfa58112
recordtype SURis
fullrecord <?xml version="1.0"?><rfc1807><datestamp>2021-10-25T11:26:31.1149294</datestamp><bib-version>v2</bib-version><id>58112</id><entry>2021-09-27</entry><title>The logical strength of B&#xFC;chi's decidability theorem</title><swanseaauthors><author><sid>3b6e9ebd791c875dac266b3b0b358a58</sid><ORCID>0000-0002-1600-8846</ORCID><firstname>C&#xE9;cilia</firstname><surname>Pradic</surname><name>C&#xE9;cilia Pradic</name><active>true</active><ethesisStudent>false</ethesisStudent></author></swanseaauthors><date>2021-09-27</date><deptcode>SCS</deptcode><abstract>We study the strength of axioms needed to prove various results related to automata on infinite words and B&#xFC;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&#xFC;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&#xF6;nig's Lemma, often used in proofs of McNaughton's theorem.</abstract><type>Conference Paper/Proceeding/Abstract</type><journal>25th EACSL Annual Conference on Computer Science Logic (CSL 2016)</journal><volume>62</volume><journalNumber/><paginationStart>36:1</paginationStart><paginationEnd>36:16</paginationEnd><publisher>Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik</publisher><placeOfPublication/><isbnPrint/><isbnElectronic>978-3-95977-022-4</isbnElectronic><issnPrint/><issnElectronic>1868-8969</issnElectronic><keywords/><publishedDay>25</publishedDay><publishedMonth>8</publishedMonth><publishedYear>2016</publishedYear><publishedDate>2016-08-25</publishedDate><doi>10.4230/LIPIcs.CSL.2016.36</doi><url>http://drops.dagstuhl.de/opus/volltexte/2016/6576</url><notes>http://drops.dagstuhl.de/opus/volltexte/2016/6576</notes><college>COLLEGE NANME</college><department>Computer Science</department><CollegeCode>COLLEGE CODE</CollegeCode><DepartmentCode>SCS</DepartmentCode><institution>Swansea University</institution><apcterm/><lastEdited>2021-10-25T11:26:31.1149294</lastEdited><Created>2021-09-27T22:52:27.6150757</Created><path><level id="1">Faculty of Science and Engineering</level><level id="2">School of Mathematics and Computer Science - Computer Science</level></path><authors><author><firstname>Leszek Aleksander</firstname><surname>Kolodziejczyk</surname><order>1</order></author><author><firstname>Henryk</firstname><surname>Michalewski</surname><order>2</order></author><author><firstname>C&#xE9;cilia</firstname><surname>Pradic</surname><orcid>0000-0002-1600-8846</orcid><order>3</order></author><author><firstname>Micha&#x142;</firstname><surname>Skrzypczak</surname><order>4</order></author></authors><documents><document><filename>58112__21287__32db592f044540d3a9d874c393b0eda9.pdf</filename><originalFilename>58112.pdf</originalFilename><uploaded>2021-10-25T10:27:14.0702520</uploaded><type>Output</type><contentLength>588109</contentLength><contentType>application/pdf</contentType><version>Version of Record</version><cronfaStatus>true</cronfaStatus><documentNotes>&#xA9; Leszek Ko&#x142;odziejczyk, Henryk Michalewski, Pierre Pradic, and Micha&#x142; Skrzypczak; licensed under Creative Commons Attribution 3.0 Unported license (CC-BY 3.0)</documentNotes><copyrightCorrect>true</copyrightCorrect><language>eng</language><licence>https://creativecommons.org/licenses/by/3.0/legalcode</licence></document></documents><OutputDurs/></rfc1807>
spelling 2021-10-25T11:26:31.1149294 v2 58112 2021-09-27 The logical strength of Büchi's decidability theorem 3b6e9ebd791c875dac266b3b0b358a58 0000-0002-1600-8846 Cécilia Pradic Cécilia Pradic true false 2021-09-27 SCS 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. Conference Paper/Proceeding/Abstract 25th EACSL Annual Conference on Computer Science Logic (CSL 2016) 62 36:1 36:16 Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik 978-3-95977-022-4 1868-8969 25 8 2016 2016-08-25 10.4230/LIPIcs.CSL.2016.36 http://drops.dagstuhl.de/opus/volltexte/2016/6576 http://drops.dagstuhl.de/opus/volltexte/2016/6576 COLLEGE NANME Computer Science COLLEGE CODE SCS Swansea University 2021-10-25T11:26:31.1149294 2021-09-27T22:52:27.6150757 Faculty of Science and Engineering School of Mathematics and Computer Science - Computer Science Leszek Aleksander Kolodziejczyk 1 Henryk Michalewski 2 Cécilia Pradic 0000-0002-1600-8846 3 Michał Skrzypczak 4 58112__21287__32db592f044540d3a9d874c393b0eda9.pdf 58112.pdf 2021-10-25T10:27:14.0702520 Output 588109 application/pdf Version of Record true © Leszek Kołodziejczyk, Henryk Michalewski, Pierre Pradic, and Michał Skrzypczak; licensed under Creative Commons Attribution 3.0 Unported license (CC-BY 3.0) true eng https://creativecommons.org/licenses/by/3.0/legalcode
title The logical strength of Büchi's decidability theorem
spellingShingle The logical strength of Büchi's decidability theorem
Cécilia Pradic
title_short 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_sort The logical strength of Büchi's decidability theorem
author_id_str_mv 3b6e9ebd791c875dac266b3b0b358a58
author_id_fullname_str_mv 3b6e9ebd791c875dac266b3b0b358a58_***_Cécilia Pradic
author Cécilia Pradic
author2 Leszek Aleksander Kolodziejczyk
Henryk Michalewski
Cécilia Pradic
Michał Skrzypczak
format Conference Paper/Proceeding/Abstract
container_title 25th EACSL Annual Conference on Computer Science Logic (CSL 2016)
container_volume 62
container_start_page 36:1
publishDate 2016
institution Swansea University
isbn 978-3-95977-022-4
issn 1868-8969
doi_str_mv 10.4230/LIPIcs.CSL.2016.36
publisher Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik
college_str Faculty of Science and Engineering
hierarchytype
hierarchy_top_id facultyofscienceandengineering
hierarchy_top_title Faculty of Science and Engineering
hierarchy_parent_id facultyofscienceandengineering
hierarchy_parent_title Faculty of Science and Engineering
department_str School of Mathematics and Computer Science - Computer Science{{{_:::_}}}Faculty of Science and Engineering{{{_:::_}}}School of Mathematics and Computer Science - Computer Science
url http://drops.dagstuhl.de/opus/volltexte/2016/6576
document_store_str 1
active_str 0
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, 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.
published_date 2016-08-25T04:14:22Z
_version_ 1763753971290210304
score 10.952468

Similar Items