Selection and Uniformization Problems in the Monadic Theory of Ordinals: A Survey
---
paper_title: The Monadic Theory of Order

paper_content:

We deal with the monadic (second-order) theory of order. We prove all known results in a unified way, show a general way of reduction, prove more results and show the limitation on extending them. We prove (CH) that the monadic theory of the real order is undecidable. Our methods are modeltheoretic, and we do not use automaton theory.
---
paper_title: The monadic second order theory of all countable ordinals

paper_content:

The monadic second order theory of ?1.- Axiomatization of the monadic second order theory of ?1.
---
paper_title: Decision problems of finite automata design and related arithmetics

paper_content:

1. Motivation. Many variants of the notion of automaton have appeared in the literature. We find it convenient here to adopt the notion of E. F. Moore [7]. Inasmuch as Rabin-Scott [9] adopt this notion, too, it is convenient to refer to [9] for various results presumed here. In particular, Kleene's theorem [5, Theorems 3, 5] is used in the form in which it appears in [9]. It is often perspicacious to view regular expressions, and this notion is used in the sense of [3]. In general, we are concerned with the problems of automatically designing an automaton from a specification of a relation which is to hold between the automaton's input sequences and determined output sequences. These "design requirements" are given via a formula of some kind. The problems with which we are concerned have been described in [1]. With respect to particular formalisms for expressing "design requirements" as well as the notion of automaton itself, the problems are briefly and informally these: (1) to produce an algorithm which when it operates on an automaton and a design requirement produces the correct answer to the question "Does this automaton satisfy this design requirement?", or else show no such algorithm exists; (2) to produce an algorithm which operates on a design requirement and produces the correct answer to the question "Does there exist an automaton which satisfies this design requirement?", or else show no such algorithm exists; (3) to produce an algorithm which operates on a design requirement and terminates with an automaton which satisfies the requirement when one exists and otherwise fails to terminate, or else show no such algorithm exists. Interrelationships among problems (1), (2), (3) will appear in the paper [1]. This paper will also indicate the close connection between problem (1) and decision problems for truth of sentences of certain arithmetics. The paper [1 ] will also make use of certain results concerning weak arithmetics already obtained in the literature to obtain answers to problems (1) and (3). Thus
---
paper_title: Weak Second-Order Arithmetic and Finite Automata

paper_content:

The formalism of regular expressions was introduced by S. C. Kleene [6] to obtain the following basic theorems.
---
paper_title: Automata on Infinite Objects and Church's Problem

paper_content:

Basic definitions and results Closure properties of difusable sets The sequential calculus Automaton transformations and Church's problem> Regular trees The emptiness problem The solvability problem.
---
paper_title: Weak Second-Order Arithmetic and Finite Automata

paper_content:

The formalism of regular expressions was introduced by S. C. Kleene [6] to obtain the following basic theorems.
---
paper_title: Rabin's uniformization problem

paper_content:

The set of all words in the alphabet {l, r) forms the full binary tree T. If x E T then xl and xr are the left and the right successors of x respectively. We consider the monadic second-order language of the full binary tree with the two successor rela- tions. This language allows quantification over elements of Tand over arbitrary subsets of T. We prove that there is no monadic second-order formula 0*(X, y) such that for every nonempty subset Xof Tthere is a uniquey e Xthat satisfies 0q*(X, y) in T.
---
paper_title: Uniformization and Skolem Functions in the Class of Trees

paper_content:

The monadic second-order theory of trees allows quantification over elements and over arbitrary subsets. We classify the class of trees with respect to the question: does a tree T have definable Skolem functions (by a monadic formula with parameters)? This continues [LiSh539] where the question was asked only with respect to choice functions. Here we define a subclass of the class of tame trees (trees with a definable choice function) and prove that this is exactly the class (actually set) of trees with definable Skolem functions.
---
paper_title: Solving sequential conditions by finite-state strategies

paper_content:

Our main purpose is to present an algorithm which decides whether or not a condition 𝕮(X, Y) stated in sequential calculus admits a finite automata solution, and produces one if it exists. This solves a problem stated in [4] and contains, as a very special case, the answer to Case 4 left open in [6]. In an equally appealing form the result can be restated in the terminology of [7], [10], [15]: Every ω-game definable in sequential calculus is determined. Moreover the player who has a winning strategy, in fact, has a winning finite-state strategy, that is one which can effectively be played in a strong sense. The main proof, that of the central Theorem 1, will be presented at the end. We begin with a discussion of its consequences.
---
paper_title: Selection over classes of ordinals expanded by monadic predicates

