A Dichotomy Theorem for Ordinal Ranks in MSO

Resumen Técnico: Un Teorema de la Dicotomía para los Rangos Ordinales en MSO

1. Formulación del Problema

El artículo investiga el poder expresivo de la lógica de Segundo Orden Monádica (MSO) sobre el árbol binario infinito completo, específicamente en relación con la complejidad de los conjuntos bien fundados que sirven como testigos de la cuantificación existencial.

Considere una fórmula de la forma $\exists X. \varphi(\vec{Y}, X)$, donde $\varphi$ es una fórmula MSO arbitraria. Los autores asumen que, siempre que la fórmula se satisface para una valoración de $\vec{Y}$, el conjunto testigo $X$ es bien fundado (es decir, no contiene cadenas descendentes infinitas con respecto al orden de descendencia del árbol). Para tal conjunto $X$, un rango ordinal contable, denotado como $\text{rank}(X)$, está bien definido, midiendo la profundidad y la estructura de ramificación del conjunto.

El problema central es determinar el ordinal de clausura (o límite superior mínimo) de estos rangos para una fórmula dada. Sea $\text{rank}(\varphi)$ definido como:
$$\text{rank}(\varphi) \stackrel{\text{def}}{=} \sup_{\vec{Y}} \min_{X} \text{rank}(X)$$
donde el supremo se toma sobre todas las valoraciones $\vec{Y}$ que satisfacen la fórmula, y el mínimo se toma sobre todos los conjuntos testigos $X$. Dado que el supremo de los ordinales contables es a lo sumo $\omega_1$ (el primer ordinal no contable), la pregunta es: ¿Cuál es el valor exacto de $\text{rank}(\varphi)$?

Trabajos previos establecieron que, para cualquier par de números naturales $(k, l)$, se puede construir una fórmula con $\text{rank}(\varphi) = \omega \cdot k + l$. Sin embargo, se desconocía si otros ordinales (específicamente aquellos $\ge \omega^2$ pero $< \omega_1$) podían ser realizados como ordinales de clausura para fórmulas MSO.

2. Metodología

Los autores emplean un enfoque teórico de juegos combinado con la teoría de autómatas para caracterizar estos rangos.

• Representación por Autómatas: En lugar de trabajar directamente con fórmulas MSO, los autores utilizan la equivalencia entre MSO y autómatas de árboles de paridad no deterministas (Teorema de Rabin). Definen una relación regular $\Gamma \subseteq \text{Tr}_A \times \text{WF}$ (donde $\text{WF}$ es el conjunto de árboles bien fundados) reconocida por un autómata podado.
• Rangos Refinados: Para facilitar la demostración, los autores introducen dos rangos auxiliares, $\text{rank}_R$ (profundidad por capas) y $\text{rank}_T$ (profundidad del tronco), que están estrechamente relacionados con el rango estándar $\text{rank}(x)$. Crucialmente, establecen que $\text{rank}_R(\Gamma) \le \text{rank}(\Gamma) \le \omega \cdot \text{rank}_R(\Gamma)$. Esto les permite centrarse en computar $\text{rank}_R$, que se comporta de manera más robusta en el contexto de la definibilidad MSO.
• El Juego de la Dicotomía ($G^N_A$): El núcleo de la metodología es la construcción de un juego de dos jugadores, $G^N_A$, jugado sobre el espacio de estados del autómata. El juego está parametrizado por un número natural $N$ (o $\infty$).
  • Jugadores: $\exists$ (Eloise) intenta construir un árbol que requiera testigos de alto rango, mientras que $\forall$ (Abelard) intenta demostrar que bastan testigos de menor rango.
  • Mecánica: El juego implica la selección de transiciones, direcciones y "selectores" que rastrean el potencial anidamiento de "peines" (estructuras que representan un alto rango). El juego rastrea dos lados, R (alcance) y T (tronco), para modelar el proceso de derivada utilizado para definir los rangos ordinales.
  • Condiciones de Victoria: Las condiciones de victoria son $\omega$-regulares. $\exists$ gana si puede forzar un camino que cambie de lado de R a T al menos $N$ veces (para $N$ finito), o infinitas veces (para $N=\infty$), o si el juego contiene caminos de rechazo con ramificación insuficiente. $\forall$ gana si puede prevenir estas condiciones.
