From Sets to Points: Simplifying MSO Interpretations via Reparameterizations

Rabinovich, Alexander

doi:10.4230/LIPIcs.ICALP.2026.189

From Sets to Points: Simplifying MSO Interpretations via Reparameterizations

Alexander Rabinovich

Blavatnik School of Computer Science and Artificial Intelligence, Tel Aviv University, Israel

Abstract

We study the conditions under which monadic second-order (MSO) interpretations can be simplified by replacing representations of elements as tuples of arbitrary sets with representations as tuples of finite sets or points. Using reparameterizations of MSO formulas, we prove that for formulas with free finite-set variables, it is decidable whether a point reparameterization exists, and that such a reparameterization can be effectively constructed over countable chains. Moreover, over countable Dedekind-complete labeled chains, a formula with free arbitrary set variables admits a finite-set reparameterization if and only if it has at most countably many satisfying assignments. These results yield effective simplification procedures for MSO interpretations over broad classes of countable linear orders.

Keywords and phrases:

Monadic Second-Order Logic,

\mathit{MSO}

interpretation, interpretation simplification, reparameterization, decidability

Category:

Track B: Automata, Logic, Semantics, and Theory of Programming

Funding:

Alexander Rabinovich: Supported in part by Len Blavatnik and the Blavatnik Family foundation.

Copyright and License:

2012 ACM Subject Classification:

Theory of computation

\rightarrow

Logic and verification ; Theory of computation

\rightarrow

Models of computation

Acknowledgements:

I would like to thank the reviewers for their careful reading and valuable comments.

DOI:

10.4230/LIPIcs.ICALP.2026.189

Event:

53rd International Colloquium on Automata, Languages, and Programming (ICALP 2026)

Editors:

Sayan Bhattacharya, Danupon Nanongkai, Michael Benedikt, and Gabriele Puppis

Series and Publisher:

Leibniz International Proceedings in Informatics, Schloss Dagstuhl – Leibniz-Zentrum für Informatik

1 Introduction

The notion of interpretation was first systematically defined and developed in the foundational work of Tarski, Mostowski, and Robinson [11]. Since then, interpretations have become a fundamental tool in mathematical logic, where they play a central role in the study of relative definability and interpretability between theories, and in the foundations of mathematics more broadly. They are also of central importance in the foundations and philosophy of science. In contemporary model theory and theoretical computer science, interpretations are routinely used to compare the expressive power of logical formalisms and to encode one class of structures inside another, for instance by interpreting complex structures in simpler, well-understood combinatorial objects such as labeled chains or trees.

We address the following question: when can a monadic second-order¹¹1Let us recall that monadic second-order logic is an extension of first-order logic by set variables (which range over the subset of the domain of a structure), and the quantifiers over the set variables (see Section 2.2 for a formal definition). ( $\mathit{MSO}$ ) interpretation be simplified – that is, when can elements of the interpreted structure be represented by simpler objects (finite sets or points) without changing the interpreted structure?

Interpretations of $\mathfrak{A}$ in $\mathfrak{B}$

Consider three standard variants of $d$ –dimensional $\mathit{MSO}$ interpretations of a structure $\mathfrak{A}$ in a structure $\mathfrak{B}$ . In each case, an element of $\mathfrak{A}$ is coded inside $\mathfrak{B}$ by a $d$ -tuple:

Set interpretations: ( $\mathit{MSO}$ , $d$ –dimensional): each element of $\mathfrak{A}$ is represented by a $d$ -tuple of (arbitrary) subsets of $\mathfrak{B}$ .
Finite-set interpretations: ( $\mathit{MSO}$ , $d$ –dimensional): each element of $\mathfrak{A}$ is represented by a $d$ -tuple of finite subsets of $\mathfrak{B}$ .
Point interpretations: ( $\mathit{MSO}$ , $d$ –dimensional): each element of $\mathfrak{A}$ is represented by a $d$ -tuple of elements of $\mathfrak{B}$ .

A natural problem is to determine whether a given interpretation can be simplified, for instance from set interpretations to finite-set or point interpretations. In general, the domain of an interpretation over a structure $\mathfrak{B}$ is defined by a formula $\varphi(\overline{X})$ , where $\overline{X}$ is a tuple of free variables. We capture this notion of simplification using reparameterizations, a concept introduced in [3].

Definition 1.1 (Reparameterization).

Let $\varphi(\overline{X})$ be an $\mathit{MSO}$ formula and let $\mathcal{C}$ be a class of structures. A formula $G(\overline{X},\overline{Y})$ is a reparameterization of $\varphi$ over $\mathcal{C}$ if:

Same domain:

$\varphi(\overline{X})\ \equiv\ \exists\overline{Y}\,G(\overline{X},\overline{Y})$ over $\mathcal{C}$ .

Bounded preimage:

There exists $N\in\mathbb{N}$ such that, for every ${\mathcal{M}}\in\mathcal{C}$ and every parameter tuple $\overline{Y}$ ,

\bigl|\{\,\overline{X}\mid{\mathcal{M}}\models G(\overline{X},\overline{Y})\,% \}\bigr|\ \leq\ N.

We call $\overline{X}$ the domain variables and $\overline{Y}$ the image variables of $G$ . The reparameterization is functional if it defines the graph of a partial function: $\forall\overline{X}\ \exists^{\leq 1}\overline{Y}\;G(\overline{X},\overline{Y}).$

A reparameterization $G(\overline{X},\overline{Y})$ is $m$ -to- $d$ -dimensional if $\overline{X}$ is an $m$ -tuple and $\overline{Y}$ is a $d$ -tuple. It is a set-to-finite-set (respectively, finite-set-to-point) reparameterization if $\overline{X}$ ranges over tuples of sets (respectively, finite sets) and $\overline{Y}$ over tuples of finite sets (respectively, elements).

Intuition.

A reparameterization replaces the original parameters $\overline{X}$ by auxiliary parameters $\overline{Y}$ in such a way that each $\overline{Y}$ corresponds to only boundedly many $\overline{X}$ . In the functional case, each $\overline{X}$ determines at most one $\overline{Y}$ .

Suppose that $\varphi(\overline{X})$ (with $|\overline{X}|=m$ ) admits a reparameterization $G(\overline{X},\overline{y})$ whose image variables $\overline{y}$ are first-order and $|\overline{y}|=d$ . Then any interpretation whose domain is defined by $\varphi$ can be simplified to a $d$ –dimensional point interpretation (see Appendix A).

Bojańczyk [2] proved that, over finite words, it is decidable whether an $\mathit{MSO}$ formula with $m$ free first-order variables admits an $m$ -to- $d$ -dimensional point-to-point reparameterization. Gallot–Lhote–Nguyen [3] studied finite-set-to-point reparameterizations over finite words and trees. We prove that the decidability results of [3] extend to the setting of arbitrary countable labeled linear orders (chains): given an $\mathit{MSO}$ formula $\varphi$ with free finite-set variables, it is decidable whether $\varphi$ admits a point reparameterization over countable chains.

Finally, building on [1], we show that it is decidable whether an $\mathit{MSO}$ formula $\varphi$ with free set variables admits a set-to-finite-set reparameterization over countable Dedekind-complete labeled chains.

Our contributions and paper organization

We develop a uniform approach to simplifying MSO interpretations via reparameterizations over countable labeled chains. Our main results are as follows. First, for $\mathit{MSO}$ formulas whose free variables are finite-set variables, we show that it is decidable whether the formula admits a reparameterization by first-order (point) image variables over an $\mathit{MSO}$ -definable class of countable labeled chains; moreover, whenever such a reparameterization exists, a functional one can be effectively constructed (see Theorem 3.1). Second, building on results of [1], we obtain an effective characterization of when a formula with free set variables admits a finite-set reparameterization over countable Dedekind-complete labeled chains: this holds exactly when the formula has at most countably many satisfying assignments in every structure from the class (see Theorem 4.2). Together, these results yield effective procedures for simplifying set interpretations to finite-set interpretations, and finite-set interpretations to point interpretations.

The paper is organized as follows. Section 2 contains preliminaries. Section 3 contains our main result and studies finite-set-to-point reparameterizations. It provides an effective characterization of when such reparameterizations exist over countable chains. Section 4 studies reparameterizations from arbitrary sets to finite sets and establishes the corresponding characterization. Section 5 contains the conclusion and further results. In Appendix A, we recall the standard definition of interpretation and explain how reparameterizations can be used to simplify interpretations. Although not strictly necessary for our main results, this material provides useful background and motivation for the reparameterization problem. Some proofs are deferred to the appendix.

2 Preliminaries

Here we recall standard notions concerning chains [9] and monadic second-order logic [7, 5, 12], and introduce basic tools from the composition method [10, 5] used throughout the paper.

2.1 Chains

A $k$ -chain is a structure $\mathcal{M}=(M,<,P_{1},\dots,P_{k}),$ where $(M,<)$ is a linear order and $\overline{P}=(P_{1},\dots,P_{k})$ is a $k$ -tuple of monadic predicates. When $k$ is clear from the context (or irrelevant), we simply say chain or labeled chain instead of $k$ -chain.

An interval is a subset $I\subseteq M$ such that whenever $b,c\in I$ and $b<d<c$ , we have $d\in I$ . We denote by $\mathcal{M}\!\upharpoonright I$ the induced substructure on $I$ .

2.2 Monadic Second-Order Logic

We work in monadic second-order logic ( $\mathit{MSO}$ ) over the signature of $\ell$ -chains

\sigma_{\ell}:=\{<,P_{1},\dots,P_{\ell}\}.

First-order variables $x,y,\dots$ range over elements, and second-order variables $X,Y,\dots$ range over subsets of the domain. Atomic formulas are $x<y$ , $x=y$ , $P_{i}(x)$ , and $X(x)$ . Formulas are built from atomic formulas using Boolean connectives and quantifiers $\exists x,\forall x,\exists X,\forall X$ . We also use second-order variables that are intended to range over finite sets. Since finiteness is $\mathit{MSO}$ -definable over linear orders, this semantic restriction can be enforced syntactically by relativizing quantification to the formula expressing finiteness.

We recall the following classical result of Rabin [7].

Theorem 2.1 (Rabin, 1969 [7]).

The monadic second-order theory of countable linear orders is decidable.

2.3 Types

