No Cover Image

Conference Paper/Proceeding/Abstract 920 views

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

Full text not available from this repository: check for access using links below.

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
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>MACS</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>Mathematics and Computer Science School</department><CollegeCode>COLLEGE CODE</CollegeCode><DepartmentCode>MACS</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/><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 MACS 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 Mathematics and Computer Science School COLLEGE CODE MACS 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
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 0
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-25T16:34:30Z
_version_ 1850686802195644416
score 11.08899

Similar Items