A Dichotomy Theorem for Ordinal Ranks in MSO

Resumo Técnico: Um Teorema de Dicotomia para Postos Ordinais em MSO

1. Formulação do Problema

O artigo investiga o poder expressivo da lógica de Segunda Ordem Monádica (MSO) sobre a árvore binária infinita completa, especificamente no que diz respeito à complexidade de conjuntos bem fundados que servem como testemunhas para a quantificação existencial.

Considere uma fórmula da forma $\exists X. \varphi(\vec{Y}, X)$, onde $\varphi$ é uma fórmula MSO arbitrária. Os autores assumem que, sempre que a fórmula é satisfeita para uma valoração de $\vec{Y}$, o conjunto testemunha $X$ é bem fundado (ou seja, não contém cadeias descendentes infinitas com relação à ordem de descendência da árvore). Para tal conjunto $X$, um posto ordinal enumerável, denotado por $\text{rank}(X)$, é bem definido, medindo a profundidade e a estrutura de ramificação do conjunto.

O problema central é determinar o ordinal de fechamento (ou limite superior mínimo) destes postos para uma dada fórmula. Seja $\text{rank}(\varphi)$ definido como:
$$\text{rank}(\varphi) \stackrel{\text{def}}{=} \sup_{\vec{Y}} \min_{X} \text{rank}(X)$$
onde o supremo é tomado sobre todas as valorações $\vec{Y}$ que satisfazem a fórmula, e o mínimo é tomado sobre todos os conjuntos testemunha $X$. Uma vez que o supremo de ordinais enumeráveis é, no máximo, $\omega_1$ (o primeiro ordinal não enumerável), a questão é: Qual é o valor exato de $\text{rank}(\varphi)$?

Trabalhos anteriores estabeleceram que, para qualquer par de números naturais $(k, l)$, é possível construir uma fórmula com $\text{rank}(\varphi) = \omega \cdot k + l$. No entanto, não se sabia se outros ordinais (especificamente aqueles $\ge \omega^2$ mas $< \omega_1$) poderiam ser realizados como ordinais de fechamento para fórmulas MSO.

2. Metodologia

Os autores empregam uma abordagem teórica de jogos combinada com a teoria de autômatos para caracterizar estes postos.

• Representação por Autômatos: Em vez de trabalhar diretamente com fórmulas MSO, os autores utilizam a equivalência entre MSO e autômatos de árvore de paridade não determinísticos (Teorema de Rabin). Eles definem uma relação regular $\Gamma \subseteq \text{Tr}_A \times \text{WF}$ (onde $\text{WF}$ é o conjunto de árvores bem fundadas) reconhecida por um autômato podado.
• Postos Refinados: Para facilitar a prova, os autores introduzem dois postos auxiliares, $\text{rank}_R$ (profundidade em camadas) e $\text{rank}_T$ (profundidade do tronco), que estão intimamente relacionados ao posto padrão $\text{rank}(x)$. Crucialmente, eles estabelecem que $\text{rank}_R(\Gamma) \le \text{rank}(\Gamma) \le \omega \cdot \text{rank}_R(\Gamma)$. Isso permite que foquem no cálculo de $\text{rank}_R$, que se comporta de forma mais robusta no contexto da definibilidade MSO.
• O Jogo de Dicotomia ($G^N_A$): O núcleo da metodologia é a construção de um jogo de dois jogadores, $G^N_A$, jogado no espaço de estados do autômato. O jogo é parametrizado por um número natural $N$ (ou $\infty$).
  • Jogadores: $\exists$ (Eloise) tenta construir uma árvore que exija testemunhas de alto posto, enquanto $\forall$ (Abelard) tenta mostrar que testemunhas de posto inferior são suficientes.
  • Mecânica: O jogo envolve a seleção de transições, direções e "seletores" que rastreiam o potencial aninhamento de "pentes" (estruturas que representam alto posto). O jogo rastreia dois lados, R (alcance) e T (tronco), para modelar o processo de derivada usado para definir postos ordinais.
  • Condições de Vitória: As condições de vitória são $\omega$-regulares. $\exists$ vence se ela conseguir forçar um caminho que mude de lado de R para T pelo menos $N$ vezes (para $N$ finito), ou infinitamente muitas vezes (para $N=\infty$), ou se o jogo contiver caminhos de rejeição com ramificação insuficiente. $\forall$ vence se ele conseguir prevenir estas condições.