The quantifier rank ${\mathrm{qr}}(\varphi)$ of an $\mathit{MSO}$ formula $\varphi$ is the maximal nesting depth of quantifiers. For $r,k\in\mathbb{N}$ , let ${\mathfrak{Form}^{r}_{k}}(\sigma_{\ell})$ denote the set of $\mathit{MSO}$ formulas of quantifier rank at most $r$ over the signature $\sigma_{\ell}$ , with free set variables $X_{1},\dots,X_{k}$ .

For $\ell$ -chains ${\mathcal{M}}_{1}$ and ${\mathcal{M}}_{2}$ , and $k$ -tuples $\overline{A_{1}}=(A_{1,1},\dots,A_{1,k})$ with $A_{1,i}\subseteq M_{1}$ and $\overline{A_{2}}=(A_{2,1},\dots,A_{2,k})$ with $A_{2,i}\subseteq M_{2}$ , we write $({\mathcal{M}}_{1},\overline{A_{1}})\equiv^{r}_{k}({\mathcal{M}}_{2},\overline% {A_{2}})$ if $({\mathcal{M}}_{1},\overline{A_{1}})$ and $({\mathcal{M}}_{2},\overline{A_{2}})$ satisfy the same formulas in ${\mathfrak{Form}^{r}_{k}}(\sigma_{\ell})$ . This is an equivalence relation with finitely many equivalence classes. If ${\mathcal{M}}$ is an $\ell$ -chain and $\overline{A}=(A_{1},\dots,A_{k})$ is a $k$ -tuple of subsets of $M$ , then we may view $({\mathcal{M}},\overline{A})$ as an $(\ell+k)$ -chain, namely

({\mathcal{M}},\overline{A})\ :=\ (M,<,P_{1},\dots,P_{\ell},A_{1},\dots,A_{k}).

The following lemma implies that every $\equiv^{r}_{k}$ -equivalence class is definable by a formula in ${\mathfrak{Form}^{r}_{k}}(\sigma_{\ell})$ .

Lemma 2.2 (Hintikka, [6]).

For every $r,k,\ell\in\mathbb{N}$ there exists a finite, effectively computable set $H^{r}_{k}\subseteq{\mathfrak{Form}^{r}_{k}}(\sigma_{\ell})$ such that:

1.

The disjunction $\bigvee_{\tau\in H^{r}_{k}}\tau$ is valid.
2.

If $\tau,\tau^{\prime}\in H^{r}_{k}$ are distinct, then $\tau\wedge\tau^{\prime}$ is unsatisfiable.
3.

Given $\varphi\in{\mathfrak{Form}^{r}_{k}}(\sigma_{\ell})$ , one can effectively compute a set $H_{\varphi}\subseteq H^{r}_{k}$ such that $\varphi$ is equivalent to the disjunction of the formulas in $H_{\varphi}$ .

By (1) and (2), for every $\sigma_{\ell}$ -structure ${\mathcal{M}}$ and every $k$ -tuple $\overline{A}\subseteq M$ , there exists a unique $\tau\in H^{r}_{k}$ such that ${\mathcal{M}}\models\tau(\overline{A}).$ We denote this formula by ${\mathrm{type}^{r}_{k}}({\mathcal{M}},\overline{A})$ and call it the $(r,k)$ -type of $({\mathcal{M}},\overline{A})$ . When $k$ is clear from the context, we write ${\mathrm{type}^{r}}({\mathcal{M}},\overline{A})$ and call it the $r$ -type of $({\mathcal{M}},\overline{A})$ . When $({\mathcal{M}},\overline{A})$ is clear from the context and $I\subseteq M$ is an interval, we write ${\mathrm{type}^{r}}(I)$ for the $r$ -type of the induced substructure $({\mathcal{M}},\overline{A})\!\upharpoonright I$ .

We define the set of $(r,k)$ -types to be the set of satisfiable formulas in $H^{r}_{k}$ .

2.4 Concatenation of Chains and Sum of Types

Given $l$ -chains $\mathfrak{A}$ and $\mathfrak{B}$ , their sum (or concatenation) $\mathfrak{A}+\mathfrak{B}$ is obtained by placing $\mathfrak{A}$ before $\mathfrak{B}$ . The following proposition implies that $\equiv^{r}_{k}$ is a congruence with respect to concatenation.

Proposition 2.3 (Sum of types [10]).

There is a computable function that, given $r$ and $k$ , returns an operation $+$ on $\mathit{Hin}^{r}_{k}$ such that

{\mathrm{type}^{r}}(\mathfrak{A}+\mathfrak{B})={\mathrm{type}^{r}}(\mathfrak{A% })+{\mathrm{type}^{r}}(\mathfrak{B}).

For every $r,k\in\mathbb{N}$ , the set $\mathit{Hin}^{r}_{k}$ , equipped with the sum operation $+$ , forms a finite semigroup.

Lemma 2.4 ( $r$ -local normal form).

Let $\psi(\overline{{X}},\bar{z})$ be an $\mathit{MSO}$ formula of quantifier depth at most $q$ , where $\overline{{X}}$ is a tuple of free monadic second-order variables and $\bar{z}=(z_{1},\dots,z_{m})$ is a tuple of free first-order variables. For every $r\geq q+2$ , the formula

\psi(\overline{{X}},\bar{z})\ \wedge\ \bigwedge_{i<m}z_{i}<z_{i+1}

is equivalent to a finite positive Boolean combination of formulas asserting the $r$ -types of the induced subchains on the intervals

(-\infty,z_{1}),\quad[z_{i},z_{i+1}),\quad\text{and}\quad[z_{m},\infty),

viewed as substructures of the expansion $({\mathcal{M}},\overline{{X}})$ . Moreover, this Boolean combination is computable from $\psi$ .

3 Finite-Set-to-Point Reparameterizations

Gallot–Lhote–Nguyen [3] studied finite-set-to-point reparameterizations over finite trees, using automata-theoretic techniques. In this paper, we extend their decidability results (Theorem 3.12 in [3]) beyond finite structures and establish them for arbitrary countable linear orders.

Theorem 3.1 (Finite-set-to-point reparameterization over countable chains).

Let $\mathcal{C}$ be an $\mathit{MSO}$ -definable class of labeled countable linear orders, and let $\varphi(\overline{X})$ be an $\mathit{MSO}$ formula whose free variables $\overline{X}$ are finite-set variables. It is decidable whether, over $\mathcal{C}$ , $\varphi$ admits a reparameterization by a formula using only first-order image variables. In addition, whenever such a reparameterization exists, there also exists a functional reparameterization using only first-order image variables, and such a functional reparameterization is effectively computable from $\varphi$ and an $\mathit{MSO}$ definition of $\mathcal{C}$ .

Throughout this section we write $\overline{{X}}$ for a tuple of finite set variables.

Lemma 3.2 (Reducing to the full class of countable chains).

Let $\psi$ be an $\mathit{MSO}$ sentence defining a class $\mathcal{C}_{\psi}:=\{\,{\mathcal{M}}\text{ countable chain}\mid{\mathcal{M}}% \models\psi\,\}$ . Let $\varphi(\overline{X})$ be an $\mathit{MSO}$ formula. Then the following are equivalent:

1.

$\varphi$ admits a reparameterization by a formula with only first-order image variables over $\mathcal{C}_{\psi}$ .
2.

$\varphi\wedge\psi$ admits a reparameterization by a formula with only first-order image variables over the class of all countable chains.

Consequently, without loss of generality we may carry out all reparameterization arguments over the full class of countable chains by replacing $\varphi$ with $\varphi\wedge\psi$ .

3.1 Idempotent obstruction to point reparameterization

Definition 3.3 (Idempotent obstruction to point reparameterization).

Let $\varphi(\overline{X})$ be an $\mathit{MSO}$ formula of quantifier depth $q$ . We say that $\varphi$ has an idempotent obstruction to point reparameterization if there exist satisfiable $q$ -types $\tau,\tau_{1},\tau_{2}$ such that:

1.

$\tau$ is idempotent, i.e., $\tau+\tau=\tau$ ;
2.

$\tau$ is realized at least twice in some structure ${\mathcal{M}}$ , i.e.,

${\mathcal{M}}\models\exists^{\geq 2}\,\overline{X}\,\tau(\overline{X});$
3.

one of the following types implies $\varphi(\overline{X})$ :

$\tau,\quad\tau_{1}+\tau,\quad\tau+\tau_{2},\quad\tau_{1}+\tau+\tau_{2}.$

Lemma 3.4 (Obstruction lemma).

Let $\varphi(\overline{X})$ be an $\mathit{MSO}$ formula.

If $\varphi$ has an idempotent obstruction to point reparameterization, then $\varphi$ admits no reparameterization whose image variables are first-order.

Furthermore, over countable chains, the existence of such an obstruction is decidable.

Proof.

We first address decidability. By Theorem 2.1, Lemma 2.2, and Proposition 2.3, one can effectively enumerate all $q$ -types in $\mathit{Hin}^{q}_{k}$ , test idempotency ( $\tau+\tau=\tau$ ), and decide whether $(\tau_{1}+\tau+\tau_{2})\to\varphi$ holds for some $q$ -types $\tau_{1},\tau,\tau_{2}$ . Moreover, since the $\mathit{MSO}$ theory of countable chains is decidable by Theorem 2.1, we can also check whether $\tau$ is realized at least twice in some structure ${\mathcal{M}}$ , that is, whether $\exists^{\geq 2}\,\overline{X}\,\tau(\overline{X})$ is satisfiable.

We now prove the nonexistence of point reparameterizations in the presence of an idempotent obstruction.

Assume toward a contradiction that $\varphi$ admits a reparameterization by a formula with only first-order image variables. Thus there exists an $\mathit{MSO}$ formula

G(\overline{{X}},\bar{y})\qquad\text{with}\qquad\bar{y}=(y_{1},\dots,y_{d})

such that:

(i)

(Same domain) for all structures,

$\varphi(\overline{{X}})\ \equiv\ \exists\bar{y}\,G(\overline{{X}},\bar{y}),$
(ii)

(Bounded preimage) there exists $N\in\mathbb{N}$ such that for every structure ${\mathcal{M}}$ and every tuple $\bar{b}\in M^{d}$ ,

$\bigl|\{\;\bar{A}\mid{\mathcal{M}}\models G(\bar{A},\bar{b})\;\}\bigr|\leq N.$

We will use the following claim, whose proof is given in Appendix B.

Claim 3.5.

