2026-07-23T20:03:01Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:16875 2024-03-06T10:58:33Z ddc:004 open_access

On Uniformization in the Full Binary Tree Rabinovich, Alexander Monadic Second-Order Logic Uniformization 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Alexander Rabinovich 2022 Is Part Of LIPIcs, Volume 241, 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.MFCS.2022.77 urn:nbn:de:0030-drops-168757 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2022.77 eng https://creativecommons.org/licenses/by/4.0/legalcode