You are not logged in |
The logical strength of Büchi's decidability theorem
- Speaker(s)
- Leszek Kołodziejczyk
- Affiliation
- Uniwersytet Warszawski
- Date
- June 8, 2016, 2:15 p.m.
- Room
- room 5870
- Seminar
- Seminar Automata Theory
I will talk about the strength of axioms needed to prove Büchi's decidability theorem and related results concerning automata on infinite words. The talk will be based on joint work with Henryk Michalewski, Michał Skrzypczak and Pierre Pradic, which complements earlier joint work with Henryk on analogous questions about infinite tree automata.
The theory of automata on infinite objects makes little sense without an axiom known as \Sigma^0_2 induction. Our main finding is that this axiom is already enough to prove all the basic theorems on word automata. In particular, the use of König's lemma and/or Ramsey's theorem in proofs of Büchi's theorem is in some sense unneeded. This situation is very different from what happens in the theory of tree automata, where \Sigma^0_2 induction also suffices to make sense of the definitions, but the basic theorems (complementation etc.) do not hold in the absence of strong set existence axioms.
The theory of automata on infinite objects makes little sense without an axiom known as \Sigma^0_2 induction. Our main finding is that this axiom is already enough to prove all the basic theorems on word automata. In particular, the use of König's lemma and/or Ramsey's theorem in proofs of Büchi's theorem is in some sense unneeded. This situation is very different from what happens in the theory of tree automata, where \Sigma^0_2 induction also suffices to make sense of the definitions, but the basic theorems (complementation etc.) do not hold in the absence of strong set existence axioms.
