Hindman's theorem does not code $\emptyset^{(\omega)}$ in one application

Resumo Técnico: "O Teorema de Hindman não codifica $\emptyset^{(\omega)}$ em uma única aplicação"

Enunciado do Problema
O artigo aborda a complexidade da teoria da computabilidade do Teorema de Hindman (HT), especificamente no que diz respeito à força das soluções que ele produz em relação à coloração de entrada. O Teorema de Hindman estabelece que, para toda coloração finita dos números naturais $\mathbb{N}$, existe um conjunto infinito $H$ tal que o conjunto de todas as somas finitas de elementos distintos de $H$ (denotado por $FS(H)$) é monocromático.

Trabalhos anteriores estabeleceram os seguintes limites:

1. Limite Superior: Blass, Hirst e Simpson (1987) provaram que, para toda coloração computável, existe uma solução computável a partir do salto $\omega$ do conjunto vazio, $\emptyset^{(\omega)}$.
2. Limite Inferior: Os mesmos autores provaram que existe uma coloração computável onde toda solução computa o conjunto de parada $\emptyset'$. Posteriormente, Liao (2026) melhorou isso ao mostrar que, para algumas colorações computáveis, não existe uma solução $\Pi^0_3$.

A questão central aberta abordada por este artigo é se o limite superior de $\emptyset^{(\omega)}$ é ótimo para uma única aplicação do teorema. Especificamente, todo caso aritmético do Teorema de Hindman admite uma solução que não computa $\emptyset^{(\omega)}$?

Metodologia
Os autores empregam uma técnica de forcing adaptada da prova combinatória de Hindman de Towsner. A metodologia envolve os seguintes componentes:

1. Reformulação: O problema é traduzido para a linguagem do Teorema da União Finita (FUT), que é computacionalmente equivalente ao HT. Isso envolve colorir o conjunto das partes finitas não vazias de $\mathbb{N}$, $P_{fin}(\mathbb{N})$, e buscar uma sequência de blocos infinita $H$ tal que o conjunto das uniões finitas $FU(H)$ seja monocromático.
2. Árvores de Towsner e Correspondência (Matching): Os autores utilizam os conceitos de "meia-correspondência" (half-match) e "correspondência total" (full-match) de Towsner. Um conjunto finito $F$ meio-corresponde a uma sequência de blocos infinita $X$ se, para cada união finita $b \in FU(X)$, houver um $a \in F$ tal que $f(a \cup b) = f(b)$. Uma correspondência total exige que $f(a) = f(a \cup b) = f(b)$.
   • Eles constroem uma "sequência de Towsner", uma sequência aninhada de meias-correspondências que induz uma estrutura de árvore (a árvore de Towsner).
   • Eles estabelecem que, para uma coloração aritmética $f$, uma sequência de Towsner computável a partir de $f''$ existe.
3. Noção de Forcing: Uma nova noção de forcing é definida usando "condições-P", que são pares $(I, X)$, onde $I$ é um conjunto finito de sequências de blocos e $X$ é um reservatório infinito. Uma condição é "f-correspondente" se satisfaz uma propriedade de extensão específica relacionada à coloração.
4. Controle do Primeiro Salto (First-Jump Control): A inovação central é o design de uma "pergunta de forcing" com propriedades de definibilidade específicas. Isso permite a construção de um filtro genérico onde a solução resultante $G$ evita computar um conjunto não aritmético específico $C$. A relação de forcing é projetada para controlar o primeiro salto da solução, garantindo que a solução permanene dentro de um grau aritmético específico relativo à entrada, enquanto evita o cone alvo.
5. Diagonalização: Para garantir que $C \not\leq_T G$, os autores satisfazem os requisitos $R^C_e: W^G_e \neq C$. Ao analisar a pergunta de forcing para fórmulas $\Sigma^0_1$, eles demonstram que, para qualquer conjunto não aritmético $C$ e coloração aritmética, é possível estender as condições para forçar $G$ a diferir de $C$ em algum elemento.

Contribuições Principais e Resultados

1. Teorema Principal (Evitação de Cone): O resultado principal (Teorema Principal 1.5) afirma: Seja $C$ um conjunto de grau não aritmético. Para todo $\ell \geq 1$ e toda coloração $f: \mathbb{N} \to \ell$ (ou $P_{fin}(\mathbb{N}) \to \ell$) de grau aritmético, existe um conjunto infinito $H$ tal que $FS(H)$é$f$-monocromático e $C \not\leq_T H$.

   • Corolário: Ao definir $C = \emptyset^{(\omega)}$, os autores provam que todo caso aritmético do Teorema de Hindman admite uma solução que não computa $\emptyset^{(\omega)}$. Isso demonstra que o limite superior computacional de $\emptyset^{(\omega)}$ não é ótimo para uma única aplicação de Hindman.

2. Limitações da Iteração: Os autores esclarecem que este resultado não implica que o Teorema de Hindman seja mais fraco que $\text{ACA}^+_0$ em matemática reversa. A evitação de cone ocorre para a redução de Turing ($C \not\leq_T H$), mas não necessariamente para a redução aritmética. Portanto, o teorema não pode ser iterado para construir um modelo-$\omega$ do Teorema de Hindman que exclua $\emptyset^{(\omega)}$.

3. Colorações Simples: O artigo investiga as restrições do HT a "colorações simples" (colorações onde a cor de uma união depende apenas das cores dos componentes e suas posições relativas).

   • Eles provam que a restrição do Teorema da União Finita a colorações simples é equivalente a $\text{ACA}_0$ sobre $\text{RCA}_0$.
   • Eles mostram que a coloração específica usada por Blass, Hirst e Simpson para provar o limite inferior é uma coloração simples.

4. Complexidade das Árvores de Towsner: Os autores provam (Proposição 2.24) que, para a coloração específica construída por Blass, Hirst e Simpson, toda sequência de Towsner computa $\emptyset'$. Isso sugere que, embora as árvores de Towsner sejam uma ferramenta poderosa, sua existência para certas colorações computáveis inerentemente codifica um poder computacional significativo, embora isso não impeça a existência de outras provas ou correspondências totais que não dependam de tais árvores.

Significância
O artigo resolve a questão de se o limite superior $\emptyset^{(\omega)}$ é apertado para aplicações únicas do Teorema de Hindman. Ao provar que cones não aritméticos podem ser evitados, os autores mostram que o teorema não requer inerentemente a força total do salto $\omega$ para produzir uma solução para entradas aritméticas. Isso refina a compreensão do conteúdo computacional do teorema, distinguindo entre a complexidade necessária para encontrar uma solução versus a complexidade necessária para encontrar uma solução que computa conjuntos de alto grau específicos. O trabalho também une provas combinatórias (de Towsner) com técnicas de forcing para alcançar um controle preciso sobre os graus de Turing das soluções.