paper_content:

Abstract A monadic formula ψ ( Y ) is a selector for a monadic formula φ ( Y ) in a structure M if ψ defines in M a unique subset P of the domain and this P also satisfies φ in M . If C is a class of structures and φ is a selector for ψ in every M ∈ C , we say that φ is a selector for φ over C . For a monadic formula φ ( X , Y ) and ordinals α ≤ ω 1 and δ ω ω , we decide whether there exists a monadic formula ψ ( X , Y ) such that for every P ⊆ α of order-type smaller than δ , ψ ( P , Y ) selects φ ( P , Y ) in ( α , ) . If so, we construct such a ψ . We introduce a criterion for a class C of ordinals to have the property that every monadic formula φ has a selector over it. We deduce the existence of S ⊆ ω ω such that in the structure ( ω ω , , S ) every formula has a selector. Given a monadic sentence π and a monadic formula φ ( Y ) , we decide whether φ has a selector over the class of countable ordinals satisfying π , and if so, construct one for it.
---
paper_title: The Monadic Theory of Order

paper_content:

We deal with the monadic (second-order) theory of order. We prove all known results in a unified way, show a general way of reduction, prove more results and show the limitation on extending them. We prove (CH) that the monadic theory of the real order is undecidable. Our methods are modeltheoretic, and we do not use automaton theory.
---
paper_title: Selection in the monadic theory of a countable ordinal

paper_content:

A monadic formula y/{ Y) is a selector for a formula cp{ Y) in a structure Jt if there exists a unique subset P of M which satisfies y/ and this P also satisfies coco there are formulas having no selector in the structure {a, <). For a < co\, we decide which formulas have a selector in (a, <), and construct selectors for them. We deduce the impossibility of a full generalization of the B?chi-Landweber solvability theorem from (co, <) to (cow, <). We state a partial extension ofthat theorem to all countable ordinals. To each formula we assign a selection degree which measures "how difficult it is to select". We show that in a countable ordinal all non-selectable formulas share the same
---
paper_title: The monadic second order theory of all countable ordinals

paper_content:

The monadic second order theory of ?1.- Axiomatization of the monadic second order theory of ?1.
---
paper_title: The monadic second order theory of all countable ordinals

paper_content:

The monadic second order theory of ?1.- Axiomatization of the monadic second order theory of ?1.
---
paper_title: Rabin's uniformization problem

paper_content:

The set of all words in the alphabet {l, r) forms the full binary tree T. If x E T then xl and xr are the left and the right successors of x respectively. We consider the monadic second-order language of the full binary tree with the two successor rela- tions. This language allows quantification over elements of Tand over arbitrary subsets of T. We prove that there is no monadic second-order formula 0*(X, y) such that for every nonempty subset Xof Tthere is a uniquey e Xthat satisfies 0q*(X, y) in T.
---
paper_title: The monadic second order theory of all countable ordinals

paper_content:

The monadic second order theory of ?1.- Axiomatization of the monadic second order theory of ?1.
---
paper_title: Uniformization and Skolem Functions in the Class of Trees

paper_content:

The monadic second-order theory of trees allows quantification over elements and over arbitrary subsets. We classify the class of trees with respect to the question: does a tree T have definable Skolem functions (by a monadic formula with parameters)? This continues [LiSh539] where the question was asked only with respect to choice functions. Here we define a subclass of the class of tame trees (trees with a definable choice function) and prove that this is exactly the class (actually set) of trees with definable Skolem functions.
---
paper_title: Automata on Infinite Objects and Church's Problem

paper_content:

Basic definitions and results Closure properties of difusable sets The sequential calculus Automaton transformations and Church's problem> Regular trees The emptiness problem The solvability problem.
---
paper_title: Selection over classes of ordinals expanded by monadic predicates

paper_content:

