A Complete Axiomatization of MSO on Infinite Trees

Anupam Das, Colin Riba

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

2 Citations (Scopus)
25 Downloads (Pure)

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
PublisherInstitute of Electrical and Electronics Engineers (IEEE)
Pages390-401
Number of pages12
ISBN (Electronic)9781479988754
DOIs
Publication statusPublished - 3 Aug 2015
Event30th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2015 - Kyoto, Japan
Duration: 6 Jul 201510 Jul 2015

Publication series

NameProceedings - Symposium on Logic in Computer Science
PublisherInstitute of Electrical and Electronics Engineers (IEEE)
ISSN (Print)1043-6871

Conference

Conference30th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2015
Country/TerritoryJapan
CityKyoto
Period6/07/1510/07/15

Bibliographical note

Publisher Copyright:
© 2015 IEEE.

Keywords

  • Automata
  • Axiomatization
  • Infinite trees
  • MSO
  • Proof theory

ASJC Scopus subject areas

  • Software
  • General Mathematics

Fingerprint

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

Cite this