A Complete Axiomatization of MSO on Infinite Trees

Anupam Das; Colin Riba

doi:10.1109/LICS.2015.44

A Complete Axiomatization of MSO on Infinite Trees

Anupam Das, Colin Riba

Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

2 Citations (Scopus)

15 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 language	English
Title of host publication	2015 30th Annual ACM/IEEE Symposium on Logic in Computer Science
Publisher	Institute of Electrical and Electronics Engineers (IEEE)
Pages	390-401
Number of pages	12
ISBN (Electronic)	9781479988754
DOIs	https://doi.org/10.1109/LICS.2015.44
Publication status	Published - 3 Aug 2015
Event	30th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2015 - Kyoto, Japan Duration: 6 Jul 2015 → 10 Jul 2015

Publication series

Name	Proceedings - Symposium on Logic in Computer Science
Publisher	Institute of Electrical and Electronics Engineers (IEEE)
ISSN (Print)	1043-6871

Conference

Conference	30th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2015
Country/Territory	Japan
City	Kyoto
Period	6/07/15 → 10/07/15

Bibliographical note

Publisher Copyright:
© 2015 IEEE.

Keywords

Automata
Axiomatization
Infinite trees
MSO
Proof theory

ASJC Scopus subject areas

Software
General Mathematics

Access to Document

10.1109/LICS.2015.44

DasA2015complete
A. Das and C. Riba, "A Complete Axiomatization of MSO on Infinite Trees," 2015 30th Annual ACM/IEEE Symposium on Logic in Computer Science, Kyoto, Japan, 2015, pp. 390-401, doi: 10.1109/LICS.2015.44. © 2015 IEEE. Personal use of this material is permitted. Permission from IEEE must be obtained for all other uses, in any current or future media, including reprinting/republishing this material for advertising or promotional purposes, creating new collective works, for resale or redistribution to servers or lists, or reuse of any copyrighted component of this work in other works.
Accepted author manuscript, 411 KBLicence: Other (please specify with Rights Statement)

http://ieeexplore.ieee.org/document/7174898/

Cite this

@inproceedings{c9f6fa2ebbfd4af1b84fdd9c7194b61f,

title = "A Complete Axiomatization of MSO on Infinite Trees",

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{\"u}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",

keywords = "Automata, Axiomatization, Infinite trees, MSO, Proof theory",

author = "Anupam Das and Colin Riba",

note = "Publisher Copyright: {\textcopyright} 2015 IEEE.; 30th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2015 ; Conference date: 06-07-2015 Through 10-07-2015",

year = "2015",

month = aug,

day = "3",

doi = "10.1109/LICS.2015.44",

language = "English",

series = "Proceedings - Symposium on Logic in Computer Science",

publisher = "Institute of Electrical and Electronics Engineers (IEEE)",

pages = "390--401",

booktitle = "2015 30th Annual ACM/IEEE Symposium on Logic in Computer Science",

}

Das, A & Riba, C 2015, A Complete Axiomatization of MSO on Infinite Trees. in 2015 30th Annual ACM/IEEE Symposium on Logic in Computer Science ., 7174898, Proceedings - Symposium on Logic in Computer Science, Institute of Electrical and Electronics Engineers (IEEE), pp. 390-401, 30th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2015, Kyoto, Japan, 6/07/15. https://doi.org/10.1109/LICS.2015.44

A Complete Axiomatization of MSO on Infinite Trees. / Das, Anupam; Riba, Colin.
2015 30th Annual ACM/IEEE Symposium on Logic in Computer Science . Institute of Electrical and Electronics Engineers (IEEE), 2015. p. 390-401 7174898 (Proceedings - Symposium on Logic in Computer Science).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - A Complete Axiomatization of MSO on Infinite Trees

AU - Das, Anupam

AU - Riba, Colin

PY - 2015/8/3

Y1 - 2015/8/3

N2 - 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

AB - 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

KW - Automata

KW - Axiomatization

KW - Infinite trees

KW - MSO

KW - Proof theory

UR - http://www.scopus.com/inward/record.url?scp=84945897163&partnerID=8YFLogxK

U2 - 10.1109/LICS.2015.44

DO - 10.1109/LICS.2015.44

M3 - Conference contribution

T3 - Proceedings - Symposium on Logic in Computer Science

SP - 390

EP - 401

BT - 2015 30th Annual ACM/IEEE Symposium on Logic in Computer Science

PB - Institute of Electrical and Electronics Engineers (IEEE)

T2 - 30th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2015

Y2 - 6 July 2015 through 10 July 2015

ER -

A Complete Axiomatization of MSO on Infinite Trees

Abstract

Publication series

Conference

Bibliographical note

Keywords

ASJC Scopus subject areas

Access to Document

Fingerprint

Cite this