Kolodziejczyk, Leszek Aleksander
[VerfasserIn];
Michalewski, Henryk
[VerfasserIn];
Pradic, Pierre
[VerfasserIn];
Skrzypczak, Michal
[VerfasserIn]
;
Leszek Aleksander Kolodziejczyk and Henryk Michalewski and Pierre Pradic and Michal Skrzypczak
[MitwirkendeR]
The Logical Strength of Büchi's Decidability Theorem
Titel:
The Logical Strength of Büchi's Decidability Theorem
Beteiligte:
Kolodziejczyk, Leszek Aleksander
[VerfasserIn];
Michalewski, Henryk
[VerfasserIn];
Pradic, Pierre
[VerfasserIn];
Skrzypczak, Michal
[VerfasserIn]
Erschienen:
Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2016
Anmerkungen:
Diese Datenquelle enthält auch Bestandsnachweise, die nicht zu einem Volltext führen.
Beschreibung:
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.