Abstract A monadic formula ψ ( Y ) is a selector for a monadic formula φ ( Y ) in a structure M if ψ defines in M a unique subset P of the domain and this P also satisfies φ in M . If C is a class of structures and φ is a selector for ψ in every M ∈ C , we say that φ is a selector for φ over C . For a monadic formula φ ( X , Y ) and ordinals α ≤ ω 1 and δ ω ω , we decide whether there exists a monadic formula ψ ( X , Y ) such that for every P ⊆ α of order-type smaller than δ , ψ ( P , Y ) selects φ ( P , Y ) in ( α , ) . If so, we construct such a ψ . We introduce a criterion for a class C of ordinals to have the property that every monadic formula φ has a selector over it. We deduce the existence of S ⊆ ω ω such that in the structure ( ω ω , , S ) every formula has a selector. Given a monadic sentence π and a monadic formula φ ( Y ) , we decide whether φ has a selector over the class of countable ordinals satisfying π , and if so, construct one for it.
---
paper_title: Uniformization and Skolem Functions in the Class of Trees

paper_content:

The monadic second-order theory of trees allows quantification over elements and over arbitrary subsets. We classify the class of trees with respect to the question: does a tree T have definable Skolem functions (by a monadic formula with parameters)? This continues [LiSh539] where the question was asked only with respect to choice functions. Here we define a subclass of the class of tame trees (trees with a definable choice function) and prove that this is exactly the class (actually set) of trees with definable Skolem functions.
---
paper_title: Selection over classes of ordinals expanded by monadic predicates

paper_content:

Abstract A monadic formula ψ ( Y ) is a selector for a monadic formula φ ( Y ) in a structure M if ψ defines in M a unique subset P of the domain and this P also satisfies φ in M . If C is a class of structures and φ is a selector for ψ in every M ∈ C , we say that φ is a selector for φ over C . For a monadic formula φ ( X , Y ) and ordinals α ≤ ω 1 and δ ω ω , we decide whether there exists a monadic formula ψ ( X , Y ) such that for every P ⊆ α of order-type smaller than δ , ψ ( P , Y ) selects φ ( P , Y ) in ( α , ) . If so, we construct such a ψ . We introduce a criterion for a class C of ordinals to have the property that every monadic formula φ has a selector over it. We deduce the existence of S ⊆ ω ω such that in the structure ( ω ω , , S ) every formula has a selector. Given a monadic sentence π and a monadic formula φ ( Y ) , we decide whether φ has a selector over the class of countable ordinals satisfying π , and if so, construct one for it.
---
paper_title: The Stationary Set Splitting Game

paper_content:

The \emph{stationary set splitting game} is a game of perfect information of length $\omega_{1}$ between two players, \unspls and \spl, in which \unspls chooses stationarily many countable ordinals and \spls tries to continuously divide them into two stationary pieces. We show that it is possible in ZFC to force a winning strategy for either player, or for neither. This gives a new counterexample to $\Sigma^{2}_{2}$ maximality with a predicate for the nonstationary ideal on $\omega_{1}$, and an example of a consistently undetermined game of length $\omega_{1}$ with payoff definable in the second-order monadic logic of order. We also show that the determinacy of the game is consistent with Martin's Axiom but not Martin's Maximum.
---
paper_title: Decision problems of finite automata design and related arithmetics

paper_content:

1. Motivation. Many variants of the notion of automaton have appeared in the literature. We find it convenient here to adopt the notion of E. F. Moore [7]. Inasmuch as Rabin-Scott [9] adopt this notion, too, it is convenient to refer to [9] for various results presumed here. In particular, Kleene's theorem [5, Theorems 3, 5] is used in the form in which it appears in [9]. It is often perspicacious to view regular expressions, and this notion is used in the sense of [3]. In general, we are concerned with the problems of automatically designing an automaton from a specification of a relation which is to hold between the automaton's input sequences and determined output sequences. These "design requirements" are given via a formula of some kind. The problems with which we are concerned have been described in [1]. With respect to particular formalisms for expressing "design requirements" as well as the notion of automaton itself, the problems are briefly and informally these: (1) to produce an algorithm which when it operates on an automaton and a design requirement produces the correct answer to the question "Does this automaton satisfy this design requirement?", or else show no such algorithm exists; (2) to produce an algorithm which operates on a design requirement and produces the correct answer to the question "Does there exist an automaton which satisfies this design requirement?", or else show no such algorithm exists; (3) to produce an algorithm which operates on a design requirement and terminates with an automaton which satisfies the requirement when one exists and otherwise fails to terminate, or else show no such algorithm exists. Interrelationships among problems (1), (2), (3) will appear in the paper [1]. This paper will also indicate the close connection between problem (1) and decision problems for truth of sentences of certain arithmetics. The paper [1 ] will also make use of certain results concerning weak arithmetics already obtained in the literature to obtain answers to problems (1) and (3). Thus
---
paper_title: Solving sequential conditions by finite-state strategies

