A Complete Axiomatization of MSO on Infinite Trees

Anupam Das, Colin Riba

Research output: Chapter in Book/Report/Conference proceedingConference contribution

2 Citations (Scopus)

Abstract

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 us to complement automata in order to deal with negation of MSO formulas. The Comprehension scheme of monadic second-order logic is used to obtain uniform winning strategies, whereas most usual proofs of positional determinacy rely on forms of the Axiom of Choice or transfinite induction
Original languageEnglish
Title of host publication2015 30th Annual ACM/IEEE Symposium on Logic in Computer Science
Subtitle of host publicationLICS 2015
PublisherIEEE Computer Society Press
Pages390-401
ISBN (Print)9781479988754
DOIs
Publication statusPublished - 6 Jul 2015
Event2015 30th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2015) - Kyoto, Japan
Duration: 6 Jul 201510 Jul 2015

Conference

Conference2015 30th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2015)
Country/TerritoryJapan
CityKyoto
Period6/07/1510/07/15

Keywords

  • MSO
  • proof theory
  • automata
  • axiomatization
  • infinite trees

Fingerprint

Dive into the research topics of 'A Complete Axiomatization of MSO on Infinite Trees'. Together they form a unique fingerprint.

Cite this