MSO on the Infinite Binary Tree: Choice and Order

Abstract : We give a new proof showing that it is not possible to define in monadic second-order logic (MSO) a choice function on the infinite binary tree. This result was first obtained by Gurevich and Shelah using set theoretical arguments. Our proof is much simpler and only uses basic tools from automata theory. We discuss some applications of the result concerning unambiguous tree automata and definability of winning strategies in infinite games. In a second part we strengthen the result of the non-existence of an MSO-definable well-founded order on the infinite binary tree by showing that every infinite binary tree with a well-founded order has an undecidable MSO-theory.
Document type :
Conference papers
Complete list of metadatas

Cited literature [13 references]  Display  Hide  Download

https://hal-upec-upem.archives-ouvertes.fr/hal-00620169
Contributor : Arnaud Carayol <>
Submitted on : Tuesday, March 5, 2013 - 11:05:36 PM
Last modification on : Wednesday, April 11, 2018 - 12:12:02 PM
Long-term archiving on: Thursday, June 6, 2013 - 3:05:12 AM

File

csl07.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

Arnaud Carayol, Christof Löding. MSO on the Infinite Binary Tree: Choice and Order. 16th EACSL Annual Conference on Computer Science and Logic (CSL'07), Sep 2007, Lausanne, Switzerland. pp.161-176, ⟨10.1007/978-3-540-74915-8_15⟩. ⟨hal-00620169⟩

Share

Metrics

Record views

237

Files downloads

200