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
|