A Dichotomy Theorem for Ordinal Ranks in MSO

Fuente: arXiv
Saved in:
Bibliographic Details
Main Authors: Niwiński, Damian, Parys, Paweł, Skrzypczak, Michał
Format: Preprint
Published: 2025
Subjects:
Online Access:
Tags: Add Tag
No Tags, Be the first to tag this record!
_version_ 1866908707732848640
author Niwiński, Damian
Parys, Paweł
Skrzypczak, Michał
author_facet Niwiński, Damian
Parys, Paweł
Skrzypczak, Michał
contents We focus on formulae $\exists X.\, φ(\vec{Y}, X)$ of monadic second-order logic over the full binary tree, such that the witness $X$ is a well-founded set. The ordinal rank $\mathrm{rank}(X) < ω_1$ of such a set $X$ measures its depth and branching structure. We search for the least upper bound for these ranks, and discover the following dichotomy depending on the formula $φ$. Let $\mathrm{rank}(φ)$ be the minimal ordinal such that, whenever an instance $\vec{Y}$ satisfies the formula, there is a witness $X$ with $\mathrm{rank}(X) \leq \mathrm{rank}(φ)$. Then $\mathrm{rank}(φ)$ is either strictly smaller than $ω^2$ or it reaches the maximal possible value $ω_1$. Moreover, it is decidable which of the cases holds. The result has potential for applications in a variety of ordinal-related problems, in particular it entails a result about the closure ordinal of a fixed-point formula.
format Preprint
id arxiv_https___arxiv_org_abs_2501_05385
institution arXiv
publishDate 2025
record_format arxiv
spellingShingle A Dichotomy Theorem for Ordinal Ranks in MSO
Niwiński, Damian
Parys, Paweł
Skrzypczak, Michał
Logic in Computer Science
We focus on formulae $\exists X.\, φ(\vec{Y}, X)$ of monadic second-order logic over the full binary tree, such that the witness $X$ is a well-founded set. The ordinal rank $\mathrm{rank}(X) < ω_1$ of such a set $X$ measures its depth and branching structure. We search for the least upper bound for these ranks, and discover the following dichotomy depending on the formula $φ$. Let $\mathrm{rank}(φ)$ be the minimal ordinal such that, whenever an instance $\vec{Y}$ satisfies the formula, there is a witness $X$ with $\mathrm{rank}(X) \leq \mathrm{rank}(φ)$. Then $\mathrm{rank}(φ)$ is either strictly smaller than $ω^2$ or it reaches the maximal possible value $ω_1$. Moreover, it is decidable which of the cases holds. The result has potential for applications in a variety of ordinal-related problems, in particular it entails a result about the closure ordinal of a fixed-point formula.
title A Dichotomy Theorem for Ordinal Ranks in MSO
topic Logic in Computer Science
url https://arxiv.org/abs/2501.05385