For every $r>q$ and every idempotent $q$ -type $\tau(\overline{X})$ , there exists an idempotent $r$ -type $\tau^{\prime}(\overline{X})$ such that $\tau^{\prime}\rightarrow\tau$ . Moreover, if $\exists^{\geq 2}\,\overline{X}\,\tau(\overline{X})$ is satisfiable, then $\exists^{\geq 2}\,\overline{X}\,\tau^{\prime}(\overline{X})$ is also satisfiable.

Step 1: Fix realizations of the types.

By assumption, there exist ${\mathcal{M}}_{1},{\mathcal{M}}_{2}$ and assignments $\bar{A}_{1},\bar{A}_{2}$ realizing $\tau_{1}(\overline{{X}})$ and $\tau_{2}(\overline{{X}})$ , respectively.

Now let $r$ be greater than both $q$ and the quantifier depth of $G$ . Choose an idempotent $r$ -type $\tau^{\prime}(\overline{{X}})$ such that $\tau^{\prime}\rightarrow\tau$ and

{\mathcal{M}}\models\exists^{\geq 2}\,\overline{X}\,\tau^{\prime}(\overline{X})

for some chain ${\mathcal{M}}$ . Such an $r$ -type exists by ˜3.5.

Also, in the given structure ${\mathcal{M}}$ pick two distinct assignments

\bar{A}^{(0)}\neq\bar{A}^{(1)}

such that both realize $\tau^{\prime}(\overline{{X}})$ in ${\mathcal{M}}$ , and hence also realize $\tau(\overline{{X}})$ in ${\mathcal{M}}$ .

Step 2: Build many witnesses using idempotence.

For $K\in\mathbb{N}$ , form the ordered sum

{\mathcal{M}}^{K}\ :=\ {\mathcal{M}}_{1}\ +\ \underbrace{{\mathcal{M}}\ +\ % \cdots\ +\ {\mathcal{M}}}_{K\ \text{copies}}\ +\ {\mathcal{M}}_{2}.

For every subset $S\subseteq\{1,\dots,K\}$ define an assignment $\bar{A}^{S}$ of $\overline{{X}}$ in ${\mathcal{M}}^{K}$ as follows:

$\blacksquare$

on ${\mathcal{M}}_{1}$ use $\bar{A}_{1}$ ;
$\blacksquare$

on ${\mathcal{M}}_{2}$ use $\bar{A}_{2}$ ;
$\blacksquare$

on the $\ell$ -th middle copy of ${\mathcal{M}}$ use $\bar{A}^{(1)}$ if $\ell\in S$ , and use $\bar{A}^{(0)}$ otherwise.

Since $\tau$ is idempotent, the $q$ -type of the concatenation of any number of copies of $\tau$ is again $\tau$ . Therefore, for every $S$ , the $q$ -type of $\bar{A}^{S}$ in ${\mathcal{M}}^{K}$ is $\tau_{1}+\tau+\tau_{2}$ , and hence

{\mathcal{M}}^{K}\models\varphi(\bar{A}^{S}).

By (i), for every $S$ there exists some tuple $\bar{b}$ such that

{\mathcal{M}}^{K}\models G(\bar{A}^{S},\bar{b}).

Step 3: Pigeonhole argument.

Choose $K>(d+1)\cdot(N+1)$ . Fix $S\subseteq\{1,\dots,K\}$ . By $(\ddagger_{S})$ , there exists a $d$ -tuple $\bar{b}$ such that

{\mathcal{M}}^{K}\models G(\bar{A}^{S},\bar{b}).

Since $\bar{b}$ consists of $d$ elements, it partitions the $K$ middle blocks into at most $d+1$ consecutive regions. By the pigeonhole principle, there exists a region containing at least $N+1$ consecutive copies ${\mathcal{M}}_{i},\dots,{\mathcal{M}}_{i+N}$ such that none of the coordinates of $\bar{b}$ lies in this region.

For every subset $S^{\prime}\subseteq\{i,\dots,i+N\}$ , let $S\triangle S^{\prime}$ denote the symmetric difference. By locality (Lemma 2.4), the truth of $G(\bar{A},\bar{b})$ depends only on the $r$ -types of the substructures over the intervals determined by $\bar{b}$ . Replacing $\bar{A}^{(0)}$ by $\bar{A}^{(1)}$ (or vice versa) inside the chosen region ${\mathcal{M}}_{i},\dots,{\mathcal{M}}_{i+N}$ does not change these $r$ -types, since the region is disjoint from the tuple $\bar{b}$ . Hence

{\mathcal{M}}^{K}\models G(\bar{A}^{S\triangle S^{\prime}},\bar{b})

for every such $S^{\prime}$ .

There are $2^{N+1}$ choices of $S^{\prime}$ , and hence more than $N$ distinct assignments $\bar{A}^{S\triangle S^{\prime}}$ in the preimage of $\bar{b}$ , contradicting $(\ast)$ . $\hfill\blacktriangleleft$

3.2 From the absence of an idempotent obstruction to point reparameterization

Our main technical result shows that, in the absence of an idempotent obstruction, the formula $\varphi(\overline{X})$ admits a point reparameterization.

Theorem 3.6 (Main).

If $\varphi(\overline{X})$ has no idempotent obstruction to point reparameterization, then $\varphi$ admits a functional reparameterization by an $\mathit{MSO}$ formula whose image variables are first-order. Furthermore, such a reparameterization can be effectively constructed from $\varphi$ .

Theorem 3.1 is an immediate consequence of Lemma 3.2, Lemma 3.4 and Theorem 3.6.

$\blacktriangleright$ Remark (Countability Assumption).

It is worth emphasizing that the structural characterization of idempotent obstructions to point reparameterization, given in Lemma 3.4 and Theorem 3.6, holds over arbitrary chains. The restriction to countable chains in this paper is used only to ensure decidability in Lemma 3.4 and the effectiveness of the construction in Theorem 3.6.

Proof overview

The proof of Theorem 3.6 proceeds in four steps.

Step 1: Encoding by $𝒒$ -type words.

Given a chain ${\mathcal{M}}$ and a tuple $\overline{A}$ of finite subsets of its domain, we split ${\mathcal{M}}$ along the elements of $\overline{A}$ into intervals and associate to each interval its $q$ -type. This yields a word $u=u_{0}\dots u_{\ell}$ over a finite alphabet of $q$ -types.

Step 2: Uniformly bounded factorization.

By Lemma 3.13, the word $u$ admits a restricted factorization $s$ of uniformly bounded length, which is again a word over $q$ -types. Hence every instance $({\mathcal{M}},\overline{A})$ is associated with one of finitely many such factorization words.

Step 3: Local reparameterizations.

For each such restricted factorization word $s$ , we construct an $\mathit{MSO}$ formula $G_{s}(\overline{X},\overline{y})$ that reparameterizes $\varphi$ on the class of structures $({\mathcal{M}},\overline{A})$ whose associated $q$ -type word admits $s$ as a restricted factorization. The assumption that $\varphi$ has no idempotent obstruction ensures that this construction is well defined and yields a functional reparameterization.

Step 4: Global construction.

We combine the finitely many formulas $G_{s}$ into a single formula $G(\overline{X},\overline{y})$ , which yields a uniform reparameterization.

Definition 3.7 ( $q$ -type word associated with a labeled chain).

Let ${\mathcal{M}}$ be a labeled linear order (chain), and let $\overline{A}=(A_{1},\dots,A_{k})$ be a $k$ -tuple of finite subsets of its domain. Let

A:=\bigcup_{i=1}^{k}A_{i},

and let $a_{1}<\cdots<a_{\ell}$ be the increasing enumeration of the distinct elements of $A$ (so $\ell=|A|$ ). Set $a_{0}:=-\infty$ and $a_{\ell+1}:=+\infty$ as formal endpoints.

Fix $q\in\mathbb{N}$ , and let $X_{1},\dots,X_{k}$ be set variables corresponding to $A_{1},\dots,A_{k}$ . For each $i=0,\dots,\ell$ , let $u_{i}$ be the $q$ -type (with free variables $X_{1},\dots,X_{k}$ ) of the structure obtained by restricting $({\mathcal{M}},\overline{A})$ to the interval

[a_{i},a_{i+1}):=\{\,x\mid a_{i}\leq x<a_{i+1}\,\},

where the order is restricted to $[a_{i},a_{i+1})$ and each $X_{j}$ is interpreted as $A_{j}\cap[a_{i},a_{i+1})$ .

The $q$ -type word associated with $({\mathcal{M}},\overline{A})$ , denoted by $\operatorname{\mathit{type}^{q}-\mathit{word}}({\mathcal{M}},\overline{A})$ , is the word

u:=u_{0}u_{1}\cdots u_{\ell}

over the finite alphabet of $q$ -types with free variables $X_{1},\dots,X_{k}$ . If $A=\varnothing$ , then $\ell=0$ and $u=u_{0}$ .

The next lemma follows immediately from the definition.

Lemma 3.8.

Assume $q\geq 2$ . Let $u_{0}u_{1}\dots u_{\ell}$ be a $q$ -type word associated with a labeled chain as in Definition 3.7. Then, for every chain ${\mathcal{M}}$ and every tuple $\overline{A}$ :

1.

If ${\mathcal{M}},\overline{A}\models u_{0}$ , then $\bigcup_{j}A_{j}=\emptyset$ .
2.

For every $i>0$ , if ${\mathcal{M}},\overline{A}\models u_{i}$ , then $\bigcup_{j}A_{j}$ is a singleton consisting of the minimal element of ${\mathcal{M}}$ . Moreover, there exists a unique tuple $\overline{B}$ such that ${\mathcal{M}},\overline{B}\models u_{i}$ .

(The assumption $q\geq 2$ is necessary to express that an element is minimal.)

A key step in the proof is to replace $\operatorname{\mathit{type}^{q}-\mathit{word}}({\mathcal{M}},\overline{A})$ by a finite uniformly bounded object that still captures the semigroup information relevant to our argument. This leads us to the notion of the restricted factorization word defined below. Intuitively, restricted factorizations compress long type words while preserving the semigroup structure relevant to reparameterization.

Definition 3.9 (Restricted Factorization).

Let $(S,+)$ be a finite semigroup. A word $e_{0}\dots e_{m-1}\in S^{+}$ is a restricted factorization of a word $u=u_{0}\dots u_{\ell-1}$ with $u_{i}\in S$ if there exist words $w_{0},\dots,w_{m-1}$ such that

u=w_{0}\dots w_{m-1},

