No Cover Image

Conference Paper/Proceeding/Abstract 447 views 48 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!
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.
Item Description: http://drops.dagstuhl.de/opus/volltexte/2016/6576
College: Faculty of Science and Engineering
Start Page: 36:1
End Page: 36:16

Similar Items