• Análisis de Estrategias: Los autores demuestran que el juego está determinado (por el teorema de Büchi-Landweber) y que la existencia de una estrategia ganadora para $\exists$ en $G^\infty_A$ corresponde exactamente a $\text{rank}_R(\Gamma) = \omega_1$, mientras que una estrategia ganadora para $\forall$ implica $\text{rank}_R(\Gamma) < \omega$.

3. Contribuciones Clave y Resultados

El Teorema Principal de la Dicotomía (Teorema 1.1):
Para cualquier fórmula $\exists X. \varphi(\vec{Y}, X)$ donde $X$ es bien fundado, el ordinal $\text{rank}(\varphi)$ satisface una dicotomía estricta:

1. Estrictamente Pequeño: $\text{rank}(\varphi) < \omega^2$. En este caso, existe un número natural computable $N$ tal que $\text{rank}(\varphi) < \omega \cdot N$.
2. Máximo: $\text{rank}(\varphi) = \omega_1$.

Además, es decidible qué uno de estos dos casos se cumple para una fórmula dada.

Resultados de Definibilidad (Sección 9):
El artículo investiga si la propiedad "$\text{rank}(X) \le \eta$" es expresable en MSO.

• Para $\eta < \omega$, el lenguaje de árboles con rango $\le \eta$ es regular (definible en MSO).
• Para $\eta \ge \omega$, el lenguaje no es regular. Consecuentemente, el predicado $\text{rank}(X) \le \eta$ no puede expresarse directamente en MSO para $\eta \ge \omega$.
• Sin embargo, el teorema de la dicotomía implica que, aunque MSO no puede definir rangos grandes específicos, puede decidir implícitamente si el rango está acotado por $\omega^2$ o es no acotado (alcanzando $\omega_1$).

Aplicación al $\mu$-Cálculo (Sección 10):
Los autores aplican sus resultados a los ordinales de clausura de las fórmulas de punto fijo en el $\mu$-cálculo.

• Abordan una pregunta planteada por Czarnecki sobre si una fórmula del $\mu$-cálculo puede tener un ordinal de clausura contable $\ge \omega^2$.
• Utilizando una reducción de $\mu$-cálculo a MSO en el árbol binario, demuestran que para los puntos fijos vectoriales (donde las variables no aparecen en el alcance de otros operadores de punto fijo), el ordinal de clausura es o bien $< \omega^2$ o bien $\ge \omega_1$.
• Esto proporciona una prueba alternativa y un procedimiento de decisión para un resultado establecido recientemente por Afshari, Barlucchi y Leigh, con la ventaja añadida de la decidibilidad y la aplicabilidad a modelos arbitrarios (no solo contables).

4. Significado y Reivindicaciones

El artículo afirma que su principal contribución es establecer una dicotomía decidible para los rangos ordinales de los testigos bien fundados en MSO.

• Impacto Teórico: Resuelve la cuestión de qué ordinales pueden aparecer como ordinales de clausura en MSO, mostrando que el espectro tiene un "hueco": no se pueden alcanzar los ordinales entre $\omega^2$ y $\omega_1$. El conjunto de rangos alcanzables es $\{ \alpha \mid \alpha < \omega^2 \} \cup \{ \omega_1 \}$.
• Decidibilidad: A diferencia de muchos problemas en extensiones de MSO, los autores muestran que determinar si el rango es $< \omega^2$ es decidible.
• Robustez de $\text{rank}_R$: El artículo destaca que el rango de "profundidad por capas" ($\text{rank}_R$) es una medida más robusta para la definibilidad MSO que el rango estándar, ya que permite la computación exacta de valores hasta $\omega$, mientras que el rango estándar se vuelve indefinible mucho antes.
• Limitaciones: Los autores señalan modestamente que, aunque pueden decidir si el rango es $< \omega^2$ o $= \omega_1$, computar el valor exacto del rango (si este es $< \omega^2$) sigue siendo un problema abierto para el rango estándar, aunque es computable para $\text{rank}_R$. También aclaran que su resultado para el $\mu$-cálculo se aplica a un fragmento específico (variables que no están en el alcance de operadores de punto fijo) y no se transfiere inmediatamente al ámbito general de MSO debido a las restricciones de monotonicidad inherentes a las iteraciones de punto fijo.

En resumen, el artículo demuestra que, si bien MSO no puede definir explícitamente rangos ordinales arbitrariamente grandes, posee el poder suficiente para distinguir implícitamente entre rangos "pequeños" (acotados por $\omega^2$) y rangos "máximos" ($\omega_1$), una distinción que es efectivamente decidible.