and for each $i$ , the sum of the letters in $w_{i}$ equals $e_{i}$ , and either $w_{i}$ is a single letter or $e_{i}$ is idempotent.

Note that a word $u$ may admit several distinct restricted factorizations. Moreover, even for a fixed restricted factorization $e_{0}\dots e_{m-1}$ of $u$ , there may be several choices of words $w_{0},\dots,w_{m-1}$ witnessing it.

By Ramsey’s theorem (see, e.g., [4]), we obtain the following lemma; its proof is deferred to Appendix C.

Lemma 3.10 (Uniform bound on restricted factorizations).

For every finite semigroup $(S,+)$ , there exists $N_{S}\in\mathbb{N}$ such that every word over $S$ admits a restricted factorization $e_{0}\dots e_{m}$ with $m\leq N_{S}$ .

As a consequence of Lemma 3.8 and Definition 3.9, we obtain the following properties of restricted factorization words.

Lemma 3.11 (Properties of restricted factorization words).

Assume $q\geq 2$ . Let $u_{0}u_{1}\dots u_{\ell}$ be a $q$ -type word associated with a labeled chain, and let $s=e_{0}\dots e_{m}$ be a restricted factorization of $u_{0}u_{1}\dots u_{\ell}$ . Then:

(a)

For $i>0$ , if ${\mathcal{M}},\overline{A}\models e_{i}$ , then ${\mathcal{M}}$ has a minimal element $m$ , and this element belongs to $\bigcup_{j=1}^{k}A_{j}$ ; moreover, either $e_{i}$ is idempotent, or $\bigcup_{j=1}^{k}A_{j}=\{m\}$ and $\overline{A}$ is the unique tuple such that ${\mathcal{M}},\overline{A}\models e_{i}$ .
(b)

Either $e_{0}$ is idempotent, or for every ${\mathcal{M}},\overline{A}\models e_{0}$ we have $\bigcup_{j}A_{j}=\emptyset$ .

Notation.

$\mathit{RFW}^{q}_{k}$ denotes the set of words over $\mathit{Hin}^{q}_{k}$ satisfying properties Lemma 3.11(a)–(b); we call its elements restricted factorization words.

Definition 3.12 (Models of a restricted factorization word).

Let $s\in\mathit{RFW}^{q}_{k}$ . Define

\mathit{Mod}(s):=\Bigl\{\,({\mathcal{M}},\overline{A})\ \Bigm|\ \begin{aligned% } &\overline{A}\text{ is a $k$-tuple of finite subsets of }{\mathcal{M}},\\ &\text{and }s\text{ is a restricted factorization of }\operatorname{\mathit{% type}^{q}-\mathit{word}}({\mathcal{M}},\overline{A})\end{aligned}\,\Bigr\}.

Applying Lemma 3.10 to the semigroup of $(q,k)$ -types, we obtain the following.

Lemma 3.13 (Short factorization word property).

For every $q, k$ there exists $N_{q,k}$ such that for every chain ${\mathcal{M}}$ and every $k$ -tuple of finite subsets $\overline{A}$ , there exists $s\in\mathit{RFW}^{q}_{k}$ of length at most $N_{q,k}$ such that $({\mathcal{M}},\overline{A})\in\mathit{Mod}(s).$

The next definition introduces a formula that will be crucial for the proof.

Definition 3.14 (Reparameterization induced by a factorization word).

Let $s\in\mathit{RFW}^{q}_{k}$ be a restricted factorization word over $\mathit{Hin}^{q}_{k}$ . We define, by induction on $|s|$ , an $\mathit{MSO}$ formula

H_{s}(\overline{X},\overline{y}),

where $\overline{y}$ is a tuple of first-order variables. This formula will be used to obtain a reparameterization of $\tau(\overline{X})$ - the sum of the letters of $s$ in the semigroup of $q$ -types, provided that the construction does not fail.

Inductive definition of $H_{s}$ .

Base case. Suppose $s$ consists of a single letter $\tau(\overline{X})$ .

Case 1 (idempotent).

Assume that $\tau(\overline{X})$ is idempotent, i.e. $\tau+\tau=\tau$ .

$\blacksquare$

If $\exists^{\geq 2}\,\overline{X}\,\tau(\overline{X})$ is satisfiable, then by Lemma 3.4 no reparameterization by first-order image variables exists for $\tau(\overline{X})$ ; we declare the construction to fail.
$\blacksquare$

Otherwise, define $H_{s}(\overline{X}):=\tau(\overline{X}).$

Case 2 (non-idempotent letter).

Assume that $s$ consists of a single non-idempotent letter $\tau(\overline{X})$ . By Lemma 3.11, either $\tau(\overline{X})\rightarrow\bigcup_{j}X_{j}=\emptyset$ or $\tau(\overline{X})\rightarrow\bigcup_{j}X_{j}$ contains exactly one element. In the former case, set $H_{s}(\overline{X}):=\tau(\overline{X}),$ and in the latter, $H_{s}(\overline{X},y):=\tau(\overline{X})\wedge\bigvee_{j}X_{j}(y).$

Inductive step. Let $s=e_{0}\dots e_{m+1}$ and set $s_{1}:=e_{0}\dots e_{m}$ . Let $H_{s_{1}}(\overline{X},\overline{y}_{1})$ and $H_{e_{m+1}}(\overline{X},\overline{y}_{2})$ be the corresponding formulas.

We write $\overline{y}_{1}<y$ to mean that all coordinates of $\overline{y}_{1}$ are $<y$ , and define $\overline{y}_{2}\geq y$ analogously.

Define

	$\displaystyle H_{s}(\overline{X},\overline{y}_{1},y,\overline{y}_{2})=\;($	$\displaystyle\ \overline{y}_{1}<y\ \wedge\ \overline{y}_{2}\geq y\ \wedge\ % \bigvee_{j}X_{j}(y)$
		$\displaystyle\wedge\ (H_{s_{1}}(\overline{X},\overline{y}_{1}))^{<y}\ \wedge\ % (H_{e_{m+1}}(\overline{X},\overline{y}_{2}))^{\geq y}).$

Here, for a formula $H$ , $H^{<y}$ (resp. $H^{\geq y}$ ) denotes the standard relativization of all quantifiers to elements satisfying $<y$ (resp. $\geq y$ ). Equivalently, in the first line of the definition of $H_{s}$ , one could replace the conjunct $\overline{y}_{2}\geq y$ by the requirement that $y$ is the minimal element among the coordinates of $\overline{y}_{2}$ . By construction, the tuple of image variables $\overline{y}$ in $H_{s}(\overline{X},\overline{y})$ may be empty.

Lemma 3.15 (Properties of $H_{s}$ ).

(Bounded dimension)

The number of first-order variables in $\overline{y}$ used by $H_{s}(\overline{X},\overline{y})$ is at most $2|s|$ .

(Range restriction)

$H_{s}(\overline{X},\overline{y})$ implies that $\overline{y}\subseteq\bigcup_{j}X_{j}$ .

(Bounded preimage)

For every chain ${\mathcal{M}}$ and every tuple $\overline{b}$ ,

\bigl|\{\,\overline{A}\mid{\mathcal{M}}\models H_{s}(\overline{A},\overline{b}% )\,\}\bigr|\ \leq\ 1.

Lemma 3.15 is proved by induction on the length of $s$ .

Note that $H_{s}$ is not necessarily functional. However, one can enforce functionality by selecting the lexicographically minimal tuple $\overline{y}$ satisfying $H_{s}(\overline{X},\overline{y})$ . Such a minimum exists by the range restriction property (see Lemma 3.15) and because $\overline{X}$ is a tuple of finite sets. Define

G_{s}(\overline{X},\overline{y})\;:=\;H_{s}(\overline{X},\overline{y})\ \wedge% \ \forall\overline{z}\,\bigl(H_{s}(\overline{X},\overline{z})\rightarrow% \overline{y}\leq_{\mathrm{lex}}\overline{z}\bigr).

By construction, $G_{s}(\overline{X},\overline{y})$ defines the graph of a partial function, i.e., for every $\overline{X}$ there is at most one tuple $\overline{y}$ such that $G_{s}(\overline{X},\overline{y})$ holds. In particular, $G_{s}$ yields a functional reparameterization over $\mathit{Mod}(s)$ .

Lemma 3.16.

Assume that $s\in\mathit{RFW}^{q}_{k}$ does not contain an idempotent $\tau(\overline{X})$ such that $\exists^{\geq 2}\,\overline{X}\,\tau(\overline{X})$ is satisfiable. Then $H_{s}$ and $G_{s}$ are well defined, and the following hold:

(Functionality)

If $({\mathcal{M}},\overline{A})\in\mathit{Mod}(s)$ , then ${\mathcal{M}},\overline{A}\models\exists!\,\overline{y}\;G_{s}(\overline{X},% \overline{y}).$

(Completeness)

${\mathcal{M}},\overline{A}\models\exists\overline{y}\;G_{s}(\overline{X},% \overline{y})$ iff $({\mathcal{M}},\overline{A})\in\mathit{Mod}(s).$

(Bounded preimage)

For every chain ${\mathcal{M}}$ and every tuple $\overline{b}$ ,

\bigl|\{\,\overline{A}\mid{\mathcal{M}}\models G_{s}(\overline{A},\overline{b}% )\,\}\bigr|\ \leq\ 1.

We are now ready to prove Theorem 3.6.

Proof of Theorem 3.6.

Let $\varphi(\overline{X})$ be a formula of quantifier depth at most $q\geq 2$ . Assume that there is no idempotent obstruction to point reparameterization of $\varphi(\overline{X})$ .

Let

\mathcal{S}_{\varphi}\;:=\;\{\,s\in\mathit{RFW}^{q}_{k}\mid\mu_{q}(s)% \Rightarrow\varphi\ \text{and}\ |s|\leq N_{q,k}\,\},

where $\mu_{q}(s)$ denotes the sum of the letters of $s$ in the semigroup of $q$ -types, and $N_{q,k}$ is the bound given by Lemma 3.13. The condition $\mu_{q}(s)\Rightarrow\varphi$ is equivalent to the fact that $\varphi$ holds in every structure in $\mathit{Mod}(s)$ .

Assume $s\in\mathcal{S}_{\varphi}$ . By the assumption, there is no idempotent obstruction to point reparameterization of $\varphi(\overline{X})$ . Hence, $s$ does not contain an idempotent $\tau(\overline{X})$ such that $\exists^{\geq 2}\,\overline{X}\,\tau(\overline{X})$ is satisfiable, and therefore, by Lemma 3.16, the construction of $G_{s}$ does not fail for any $s\in\mathcal{S}_{\varphi}$ .

