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.

---