Document

# On Uniformization in the Full Binary Tree

## File

LIPIcs.MFCS.2022.77.pdf
• Filesize: 0.75 MB
• 14 pages

## Cite As

Alexander Rabinovich. On Uniformization in the Full Binary Tree. In 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 241, pp. 77:1-77:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.MFCS.2022.77

## Abstract

A function f uniformizes a relation R(X,Y) if R(X,f(X)) holds for every X in the domain of R. The uniformization problem for a logic L asks whether for every L-definable relation there is an L-definable function that uniformizes it. Gurevich and Shelah proved that no Monadic Second-Order (MSO) definable function uniformizes relation "Y is a one element subset of X" in the full binary tree. In other words, there is no MSO definable choice function in the full binary tree. The cross-section of a relation R(X,Y) at D is the set of all E such that R(D,E) holds. Hence, a function that uniformizes R chooses one element from every non-empty cross-section. The relation "Y is a one element subset of X" has finite and countable cross-sections. We prove that in the full binary tree the following theorems hold: ▶ Theorem (Finite cross-sections) If every cross-section of an MSO definable relation is finite, then it has an MSO definable uniformizer. ▶ Theorem (Uncountable cross-section) There is an MSO definable relation R such that every MSO definable relation included in R and with the same domain as R has an uncountable cross-section.

## Subject Classification

##### ACM Subject Classification
• Theory of computation → Logic and verification
##### Keywords
• Uniformization

## Metrics

• Access Statistics
• Total Accesses (updated on a weekly basis)
0

## References

1. Vince Bárány, Łukasz Kaiser, and Alex Rabinovich. Expressing cardinality quantifiers in monadic second-order logic over trees. Fundamenta Informaticae, 100(1-4):1-17, 2010.
2. Arnaud Carayol and Christof Löding. MSO on the infinite binary tree: Choice and order. In International Workshop on Computer Science Logic, pages 161-176. Springer, 2007.
3. Arnaud Carayol, Christof Löding, Damian Niwinski, and Igor Walukiewicz. Choice functions and well-orderings over the infinite binary tree. Open Mathematics, 8(4):662-682, 2010.
4. Grzegorz Fabianski, Michal Skrzypczak, and Szymon Torunczyk. Uniformisations of regular relations over bi-infinite words. In Holger Hermanns, Lijun Zhang, Naoki Kobayashi, and Dale Miller, editors, LICS '20: 35th Annual ACM/IEEE Symposium on Logic in Computer Science, Saarbrücken, Germany, July 8-11, 2020, pages 384-396. ACM, 2020. URL: https://doi.org/10.1145/3373718.3394782.
5. Yuri Gurevich. Monadic second-order theories. Model-theoretic logics, pages 479-506, 1985.
6. Yuri Gurevich and Saharon Shelah. Rabin’s uniformization problem 1. The Journal of Symbolic Logic, 48(4):1105-1119, 1983.
7. Shmuel Lifsches and Saharon Shelah. Uniformization and skolem functions in the class of trees. The Journal of Symbolic Logic, 63(1):103-127, 1998.
8. Michael O Rabin. Decidability of second-order theories and automata on infinite trees. Transactions of the american Mathematical Society, 141:1-35, 1969.
9. Saharon Shelah. The monadic theory of order. Annals of Mathematics, 102(3):379-419, 1975.
10. Wolfgang Thomas. Automata on infinite objects. In Formal Models and Semantics, pages 133-191. Elsevier, 1990.
11. Wolfgang Thomas. Ehrenfeucht games, the composition method, and the monadic theory of ordinal words. In Structures in Logic and Computer Science, pages 118-143. Springer, 1997.
12. Boris Trakhtenbrot and Ya Martynovich Barzdin. Finite automate: behaviour and synthesis. North-Holland, 1973.
X

Feedback for Dagstuhl Publishing