Fix an arbitrary linear order on the finite set $\mathcal{S}_{\varphi}$ :

\mathcal{S}_{\varphi}=\{s_{1}<s_{2}<\cdots<s_{n}\}.

For $i=1,\dots,n$ , define

G_{i}(\overline{X},\overline{y})\;:=\;G_{s_{i}}(\overline{X},\overline{y}_{s_{% i}})\ \wedge\ \bigwedge_{j<i}\neg\exists\overline{y}_{s_{j}}\,G_{s_{j}}(% \overline{X},\overline{y}_{s_{j}}),

where all tuples of image variables are padded to a common arity if necessary. Thus, $G_{i}$ holds precisely when $i$ is the least index such that $G_{s_{i}}(\overline{X},\overline{y}_{s_{i}})$ holds.

Finally, define

G(\overline{X},\overline{y})\;:=\;\bigvee_{i=1}^{n}G_{i}(\overline{X},% \overline{y}).

By construction and Lemma 3.16, $G$ is functional and has preimage bound $1$ .

It remains to show that $\exists\overline{y}\,G(\overline{X},\overline{y})$ is equivalent to $\varphi(\overline{X})$ .

( $\Rightarrow$ ) Assume that ${\mathcal{M}}\models G(\overline{A},\overline{b})$ . Then ${\mathcal{M}}\models G_{s}(\overline{A},\overline{b}_{s})$ for some $s\in\mathcal{S}_{\varphi}$ . By completeness (Lemma 3.16), $({\mathcal{M}},\overline{A})\in\mathit{Mod}(s)$ . Hence, by the definition of $\mathcal{S}_{\varphi}$ , we obtain ${\mathcal{M}},\overline{A}\models\varphi$ .

( $\Leftarrow$ ) Assume that ${\mathcal{M}}\models\varphi(\overline{A})$ . By Lemma 3.13, there exists $s\in\mathcal{S}_{\varphi}$ such that $({\mathcal{M}},\overline{A})\in\mathit{Mod}(s)$ . Since $\varphi$ has no idempotent obstruction, the construction of $G_{s}$ does not fail. By Lemma 3.16, it follows that

{\mathcal{M}},\overline{A}\models\exists\overline{y}\,G_{s}(\overline{X},% \overline{y}),

and hence ${\mathcal{M}},\overline{A}\models\exists\overline{y}\,G(\overline{X},\overline% {y})$ .

Combining the two implications, we conclude that $\varphi$ and $\exists\overline{y}G$ are equivalent and hence $G$ is a functional reparameterization whose image variables are all first-order. $\hfill\blacktriangleleft$

4 Reparameterization of arbitrary sets by finite sets

Cardinality obstruction

By a simple cardinality argument, if there are uncountably many tuples satisfying $\varphi(\overline{X})$ over a countable chain ${\mathcal{M}}$ , then $\varphi$ cannot be reparameterized using only image variables ranging over finite sets. We record this observation explicitly:

Lemma 4.1 (Cardinality obstruction for finite-set reparameterization).

Let ${\mathcal{M}}$ be a countable chain and let $\varphi(\overline{X})$ be an $\mathit{MSO}$ formula. If

S_{\varphi}({\mathcal{M}})\ :=\ \{\,\overline{A}=(A_{1},\dots,A_{k})\mid A_{i}% \subseteq{\mathcal{M}}\text{ and }{\mathcal{M}}\models\varphi(\overline{A})\,\}

is uncountable, then $\varphi$ admits no reparameterization over $\{{\mathcal{M}}\}$ using only image variables ranging over finite sets.

Proof.

If $G(\overline{X},\overline{F})$ were such a reparameterization with $\overline{F}$ ranging over finite subsets of ${\mathcal{M}}$ , then the set of possible parameter tuples $\overline{F}$ would be countable (finite subsets of a countable set form a countable family, and finite products of countable sets are countable). The bounded-preimage condition would then force $S_{\varphi}({\mathcal{M}})$ to be countable, a contradiction. $\hfill\blacktriangleleft$ Building on results of [1], we show that over Dedekind-complete chains, the cardinality obstruction above is the only obstruction to finite-set reparameterization:

Theorem 4.2 (Reparameterization over Dedekind-complete chains).

Let $\mathsf{DC}$ be the class of Dedekind-complete countable linear orders, and let $\varphi(\overline{X})$ be an $\mathit{MSO}$ formula. The following are equivalent:

1.

$\varphi$ admits a reparameterization over $\mathsf{DC}$ using only image variables ranging over finite sets.
2.

For every ${\mathcal{M}}\in\mathsf{DC}$ , the set $S_{\varphi}({\mathcal{M}})$ is at most countable.

In addition, it is decidable whether (2) holds, and one can effectively construct such a reparameterization from $\varphi$ .

$\blacktriangleright$ Remark.

Arguments analogous to those in Lemma 3.2 show that Theorem 4.2 immediately generalizes to the case where $\mathsf{DC}$ is replaced by any $\mathit{MSO}$ -definable subclass $C\subseteq\mathsf{DC}$ .

We first address decidability. In [1], the authors study an extension of monadic second-order logic over linear orders by a cardinality quantifier of the form “there exist uncountably many sets such that $\dots$ ”. They prove that, over the class of countable linear orders, every formula of this extended logic is effectively equivalent to a pure $\mathit{MSO}$ formula. Consequently, Condition (2) of Theorem 4.2 can be expressed in $\mathit{MSO}$ and is therefore decidable over countable linear orders by Rabin’s theorem [7].

We now turn to the existence and effective construction of finite-set reparameterizations. Assume that $\varphi$ does not have a cardinality obstruction to finite-set reparameterization. We will prove that $\varphi$ admits a reparameterization over $\mathsf{DC}$ using only image variables ranging over finite sets. We begin with the following definition.

Definition 4.3 (Reparameterization by finite unions of intervals).

A reparameterization $G(\overline{X},\overline{Y})$ is a reparameterization of $\varphi$ over $\mathcal{C}$ by finite unions of intervals if each image variable $Y_{i}$ is restricted to range over finite unions of intervals.

The following theorem is a consequence of results in [1]; see Appendix D for a proof.

Theorem 4.4 (Reparameterization by finite unions of intervals).

Let $\mathcal{C}$ be the class of countable chains, and let $\varphi(\overline{X})$ be an $\mathit{MSO}$ formula. If for every ${\mathcal{M}}\in\mathcal{C}$ the set $S_{\varphi}({\mathcal{M}})$ is at most countable, then $\varphi$ effectively admits a reparameterization over $\mathcal{C}$ in which each image variable ranges over finite unions of intervals.

The Dedekind completeness assumption in Theorem 4.2 is needed to represent intervals by pairs of endpoints, which is possible only in Dedekind-complete orders. Theorem 4.2 then follows from Theorem 4.4, together with the observation that, over such orders, finite unions of intervals can be encoded by a bounded tuple of finite sets.

Lemma 4.5 (Uniform coding of finite unions of intervals).

There exists a constant $m\in\mathbb{N}$ and a first-order formula $\psi(x,F_{0},\dots,F_{m})$ such that:

1.

For every Dedekind-complete linear order $L$ and every set $U\subseteq L$ that is a finite union of intervals, there exist finite sets $F_{0},\dots,F_{m}\subseteq L$ such that for all $x\in L$ :

$x\in U\quad\Longleftrightarrow\quad(L,<,F_{0},\dots,F_{m})\models\psi(x,F_{0},% \dots,F_{m}).$
2.

Conversely, for every Dedekind-complete linear order $L$ and every tuple of finite sets $\overline{F}\subseteq L$ , the set defined by $\{x\in L\mid(L,<,\overline{F})\models\psi(x,\overline{F})\}$ is a finite union of intervals.

Hence every reparameterization by finite unions of intervals can be uniformly converted into a finite-set reparameterization, yielding Theorem 4.2.

Functional refinement over ordinals

The reparameterizations obtained in Theorem 4.4 (and hence in Theorem 4.2) are not necessarily functional. Over ordinals, however, they can be made functional by choosing, for each input, a canonical (least) tuple of finite-set parameters.

Lemma 4.6 (Definable well-order on finite subsets of ordinals).

There exists an $\mathit{MSO}(<)$ -formula $W(X,Y)$ such that, for every ordinal $\langle\alpha,<\rangle$ , the relation $W$ is a well-order on the family of finite subsets of $\alpha$ .

$\blacktriangleright$ Remark (Canonical choice yields functionality).

Over ordinals, any reparameterization with finite-set image variables can be made functional by requiring that the image tuple be $W$ -least among all witnesses, where $W$ is an $\mathit{MSO}(<)$ -definable well-order on finite subsets (Lemma 4.6).

5 Conclusion and Further Results

We establish reparameterization as a unifying and effective framework for systematically simplifying MSO interpretations. By leveraging Rabin’s theorem in this new context, we obtain a complete, decidable toolkit for interpretation simplification over infinite countable chains.

Our primary goal in this work is to establish existence results rather than optimality. In particular, Theorem 3.1 characterizes when a finite-set-to-point reparameterization exists, and Theorem 4.2 characterizes when a set-to-finite-set reparameterization exists. However, our constructions are not optimized with respect to the dimension of the resulting reparameterizations.

Bojańczyk [2] introduced polyregular functions, a class of string-to-string functions with polynomial output size, and showed that it is decidable whether an $\mathit{MSO}$ formula with $m$ free first-order variables admits a $d$ -dimensional point reparameterization over finite words. In [8], we extended this result to arbitrary countable labeled chains, showing that it is decidable whether an $\mathit{MSO}$ formula with $m$ free first-order variables admits a $d$ -dimensional point reparameterization in this setting. Together with Theorem 3.1, this yields a characterization of the optimal dimension of finite-set-to-point reparameterizations.

A natural open problem is to decide whether an $\mathit{MSO}$ formula with $m$ free finite-set variables admits a $d$ -dimensional reparameterization over countable chains using only image variables ranging over finite sets. This problem appears to require new techniques beyond those developed in the present work.

Another interesting problem is to decide when a formula admits a functional set-to-finite-set reparameterization over $\mathsf{DC}$ .

References

