A complete axiomatization of MSO on infinite trees


We show that an adaptation of Peano's axioms for second-order arithmetic to the language of MSO completely axiomatises 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.