You are not logged in |
A Complete Axiomatization of MSO on Infinite Trees
- Speaker(s)
- Das Anupam
- Affiliation
- École Normale Supérieure de Lyon
- Date
- April 15, 2015, 2:15 p.m.
- Room
- room 5870
- Seminar
- Seminar Automata Theory
We show that an adaptation of Peano’s axioms for second-order
arithmetic to the language of MSO completely axiomatizes the theory
over infinite trees. This continues a line of work begun by Büchi
and Siefkes with axiomatizations of MSO over various classes of linear
orders.
Our proof formalizes, in the axiomatic theory, a translation of MSO formulas to alternating parity tree automata. The main ingredient is
the formalized proof of positional determinacy for the corresponding
parity games, which as usual allows to complement automata and to deal with negation of MSO formulas. The Comprehension Scheme of monadic second-order logic is used to obtain uniform winning strategies, where most usual proofs of positional determinacy rely on instances of the Axiom of Choice or of transfinite induction.
arithmetic to the language of MSO completely axiomatizes the theory
over infinite trees. This continues a line of work begun by Büchi
and Siefkes with axiomatizations of MSO over various classes of linear
orders.
Our proof formalizes, in the axiomatic theory, a translation of MSO formulas to alternating parity tree automata. The main ingredient is
the formalized proof of positional determinacy for the corresponding
parity games, which as usual allows to complement automata and to deal with negation of MSO formulas. The Comprehension Scheme of monadic second-order logic is used to obtain uniform winning strategies, where most usual proofs of positional determinacy rely on instances of the Axiom of Choice or of transfinite induction.