[1] Vince Barany, Lukasz Kaiser, and Alexander Rabinovich. Expressing cardinality quantifiers in monadic second-order logic over chains. J. Symb. Log., 76(2):603–619, 2011. doi:10.2178/jsl/1305810766.
[2] Mikołaj Bojańczyk. On the growth rates of polyregular functions. In 2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 1–13. IEEE, 2023. doi:10.1109/LICS56636.2023.10175808.
[3] Paul Gallot, Nathan Lhote, and Lê Thành Dũng Nguyên. The structure of polynomial growth for tree automata/transducers and MSO set queries. To appear in TheoretiCS, 2025. Available at https://doi.org/10.48550/arXiv.2501.10270.
[4] Ronald L. Graham, Bruce L. Rothschild, and Joel H. Spencer. Ramsey Theory. Wiley, 1990.
[5] Yuri Gurevich. Monadic second-order theories. Model-theoretic logics, pages 479–506, 1985.
[6] Jaakko Hintikka. Distributive Normal Forms in the Calculus of Predicates. Number 6 in Acta Philosophica Fennica. Societas Philosophica Fennica, Helsinki, 1953.
[7] Michael O Rabin. Decidability of second-order theories and automata on infinite trees. Transactions of the american Mathematical Society, 141:1–35, 1969.
[8] Alexander Rabinovich. Decidability of mso reparametrization over countable labelled chains. In Proceedings of the 33rd Workshop on Logic, Language, Information and Computation (WoLLIC 2026), 2026.
[9] Joseph G. Rosenstein. Linear Orderings. Academic Press, New York, 1982.
[10] Saharon Shelah. The monadic theory of order. Annals of Mathematics, 102(3):379–419, 1975.
[11] Alfred Tarski, Andrzej Mostowski, and Raphael M. Robinson. Undecidable Theories. North-Holland, Amsterdam, 1953.
[12] Wolfgang Thomas. Automata on infinite objects. In Formal Models and Semantics, pages 133–191. Elsevier, 1990. doi:10.1016/B978-0-444-88074-1.50009-3.

Appendix A Interpretations and Reparameterizations

In this section, we recall the standard definition of interpretation and explain how reparameterizations can be used to simplify interpretations. Although not strictly necessary for our main results, this material provides useful background and motivation for the reparameterization problem.

We follow [2] and adapt the definition of interpretation to our setting.

Definition (Interpretation)

An MSO interpretation is a function

f:C\to D

between two classes of structures. All formulas mentioned below are MSO formulas over the vocabulary of the input class $C$ .

1.

Components. There is a finite set $Q$ of components. Each component has a dimension in $\{0,1,\dots\}$ .
2.

Universe formulas. Each component $q\in Q$ has a universe formula. The number of free variables equals the dimension of $q$ .

For an input structure $A\in C$ , the universe of the output is

$\bigsqcup_{q\in Q}\left\{\overline{X}\in(2^{A})^{\mathrm{dim}(q)}\;\middle|\;% \overline{X}\text{ satisfies the universe formula for }q\right\}.$
3.

Relation interpretations. Let $R$ be a relation in the output vocabulary $D$ of arity $\ell$ . For every $q_{1},\dots,q_{\ell}\in Q$ , there is a formula $\varphi$ such that for every $A\in C$ ,

$A\models\varphi(\overline{X}_{1},\dots,\overline{X}_{\ell}),\quad\text{where }% \overline{X}_{i}\in(2^{A})^{\mathrm{dim}(q_{i})},$

if and only if $(\overline{X}_{1},\dots,\overline{X}_{\ell})$ belongs to $R$ in the output structure.

An interpretation is a set (respectively, finite-set, point) interpretation if its free variables range over sets (respectively, finite sets, singleton sets). It is $d$ -dimensional if the maximal dimension of its components is $d$ .

Two interpretations $f,h:C\to D$ are equivalent if, for every $A\in C$ , the structures $f(A)$ and $h(A)$ are isomorphic.

The following proposition is well known (folklore).

Proposition A.1.

Let $C$ be a class of structures equipped with an MSO-definable linear order. Assume that for each component $q$ of a finite-set interpretation over $C$ , the corresponding universe formula $\varphi_{q}$ admits a functional point reparameterization of dimension $d$ . Then the interpretation is equivalent to a $d$ -dimensional point interpretation. In addition, there exists an $\mathit{MSO}$ formula that uniformly defines an isomorphism between the two interpretations.

Sketch.

Let $G_{q}(\overline{X},\overline{Y})$ be a functional reparameterization of $\varphi_{q}$ of dimension $d$ , and let $N$ be a bound on the number of preimages.

New components are pairs $(q,i)$ , where $q\in Q$ and $1\leq i\leq N$ . The universe formula for $(q,i)$ states that $\overline{Y}$ has at least $i$ preimages under $G_{q}$ .

To interpret relations, let $R$ be defined by a formula $\varphi(\overline{X}_{1},\dots,\overline{X}_{\ell})$ corresponding to components $q_{1},\dots,q_{\ell}$ . For components $(q_{1},j_{1}),\dots,(q_{\ell},j_{\ell})$ , define a formula $\psi(\overline{Y_{1}},\dots,\overline{Y_{\ell})}$ such that $\varphi(\overline{X}_{1},\dots,\overline{X}_{\ell})$ holds, where $\overline{X}_{i}$ is the $j_{i}$ -th preimage of $\overline{Y_{i}}$ under $G_{q_{i}}$ , taken in lexicographic order.

Since the linear order is MSO-definable, so is the lexicographic order on finite sets, and hence the $j_{i}$ -th preimage is MSO-definable.

This yields a $d$ -dimensional interpretation. The correspondence between original elements and their representatives is MSO-definable and induces an isomorphism. $\hfill\blacktriangleleft$ Every reparameterization has an equivalent reparameterization of bound $1$ . This reduction is achieved by introducing additional first-order image variables, at the cost of losing functionality.

Proposition A.2 (Reduction to preimage one).

Let $G(\overline{X},\overline{Y})$ be a reparameterization of $\varphi(\overline{X})$ with bound $N$ . Then there exists a reparameterization

H(\overline{X},\overline{Y},z_{1},\dots,z_{m})

of $\varphi(\overline{X})$ whose bound is $1$ , where $z_{1},\dots,z_{m}$ are first-order variables, such that

G(\overline{X},\overline{Y})\;\Leftrightarrow\;\exists z_{1}\dots z_{m}\,H(% \overline{X},\overline{Y},z_{1},\dots,z_{m}).

Furthermore, $H$ is effectively computable from $G$ . However, $H$ need not be functional.

Sketch.

We present the construction in the one-dimensional case; the general case follows by a similar argument.

Assume $\overline{X}=X$ and $\overline{Y}=Y$ . Fix $Y$ , and let $X_{1},\dots,X_{k}$ , where $k\leq N$ , be all distinct $G$ -preimages of $Y$ . For simplicity, assume that $X_{i}\nsubseteq X_{j}$ for all $i\neq j$ . Then, for every $i\neq j$ , there exists an element $z_{i,j}\in X_{i}\setminus X_{j}$ .

In this simplified case, we take $m:=N-1$ new first-order image variables.

Define $H(X,Y,z_{1},\dots,z_{m})$ to hold if:

(i)

$G(X,Y)$ ;
(ii)

$z_{1},\dots,z_{m}\in X$ ;
(iii)

for every $X^{\prime}\neq X$ , if $G(X^{\prime},Y)$ , then

$\{z_{1},\dots,z_{m}\}\nsubseteq X^{\prime}.$

Then $H$ has bound $1$ . Indeed, for fixed $Y,z_{1},\dots,z_{m}$ , there is at most one $X$ satisfying $H$ , since the tuple $z_{1},\dots,z_{m}$ is contained in such an $X$ and, by condition (iii), is not contained in any other $G$ -preimage of $Y$ .

Moreover,

G(X,Y)\quad\Longleftrightarrow\quad\exists z_{1}\dots z_{m}\,H(X,Y,z_{1},\dots% ,z_{m}).

For the nontrivial direction, choose for each other $G$ -preimage $X^{\prime}\neq X$ an element of $X\setminus X^{\prime}$ ; this is possible by the simplifying assumption. Since there are at most $N-1$ such preimages, the variables $z_{1},\dots,z_{m}$ suffice.

Note that $H$ need not be functional. $\hfill\blacktriangleleft$ In an interpretation as defined above, each element of the output structure is represented by a unique tuple from the input structure. In contrast, in an interpretation with equivalence, an element may admit several representations.

An interpretation with equivalence is equipped with a definable equivalence relation that is a congruence with respect to all interpreted relations. The elements of the output structure are equivalence classes of tuples satisfying the universe formulas.

Proposition A.3.

Assume that for each component $q$ , the corresponding universe formula $\varphi_{q}$ admits a reparameterization of dimension $d$ with bound $1$ . Then the interpretation is equivalent to a $d$ -dimensional interpretation with equivalence. Moreover, there exists an $\mathit{MSO}$ formula that uniformly defines an isomorphism between the two interpretations.

Sketch.

Replace each component by its $d$ -dimensional reparameterization. For each component $q$ , define the new universe formula

\psi_{q}(\overline{Y}):=\exists\overline{X}\,\bigl(\varphi_{q}(\overline{X})% \wedge G(\overline{X},\overline{Y})\bigr).

Define the new equivalence relation by

\mathrm{Eq}_{\mathrm{new}}(\overline{Y},\overline{Y}^{\prime}):=\exists% \overline{X}\exists\overline{X}^{\prime}\bigl(\mathrm{Eq}(\overline{X},% \overline{X}^{\prime})\wedge G(\overline{X},\overline{Y})\wedge G(\overline{X}% ^{\prime},\overline{Y}^{\prime})\bigr).

To interpret relations, let $R$ be defined by a formula $\varphi(\overline{X}_{1},\dots,\overline{X}_{\ell})$ corresponding to components $q_{1},\dots,q_{\ell}$ . For components $q_{1},\dots,q_{\ell}$ , define a formula $\psi(\overline{Y}_{1},\dots,\overline{Y}_{\ell})$ such that $\varphi(\overline{X}_{1},\dots,\overline{X}_{\ell})$ holds, where $\overline{X}_{i}$ is the preimage of $\overline{Y_{i}}$ under $G_{q_{i}}$ .

Since $G$ has bound $1$ , this is well defined. It is straightforward to check that $\mathrm{Eq}_{\mathrm{new}}$ is an equivalence relation and a congruence with respect to the interpreted relations. The resulting interpretation with equivalence is equivalent to the original one. $\hfill\blacktriangleleft$

