On the Decidability of MSO+U on Infinite Trees

Mikolaj Bojaczyk; Tomasz Gogacz; Henryk Michalewski; Michal Skrzypczak

doi:10.1007/978-3-662-43951-7_5

On the Decidability of MSO+U on Infinite Trees

Mikolaj Bojaczyk, Tomasz Gogacz, Henryk Michalewski, Michal Skrzypczak

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

Abstract

This paper is about MSO+U, an extension of monadic second-order logic, which has a quantifier that can express that a property of sets is true for arbitrarily large sets. We conjecture that the MSO+U theory of the complete binary tree is undecidable. We prove a weaker statement: there is no algorithm which decides this theory and has a correctness proof in zfc. This is because the theory is undecidable, under a set-theoretic assumption consistent with zfc, namely that there exists of projective well-ordering of 2 ω of type ω 1. We use Shelah’s undecidability proof of the MSO theory of the real numbers.

Original language	English
Title of host publication	Automata, Languages, and Programming
Subtitle of host publication	41st International Colloquium, ICALP 2014, Copenhagen, Denmark, July 8-11, 2014, Proceedings, Part II
Publisher	Springer
Pages	50-61
Number of pages	12
ISBN (Electronic)	978-3-662-43951-7
ISBN (Print)	978-3-662-43950-0
DOIs	https://doi.org/10.1007/978-3-662-43951-7_5
Publication status	Published - 2014

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer Berlin Heidelberg
Volume	8573
ISSN (Print)	0302-9743

Access to Document

10.1007/978-3-662-43951-7_5

http://link.springer.com/chapter/10.1007%2F978-3-662-43951-7_5

Cite this

Bojaczyk, M., Gogacz, T., Michalewski, H., & Skrzypczak, M. (2014). On the Decidability of MSO+U on Infinite Trees. In Automata, Languages, and Programming: 41st International Colloquium, ICALP 2014, Copenhagen, Denmark, July 8-11, 2014, Proceedings, Part II (pp. 50-61). ( Lecture Notes in Computer Science; Vol. 8573). Springer. https://doi.org/10.1007/978-3-662-43951-7_5

@inproceedings{9504d722c4a6426cb37349d882a9f726,

title = "On the Decidability of MSO+U on Infinite Trees",

abstract = "This paper is about MSO+U, an extension of monadic second-order logic, which has a quantifier that can express that a property of sets is true for arbitrarily large sets. We conjecture that the MSO+U theory of the complete binary tree is undecidable. We prove a weaker statement: there is no algorithm which decides this theory and has a correctness proof in zfc. This is because the theory is undecidable, under a set-theoretic assumption consistent with zfc, namely that there exists of projective well-ordering of 2 ω of type ω 1. We use Shelah{\textquoteright}s undecidability proof of the MSO theory of the real numbers.",

author = "Mikolaj Bojaczyk and Tomasz Gogacz and Henryk Michalewski and Michal Skrzypczak",

year = "2014",

doi = "10.1007/978-3-662-43951-7_5",

language = "English",

isbn = "978-3-662-43950-0",

series = " Lecture Notes in Computer Science",

publisher = "Springer",

pages = "50--61",

booktitle = "Automata, Languages, and Programming",

address = "United Kingdom",

}

On the Decidability of MSO+U on Infinite Trees. / Bojaczyk, Mikolaj; Gogacz, Tomasz; Michalewski, Henryk et al.
Automata, Languages, and Programming: 41st International Colloquium, ICALP 2014, Copenhagen, Denmark, July 8-11, 2014, Proceedings, Part II. Springer, 2014. p. 50-61 ( Lecture Notes in Computer Science; Vol. 8573).

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

TY - GEN

T1 - On the Decidability of MSO+U on Infinite Trees

AU - Bojaczyk, Mikolaj

AU - Gogacz, Tomasz

AU - Michalewski, Henryk

AU - Skrzypczak, Michal

PY - 2014

Y1 - 2014

N2 - This paper is about MSO+U, an extension of monadic second-order logic, which has a quantifier that can express that a property of sets is true for arbitrarily large sets. We conjecture that the MSO+U theory of the complete binary tree is undecidable. We prove a weaker statement: there is no algorithm which decides this theory and has a correctness proof in zfc. This is because the theory is undecidable, under a set-theoretic assumption consistent with zfc, namely that there exists of projective well-ordering of 2 ω of type ω 1. We use Shelah’s undecidability proof of the MSO theory of the real numbers.

AB - This paper is about MSO+U, an extension of monadic second-order logic, which has a quantifier that can express that a property of sets is true for arbitrarily large sets. We conjecture that the MSO+U theory of the complete binary tree is undecidable. We prove a weaker statement: there is no algorithm which decides this theory and has a correctness proof in zfc. This is because the theory is undecidable, under a set-theoretic assumption consistent with zfc, namely that there exists of projective well-ordering of 2 ω of type ω 1. We use Shelah’s undecidability proof of the MSO theory of the real numbers.

U2 - 10.1007/978-3-662-43951-7_5

DO - 10.1007/978-3-662-43951-7_5

M3 - Conference contribution

SN - 978-3-662-43950-0

T3 - Lecture Notes in Computer Science

SP - 50

EP - 61

BT - Automata, Languages, and Programming

PB - Springer

ER -

On the Decidability of MSO+U on Infinite Trees

Abstract

Publication series

Access to Document

Fingerprint

Cite this