paper_content:

Our main purpose is to present an algorithm which decides whether or not a condition 𝕮(X, Y) stated in sequential calculus admits a finite automata solution, and produces one if it exists. This solves a problem stated in [4] and contains, as a very special case, the answer to Case 4 left open in [6]. In an equally appealing form the result can be restated in the terminology of [7], [10], [15]: Every ω-game definable in sequential calculus is determined. Moreover the player who has a winning strategy, in fact, has a winning finite-state strategy, that is one which can effectively be played in a strong sense. The main proof, that of the central Theorem 1, will be presented at the end. We begin with a discussion of its consequences.
---
paper_title: The Stationary Set Splitting Game

paper_content:

The \emph{stationary set splitting game} is a game of perfect information of length $\omega_{1}$ between two players, \unspls and \spl, in which \unspls chooses stationarily many countable ordinals and \spls tries to continuously divide them into two stationary pieces. We show that it is possible in ZFC to force a winning strategy for either player, or for neither. This gives a new counterexample to $\Sigma^{2}_{2}$ maximality with a predicate for the nonstationary ideal on $\omega_{1}$, and an example of a consistently undetermined game of length $\omega_{1}$ with payoff definable in the second-order monadic logic of order. We also show that the determinacy of the game is consistent with Martin's Axiom but not Martin's Maximum.
---

Title: Selection and Uniformization Problems in the Monadic Theory of Ordinals: A Survey

Section 1: Introduction
Description 1: This section provides the aim and focus of the survey, discussing the methodological issues of selection and uniformization problems in monadic logic without delving into technical details or proofs.

Section 2: Notations
Description 2: This section defines the notations and terminology used throughout the paper to ensure clarity in the presentation of concepts.

Section 3: MLO
Description 3: This section introduces the vocabulary and structure of Monadic Logic of Order (MLO), including the types of variables, atomic formulas, and how formulas are constructed.

Section 4: The Monadic Theory of Countable Ordinals
Description 4: This section discusses Büchi's results on the data required to determine the monadic theory of any ordinal less than or equal to ω₁ and the algorithmic implications.

Section 5: The Selection Property in an Ordinal
Description 5: This section examines the selection property within specific ordinals, characterizing when an ordinal has the selection property and deriving implications from definable subsets.

Section 6: The Selection Problem in an Ordinal
Description 6: This section investigates the solvability of the selection problem within ordinals, presenting algorithms that decide and construct selectors for formulas in given ordinals.

Section 7: Selection over Classes of Countable Ordinals
Description 7: This section addresses the selection property and problem over various classes of countable ordinals, including definable subclasses and providing algorithmic solutions.

Section 8: Selection between First-Order and Second-Order Logics
Description 8: This section explores the selection property and problem across different fragments of MLO, comparing first-order and second-order formulas within countable ordinals.

Section 9: Selection Degrees
Description 9: This section introduces the concept of selection degrees, comparing and classifying formulas based on their selectability in various structures.

Section 10: Labeled Ordinals
Description 10: This section discusses the extensions and modifications of ordinals with additional labeled subsets and examines their impact on the selection property.

Section 11: The Church Uniformization Problem
Description 11: This section describes the Church uniformization problem, presenting both historical solutions and current open questions relating to causal uniformizers in ordinals.

Section 12: The Bounded Uniformization Problem
Description 12: This section explores a restricted version of the uniformization problem, focusing on bounded subsets and providing algorithms for their solvability.

Section 13: Open Problems
Description 13: This section concludes the survey by presenting several open questions and conjectures for future research, mainly related to the uniformization and selection problems in the monadic theory of ordinals.