Appendix B Proof of Claim 3.5

Claim 3.5. [Restated, see original statement.]

For every $r>q$ and every idempotent $q$ -type $\tau(\overline{X})$ , there exists an idempotent $r$ -type $\tau^{\prime}(\overline{X})$ such that $\tau^{\prime}\rightarrow\tau$ . Moreover, if $\exists^{\geq 2}\,\overline{X}\,\tau(\overline{X})$ is satisfiable, then $\exists^{\geq 2}\,\overline{X}\,\tau^{\prime}(\overline{X})$ is also satisfiable.

Proof.

Let $\pi$ be the natural projection from $r$ -types to $q$ -types. This projection is a semigroup morphism with respect to concatenation.

Since $\tau$ is satisfiable, choose an $r$ -type $\rho$ such that $\pi(\rho)=\tau$ . Since the semigroup of $r$ -types is finite, some power $\rho^{m}$ is idempotent. Put

\tau^{\prime}:=\rho^{m}.

Then $\tau^{\prime}$ is an idempotent $r$ -type, and

\pi(\tau^{\prime})=\pi(\rho^{m})=\pi(\rho)^{m}=\tau^{m}=\tau,

because $\tau$ is idempotent. Hence $\tau^{\prime}\rightarrow\tau$ .

Assume now that

\exists^{\geq 2}\,\overline{X}\,\tau(\overline{X})

is satisfiable. Then there is a structure ${\mathcal{M}}$ with two distinct assignments $\overline{A}^{0}\neq\overline{A}^{1}$ realizing $\tau$ . For each $K$ , consider the concatenation of $K$ copies of ${\mathcal{M}}$ , and for every $S\subseteq\{1,\dots,K\}$ define an assignment $\overline{A}^{S}$ by using $\overline{A}^{1}$ on the copies in $S$ and $\overline{A}^{0}$ on the remaining copies. Since $\tau$ is idempotent, every $\overline{A}^{S}$ realizes the same $q$ -type $\tau$ .

There are only finitely many $r$ -types. Hence, for $K$ large enough, two distinct sets $S\neq T$ yield assignments $\overline{A}^{S}$ and $\overline{A}^{T}$ with the same $r$ -type, say $\rho$ . Since both refine $\tau$ , we have $\pi(\rho)=\tau$ . Choose $m$ such that $\rho^{m}$ is idempotent and put $\tau^{\prime}:=\rho^{m}$ . Then $\tau^{\prime}$ is an idempotent $r$ -type with $\tau^{\prime}\rightarrow\tau$ .

In addition, $\tau^{\prime}$ is realized at least twice: take the concatenation of $m$ copies of a structure realizing $\rho$ twice, and use the first realization in all copies for one assignment, and the second realization in one copy and the first realization elsewhere for another. These two assignments are distinct and both have $r$ -type $\rho^{m}=\tau^{\prime}$ . Thus $\exists^{\geq 2}\,\overline{X}\,\tau^{\prime}(\overline{X})$ is satisfiable. $\hfill\vartriangleleft$

Appendix C Proof of Lemma 3.10

Lemma 3.10 (Uniform bound on restricted factorizations). [Restated, see original statement.]

For every finite semigroup $(S,+)$ , there exists $N_{S}\in\mathbb{N}$ such that every word over $S$ admits a restricted factorization $e_{0}\dots e_{m}$ with $m\leq N_{S}$ .

Proof.

Let $S$ be a finite semigroup. By Ramsey’s theorem for pairs, there exists $N_{S}\in\mathbb{N}$ such that for every coloring $c$ of pairs $\{i,j\}$ with $0\leq i<j\leq N_{S}$ by elements of $S$ , there exist

0\leq i<j<k\leq N_{S}

such that

c(i,j)=c(j,k)=c(i,k).

We show that this $N_{S}$ satisfies the claim.

Suppose, for contradiction, that there exists a word $u=u_{0}\dots u_{\ell-1}\in S^{+}$ with $u_{i}\in S$ that admits no restricted factorization of length at most $N_{S}$ . Among all such words, fix one together with a restricted factorization

e_{0}\dots e_{n-1}

of minimal length $n$ , and let $w_{0},\dots,w_{n-1}$ be the corresponding factors. Then $n>N_{S}$ .

Define a coloring of pairs $0\leq i<j\leq n$ by

c(i,j):=e_{i}+\cdots+e_{j-1}.

Since $n\geq N_{S}+1$ , there exist indices $i<j<k$ such that

c(i,j)=c(j,k)=c(i,k).

Let $e:=c(i,j)$ . Then $e+e=e$ , so $e$ is idempotent.

We merge the factors $w_{i},\dots,w_{k-1}$ into a single factor. Define a new word $e^{\prime}_{0}\dots e^{\prime}_{\,n-(k-i)-1}$ by

e^{\prime}_{p}:=\begin{cases}e_{p}&\text{if }p<i,\\ e_{i}+\dots+e_{k-1}&\text{if }p=i,\\ e_{p+(k-i-1)}&\text{if }p>i.\end{cases}

Then $e^{\prime}_{0}\dots e^{\prime}_{\,n-(k-i)-1}$ has length $n-(k-i)+1<n$ .

Moreover, it is a restricted factorization of $u$ , since the merged factor $w_{i}\cdots w_{k-1}$ has value

e_{i}+\dots+e_{k-1}=c(i,k)=e,

which is idempotent.

This contradicts the minimality of $n$ . Hence every word admits a restricted factorization of length at most $N_{S}$ . $\hfill\blacktriangleleft$

Appendix D Proof of Theorem 4.4

Using the results of [1], we now prove the following strengthening of Theorem 4.4.

Theorem D.1 (Reparameterization by finite unions of intervals).

Let $\mathcal{C}$ be the class of countable chains, and let $\varphi(\overline{X})$ be an $\mathit{MSO}$ formula. Then one can effectively compute an $\mathit{MSO}$ formula $G(\overline{X},\overline{Y})$ such that for every ${\mathcal{M}}\in\mathcal{C}$ , if $S_{\varphi}({\mathcal{M}})$ is at most countable, then $G(\overline{X},\overline{Y})$ defines a reparameterization of $\varphi$ over ${\mathcal{M}}$ , where each image variable in $\overline{Y}$ ranges over finite unions of intervals.

Proof.

A finite family of non-empty intervals $\mathcal{I}=\{I_{1},\dots,I_{n}\}$ is a cover of a chain ${\mathcal{M}}$ if it forms a partition of the domain of ${\mathcal{M}}$ , that is,

\bigcup_{i=1}^{n}I_{i}={\mathcal{M}}\qquad\text{and}\qquad I_{i}\cap I_{j}=% \varnothing\text{ for all }i\neq j.

We first observe that every finite interval cover can be encoded by a single monadic predicate interpreted as a finite union of intervals. Assume that $I_{1}<I_{2}<\cdots<I_{n}$ is such a cover, and let

P\ :=\ \bigcup_{\begin{subarray}{c}1\leq j\leq n\\ j\ \text{odd}\end{subarray}}I_{j}

be the union of the odd-indexed intervals. Let $\Gamma(P,X)$ express that $X$ is a maximal interval of ${\mathcal{M}}$ such that either $X\subseteq P$ or $X\subseteq{\mathcal{M}}\setminus P$ . Then

L\models\Gamma(P,X)\quad\text{iff}\quad X\in\{I_{1},\dots,I_{n}\}.

Thus, every finite interval cover of ${\mathcal{M}}$ can be encoded bijectively by a single monadic predicate $P$ , interpreted as a finite union of intervals.

Now fix a chain ${\mathcal{M}}$ and an $\mathit{MSO}$ formula $\varphi(\overline{X})$ . The following notions and facts are defined and proved in [1]:

$\blacksquare$

The notion of a balanced $U$ – $U$ cover for $\overline{A}$ with respect to ${\mathcal{M}}$ and $\varphi$ is defined in [1, Definition 14]. Every balanced $U$ – $U$ cover is a finite interval cover.
$\blacksquare$

There exists an $\mathit{MSO}$ formula expressing that a given cover is a balanced $U$ – $U$ cover for $\overline{A}$ with respect to ${\mathcal{M}}$ and $\varphi$ (see [1, Definition 14]).
$\blacksquare$

If $S_{\varphi}({\mathcal{M}})$ is at most countable, then every tuple $\overline{A}$ with ${\mathcal{M}}\models\varphi(\overline{A})$ admits a balanced $U$ – $U$ cover (see [1, Lemma 10 and Lemma 13]).

Furthermore, if $\mathcal{I}=\{I_{1},\dots,I_{n}\}$ is a balanced $U$ – $U$ cover of a tuple $\overline{A}$ , then each interval $I_{j}$ belongs to one of finitely many kinds (e.g. $U$ -intervals, left-balanced unsplittable $D$ intervals, and right-balanced unsplittable $D$ intervals); see [1, Definition 14 and Lemma 15]. Furthermore, by [1, Lemma 16 and its proof] there exists a constant $N\in\mathbb{N}$ , computable from $\varphi$ , such that, for any fixed balanced $U$ – $U$ cover $\mathcal{I}$ and any fixed interval kind, the restriction $\overline{A}\cap I_{j}$ can take at most $N$ distinct values among all tuples $\overline{A}$ admitting the cover $\mathcal{I}$ .

Consequently, every tuple $\overline{A}$ with ${\mathcal{M}}\models\varphi(\overline{A})$ can be encoded by the following data:

1.

a balanced $U$ – $U$ cover $\mathcal{I}=\{I_{1},\dots,I_{n}\}$ of ${\mathcal{M}}$ associated with $\overline{A}$ ,
2.
for each interval $I_{j}\in\mathcal{I}$ :
- $\blacksquare$
  
  the kind of $I_{j}$ , and
- $\blacksquare$
  
  an index in $\{1,\dots,N\}$ identifying the restriction $\overline{A}\cap I_{j}$ among all possibilities consistent with that kind.

By the first part of the proof, the cover $\mathcal{I}$ can be encoded by a monadic predicate interpreted as a finite union of intervals. The interval kinds and the corresponding indices can be encoded using finitely many additional monadic predicates, each definable as a finite union of intervals; moreover, for this information, finite predicates already suffice. Hence, the above information can be represented by a bounded tuple of monadic predicates, each ranging over finite unions of intervals.

Therefore, one obtains a reparameterization of $\varphi$ in which all image variables range over finite unions of intervals.