• Análise de Estratégia: Os autores provam que o jogo é determinado (pelo teorema de Büchi-Landweber) e que a existência de uma estratégia vencedora para $\exists$ em $G^\infty_A$ corresponde exatamente a $\text{rank}_R(\Gamma) = \omega_1$, enquanto uma estratégia vencedora para $\forall$ implica $\text{rank}_R(\Gamma) < \omega$.

3. Principais Contribuições e Resultados

O Teorema da Dicotomia Principal (Teorema 1.1):
Para qualquer fórmula MSO $\exists X. \varphi(\vec{Y}, X)$ onde $X$ é bem fundado, o ordinal $\text{rank}(\varphi)$ satisfaz uma dicotomia estrita:

1. Estritamente Pequeno: $\text{rank}(\varphi) < \omega^2$. Neste caso, existe um número natural computável $N$ tal que $\text{rank}(\varphi) < \omega \cdot N$.
2. Máximo: $\text{rank}(\varphi) = \omega_1$.

Além disso, é decidível qual destes dois casos ocorre para uma dada fórmula.

Resultados de Definibilidade (Seção 9):
O artigo investiga se a propriedade "$\text{rank}(X) \le \eta$" é expressável em MSO.

• Para $\eta < \omega$, a linguagem de árvores com posto $\le \eta$ é regular (definível em MSO).
• Para $\eta \ge \omega$, a linguagem não é regular. Consequentemente, o predicado $\text{rank}(X) \le \eta$ não pode ser expresso diretamente em MSO para $\eta \ge \omega$.
• No entanto, o teorema da dicotomia implica que, embora o MSO não possa definir postos grandes específicos, ele pode decidir implicitamente se o posto é limitado por $\omega^2$ ou se é ilimitado (atingindo $\omega_1$).

Aplicação ao $\mu$-Cálculo (Seção 10):
Os autores aplicam seus resultados ao ordinais de fechamento de fórmulas de ponto fixo no $\mu$-cálculo.

• Eles abordam uma questão levantada por Czarnecki sobre se uma fórmula do $\mu$-cálculo pode ter um ordinal de fechamento enumerável $\ge \omega^2$.
• Usando uma redução do $\mu$-cálculo para MSO na árvore binária, eles provam que, para pontos fixos vetoriais (onde as variáveis não ocorrem no escopo de outros operadores de ponto fixo), o ordinal de fechamento é ou $< \omega^2$ ou $\ge \omega_1$.
• Isto fornece uma prova alternativa e um procedimento de decisão para um resultado estabelecido recentemente por Afshari, Barlucchi e Leigh, com o benefício adicional da decidibilidade e aplicabilidade a modelos arbitrários (não apenas enumeráveis).

4. Significância e Alegações

O artigo afirma que sua principal contribuição é estabelecer uma dicotomia decidível para os postos ordinais de testemunhas bem fundadas em MSO.

• Impacto Teórico: Resolve a questão de quais ordinais podem aparecer como ordinais de fechamento em MSO, mostrando que o espectro possui um "gap": nenhum ordinal entre $\omega^2$ e $\omega_1$ é alcançável. O conjunto de postos alcançáveis é $\{ \alpha \mid \alpha < \omega^2 \} \cup \{ \omega_1 \}$.
• Decidibilidade: Ao contrário de muitos problemas em extensões de MSO, os autores mostram que determinar se o posto é limitado por $\omega^2$ é decidível.
• Robustez de $\text{rank}_R$: O artigo destaca que o posto de "profundidade em camadas" ($\text{rank}_R$) é uma medida mais robusta para a definibilidade MSO do que o posto padrão, pois permite o cálculo exato de valores até $\omega$, enquanto o posto padrão torna-se indefinível muito antes.
• Limitações: Os autores notam modestamente que, embora possam decidir se o posto é $< \omega^2$ ou $= \omega_1$, calcular o valor exato do posto (se este for $< \omega^2$) permanece um problema aberto para o posto padrão, embora seja computável para $\text{rank}_R$. Eles também esclarecem que seu resultado para o $\mu$-cálculo aplica-se a um fragmento específico (variáveis não no escopo de operadores de ponto fixo) e não se transfere imediatamente para o domínio geral do MSO devido às restrições de monotonicidade inerentes às iterações de ponto fixo.

Em resumo, o artigo demonstra que, embora o MSO não possa definir explicitamente postos ordinais grandes e arbitrários, ele possui poder suficiente para distinguir implicitamente entre postos "pequenos" (limitados por $\omega^2$) e postos "máximos" ($\omega_1$), uma distinção que é efetivamente decidível.