Finally, the construction is effective: the $\mathit{MSO}$ definitions of balanced $U$ – $U$ covers, the finite list of interval kinds, and the bound $N$ are computable from $\varphi$ . This yields the required formula $G(\overline{X},\overline{Y})$ and completes the proof. $\hfill\blacktriangleleft$

Appendix E Proof of Lemma 4.5

Lemma 4.5 (Uniform coding of finite unions of intervals). [Restated, see original statement.]

There exists a constant $m\in\mathbb{N}$ and a first-order formula $\psi(x,F_{0},\dots,F_{m})$ such that:

1.

For every Dedekind-complete linear order $L$ and every set $U\subseteq L$ that is a finite union of intervals, there exist finite sets $F_{0},\dots,F_{m}\subseteq L$ such that for all $x\in L$ :

$x\in U\quad\Longleftrightarrow\quad(L,<,F_{0},\dots,F_{m})\models\psi(x,F_{0},% \dots,F_{m}).$
2.

Conversely, for every Dedekind-complete linear order $L$ and every tuple of finite sets $\overline{F}\subseteq L$ , the set defined by $\{x\in L\mid(L,<,\overline{F})\models\psi(x,\overline{F})\}$ is a finite union of intervals.

Proof.

Let $L$ be a Dedekind-complete linear order. Any set $U\subseteq L$ that is a finite union of intervals can be uniquely decomposed into a union of $k$ disjoint, non-adjacent intervals $I_{1}<I_{2}<\dots<I_{k}$ .

Construction of the finite sets

We define six finite sets $F_{0},\dots,F_{5}$ (i.e., $m=5$ ) to encode the boundary behavior of $U$ :

$\blacksquare$

$L_{cl}$ and $L_{op}$ : the sets of finite left endpoints of the intervals $I_{j}$ that are closed and open, respectively.
$\blacksquare$

$R_{cl}$ and $R_{op}$ : the sets of finite right endpoints of the intervals $I_{j}$ that are closed and open, respectively.
$\blacksquare$

$B$ and $T$ : flag sets. We set $B\neq\emptyset$ if and only if $U$ is unbounded below, and $T\neq\emptyset$ if and only if $U$ is unbounded above. (For example, $B$ can be a singleton containing any arbitrary element of $L$ if the condition holds, and empty otherwise.)

Since $U$ is a finite union of intervals, the set of all finite endpoints $E=L_{cl}\cup L_{op}\cup R_{cl}\cup R_{op}$ is finite.

The first-order formula

The formula $\psi(x,\overline{F})$ determines membership in $U$ by identifying the relative position of $x$ with respect to the finite set $E$ . Using first-order logic over the signature $\{<\}$ , we can define the greatest endpoint at or below $x$ :

\text{max\_below}(x,y):=(y\leq x\land y\in E)\land\forall z((y<z\leq x)% \implies z\notin E)

In a Dedekind-complete order, if the set $\{y\in E\mid y\leq x\}$ is non-empty, then the maximum $y$ exists because $E$ is finite. The formula $\psi(x,\overline{F})$ is defined by a case analysis:

1.

If $x$ has no endpoints at or below it ( $\neg\exists y(y\leq x\land y\in E)$ ), then $x\in U$ if and only if $B\neq\emptyset$ .
2.
If there exists $a$ such that $\text{max\_below}(x,a)$ , then $x\in U$ if and only if:
- $\blacksquare$
  
  $a\in L_{cl}$ , or
- $\blacksquare$
  
  $a\in L_{op}$ and $a<x$ , or
- $\blacksquare$
  
  $a\in R_{cl}$ and $a=x$ .

This logic ensures that if $x$ falls within an interval $(a,b)$ , $[a,b)$ , $(a,b]$ , or $[a,b]$ , its membership is correctly determined by the kind of the last boundary point $a$ . If $x$ is beyond all endpoints, its membership is determined by whether the final interval is unbounded above, which is consistent with the behavior of the last endpoint in $E$ and the flag $T$ .

Property of the constructed formula

The second part of the lemma follows from the structure of $\psi$ . For any choice of finite sets $\overline{F}$ , the points in $E=\bigcup F_{i}$ partition $L$ into finitely many points and open segments $(e_{i},e_{i+1})$ . Because $\psi(x,\overline{F})$ evaluates $x$ solely based on its identity as an endpoint or its relative order to the nearest element in $E$ , the truth value of $\psi$ remains constant on each such segment. Consequently, for any finite $\overline{F}$ , the set $\{x\in L\mid(L,<,\overline{F})\models\psi(x,\overline{F})\}$ is necessarily a finite union of intervals. $\hfill\blacktriangleleft$

[bib.bib1] [1] Vince Barany, Lukasz Kaiser, and Alexander Rabinovich. Expressing cardinality quantifiers in monadic second-order logic over chains. J. Symb. Log., 76(2):603–619, 2011. doi:10.2178/jsl/1305810766.

[bib.bib2] [2] Mikołaj Bojańczyk. On the growth rates of polyregular functions. In 2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 1–13. IEEE, 2023. doi:10.1109/LICS56636.2023.10175808.

[bib.bib3] [3] Paul Gallot, Nathan Lhote, and Lê Thành Dũng Nguyên. The structure of polynomial growth for tree automata/transducers and MSO set queries. To appear in TheoretiCS, 2025. Available at https://doi.org/10.48550/arXiv.2501.10270.

[bib.bib4] [4] Ronald L. Graham, Bruce L. Rothschild, and Joel H. Spencer. Ramsey Theory. Wiley, 1990.

[bib.bib5] [5] Yuri Gurevich. Monadic second-order theories. Model-theoretic logics, pages 479–506, 1985.

[bib.bib6] [6] Jaakko Hintikka. Distributive Normal Forms in the Calculus of Predicates. Number 6 in Acta Philosophica Fennica. Societas Philosophica Fennica, Helsinki, 1953.

[bib.bib7] [7] Michael O Rabin. Decidability of second-order theories and automata on infinite trees. Transactions of the american Mathematical Society, 141:1–35, 1969.

[bib.bib8] [8] Alexander Rabinovich. Decidability of mso reparametrization over countable labelled chains. In Proceedings of the 33rd Workshop on Logic, Language, Information and Computation (WoLLIC 2026), 2026.

[bib.bib9] [9] Joseph G. Rosenstein. Linear Orderings. Academic Press, New York, 1982.

[bib.bib10] [10] Saharon Shelah. The monadic theory of order. Annals of Mathematics, 102(3):379–419, 1975.

[bib.bib11] [11] Alfred Tarski, Andrzej Mostowski, and Raphael M. Robinson. Undecidable Theories. North-Holland, Amsterdam, 1953.

[bib.bib12] [12] Wolfgang Thomas. Automata on infinite objects. In Formal Models and Semantics, pages 133–191. Elsevier, 1990. doi:10.1016/B978-0-444-88074-1.50009-3.

From Sets to Points: Simplifying MSO Interpretations via Reparameterizations

Abstract

Keywords and phrases:

Category:

Funding:

Copyright and License:

2012 ACM Subject Classification:

Acknowledgements:

DOI:

Event:

Editors:

Series and Publisher:

1 Introduction

Interpretations of 𝔄 in 𝔅

Definition 1.1 (Reparameterization).

Intuition.

Our contributions and paper organization

2 Preliminaries

2.1 Chains

2.2 Monadic Second-Order Logic

Theorem 2.1 (Rabin, 1969 [7]).

2.3 Types

Lemma 2.2 (Hintikka, [6]).

2.4 Concatenation of Chains and Sum of Types

Proposition 2.3 (Sum of types [10]).

Lemma 2.4 (r-local normal form).

3 Finite-Set-to-Point Reparameterizations

Theorem 3.1 (Finite-set-to-point reparameterization over countable chains).

Lemma 3.2 (Reducing to the full class of countable chains).

3.1 Idempotent obstruction to point reparameterization

Definition 3.3 (Idempotent obstruction to point reparameterization).

Lemma 3.4 (Obstruction lemma).

Proof.

Claim 3.5.

Step 1: Fix realizations of the types.

Step 2: Build many witnesses using idempotence.

Step 3: Pigeonhole argument.

3.2 From the absence of an idempotent obstruction to point reparameterization

Theorem 3.6 (Main).

▶ Remark (Countability Assumption).

Proof overview

Step 1: Encoding by 𝒒-type words.

Step 2: Uniformly bounded factorization.

Step 3: Local reparameterizations.

Step 4: Global construction.

Definition 3.7 (q-type word associated with a labeled chain).

Lemma 3.8.

Definition 3.9 (Restricted Factorization).

Lemma 3.10 (Uniform bound on restricted factorizations).

Lemma 3.11 (Properties of restricted factorization words).

Notation.

Definition 3.12 (Models of a restricted factorization word).

Lemma 3.13 (Short factorization word property).

Definition 3.14 (Reparameterization induced by a factorization word).

Inductive definition of 𝑯𝒔.

Lemma 3.15 (Properties of Hs).

Lemma 3.16.

Proof of Theorem 3.6.

4 Reparameterization of arbitrary sets by finite sets

Cardinality obstruction

Lemma 4.1 (Cardinality obstruction for finite-set reparameterization).

Proof.

Theorem 4.2 (Reparameterization over Dedekind-complete chains).

▶ Remark.

Definition 4.3 (Reparameterization by finite unions of intervals).

Theorem 4.4 (Reparameterization by finite unions of intervals).

Lemma 4.5 (Uniform coding of finite unions of intervals).

Functional refinement over ordinals

Lemma 4.6 (Definable well-order on finite subsets of ordinals).

▶ Remark (Canonical choice yields functionality).

5 Conclusion and Further Results

References

Appendix A Interpretations and Reparameterizations

Definition (Interpretation)

Proposition A.1.

Sketch.

Proposition A.2 (Reduction to preimage one).

Sketch.

Proposition A.3.

Sketch.

Interpretations of $\mathfrak{A}$ in $\mathfrak{B}$

Lemma 2.4 ( $r$ -local normal form).

$\blacktriangleright$ Remark (Countability Assumption).

Step 1: Encoding by $𝒒$ -type words.

Definition 3.7 ( $q$ -type word associated with a labeled chain).

Inductive definition of $H_{s}$ .

Lemma 3.15 (Properties of $H_{s}$ ).

$\blacktriangleright$ Remark.

$\blacktriangleright$ Remark (Canonical choice yields functionality).