🔢 mathematics

Generalized Decidability via Brouwer Trees

Este artigo introduz um arcabouço em teoria de tipos homotópicos que generaliza a decidibilidade usando ordinais de Brouwer para estabelecer uma hierarquia de proposições $\alpha$ -decidíveis, caracterizando suas propriedades de fechamento sob operações lógicas e quantificadores, com todos os resultados formalizados em Cubical Agda.

Autores originais: Tom de Jong, Nicolai Kraus, Aref Mohammadzadeh, Fredrik Nordvall Forsberg

Publicado 2026-07-10

📖 6 min de leitura🧠 Leitura aprofundada

CC BY 4.0

Autores originais: Tom de Jong, Nicolai Kraus, Aref Mohammadzadeh, Fredrik Nordvall Forsberg

Artigo original sob licença CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Esta é uma explicação gerada por IA do artigo abaixo. Não foi escrita nem endossada pelos autores. Para precisão técnica, consulte o artigo original. Ler aviso legal completo

Imagine que você é um detetive tentando resolver um mistério. No mundo da ciência da computação, costumamos classificar os mistérios em três baldes: Decidível (podemos encontrar a resposta rapidamente), Semidecidível (podemos encontrar a resposta se for "sim", mas se for "não", podemos esperar para sempre) e Indecidível (não podemos resolvê-lo de forma alguma).

Mas e se existissem mistérios que fossem "mais" semidecidíveis do que outros? E se algumas respostas "sim" demorassem um pouco mais para serem encontradas, mas ainda assim não demorassem para sempre?

É exatamente isso que Tom de Jong, Nicolai Kraus, Aref Mohammadzadeh e Fredrik Nordvall Forsberg estão explorando em seu novo artigo. Eles sugerem uma maneira de medir exatamente quanto tempo leva para encontrar uma resposta "sim", usando um tipo especial de sistema numérico chamado ordinais de árvores de Brouwer. Pense nisso não como números comuns como 1, 2, 3, mas como uma escada mágica de passos de tempo que vai muito além do infinito.

A Escada Mágica do Tempo

Em sua estrutura, eles não dizem apenas "é solucionável". Eles dizem: "É $\alpha$ -decidível", onde $\alpha$ é um degrau específico em sua escada mágica.

Nível 1 (Decidível): Se um problema é 1-decidível, significa que você pode encontrar a resposta (ou provar que é impossível) em um número finito de passos. É como verificar se um número é primo; você apenas conta para cima e, eventualmente, sabe com certeza.
Nível $\omega + 1$ (Semidecidível): Se um problema é $(\omega + 1)$ -decidível, significa que, se a resposta for "sim", você a encontrará dentro de $\omega$ passos. Mas $\omega$ não é um número normal; ele representa "contar para sempre". Portanto, se a resposta for "sim", você eventualmente a encontrará, mas se a resposta for "não", você poderá continuar contando para sempre sem nunca parar. Esta é a definição clássica de "semidecidível".

Os autores provam que este novo sistema se encaixa perfeitamente no antigo. Se você tem um problema que é "decidível", ele se encaixa no degrau 1. Se é "semidecidível", ele se encaixa no degrau $\omega + 1$ . Mas a magia é que agora eles podem falar de degraios entre estes, ou muito acima deles.

O Mistério dos Primos Gêmeos

Para mostrar como isso funciona, eles usam um famoso enigma matemático: a Conjectura dos Primos Gêmeos. Ela pergunta: "Sempre existe um par de números primos (como 3 e 5, ou 11 e 13) que estão a apenas dois números de distância, não importa o quão alto você conte?"

Verificar se um par específico existe é fácil (decidível).
Verificar se qualquer par existe acima de um certo número é semidecidível (você continua procurando; se encontrar um, você para).
Mas a grande questão pergunta se isso é verdade para cada número.

Os autores mostram que esta questão específica é $\omega^2$ -decidível. Imagine $\omega$ como uma única linha infinita de passos. $\omega^2$ é como ter um número infinito dessas linhas empilhadas umas sobre as outras. Significa que, se um contraexemplo para a Conjectura dos Primos Gêmeos existir, você poderia encontrá-lo, mas pode levar um intervalo de tempo equivalente a caminhar através de uma pilha infinita de linhas infinitas.

Eles também observaram o que acontece quando você combina esses problemas:

E (AND): Se você tem dois problemas que são $\alpha$ -decidíveis, o seu "E" (ambos devem ser verdadeiros) também é $\alpha$ -decidível. É como verificar duas caixas; se você puder verificar ambas dentro do mesmo limite de tempo, está tudo bem.
OU (OR): Isto é mais complicado. Se você tem dois problemas, o seu "OU" (um ou outro é verdadeiro) só é garantido como decidível se o limite de tempo for pequeno o suficiente (especificamente, se o nível for algo como $\omega \cdot k + n$ ). Se o limite de tempo ficar grande demais, o "OU" pode quebrar as regras do sistema deles.

O Problema da "Escolha"

Aqui é onde fica realmente interessante. Os autores descobriram que, se você quiser combinar um número infinito de problemas "semidecidíveis" (como verificar a Conjectura dos Primos Gêmeos para cada número inicial), você esbarra em um muro. Sem uma regra matemática especial chamada Escolha Enumerável (Countable Choice), você não consegue provar que o resultado combinado é semidecidível.

De fato, eles provaram que, se você pudesse provar isso sem essa regra, isso quebraria outras leis fundamentes da lógica. Por isso, eles sugerem que, para fazer a matemática funcionar suavemente para combinações infinitas, você precisa assumir a Escolha Enumerável.

No entanto, eles também encontraram uma solução alternativa! Eles olharam para um tipo diferente de "semidecidível" chamado Sierpiński-semidecidível. Esta é uma versão ligeiramente mais fraca que permite que você combine listas infinitas sem precisar da regra da Escolha Enumerável. É como ter um tipo diferente de lanterna que não brilha tão intensamente quanto a original, mas não precisa de uma bateria (a regra da Escolha) para acender.

O Que Eles Não Resolveram

É importante saber o que este artigo não faz. Os autores são muito claros: eles não resolveram a Conjectura dos Primos Gêmeos. Eles apenas a usaram como um exemplo didático para mostrar como o seu novo instrumento de medição funciona.

Eles também admitem que não conhecem a forma completa de sua escada ainda. Eles suspeitam que, se você tiver um problema no degrau $\alpha$ e outro no degrau $\beta$ , e $\alpha$ for menor que $\beta$ , então o problema no degrau $\alpha$ também deve ser solucionável no degrau $\beta$ . Mas eles ainda não provaram isso para cada degrau da escada. É uma "conjectura" (um palpite forte), não um fato.

A Conclusão

Este artigo sugere uma nova maneira de falar sobre o quão difícil é encontrar uma resposta "sim" na matemática e na computação. Em vez de apenas dizer "podemos encontrar" ou "não podemos", eles nos dão uma régua precisa feita de passos infinitos. Eles provaram que esta régua funciona para as coisas que já conhecemos (decidível e semidecidível) e a usaram para medir problemas complexos como a Conjectura dos Primos Gêmeos, encontrando que eles se situam em uma altura específica e mensurável de $\omega^2$ .

Eles também mostraram que, embora esta régua seja poderosa, ela tem limites: combinar listas infinitas de problemas requer uma suposição específica (Escolha Enumerável), a menos que você mude para um tipo ligeiramente diferente de régua (Sierpiński-semidecidabilidade).

Tudo isso foi construído e verificado dentro de um programa de computador chamado Cubical Agda, que atua como um árbitro super rigoroso para garantir que cada passo de sua lógica seja perfeito. Portanto, embora as ideias sejam novas e empolgantes, a matemática por trás delas é sólida como uma rocha.

Resumo Técnico: Decidibilidade Generalizada via Árvores de Brouwer

Enunciado do Problema
Na matemática construtiva e na teoria da computabilidade sintética, a classificação padrão de proposições em "decidíveis", "semidecidíveis" ou "indecidíveis" é frequentemente demasiado grosseira. Por exemplo, enquanto a decidibilidade da primalidade é clara, o status da Conjectura dos Primos Gêmeos (se um par de primos gêmeos existe acima de qualquer $n$ ) envolve uma estrutura de $\omega$ -muitos subproblemas semidecidíveis. Classicamente, isso poderia ser visto como um limite de limites, mas os frameworks construtivos exigem uma forma mais precisa de medir a "duração" ou a complexidade da busca por evidências. Noções existentes de ordinais (por exemplo, Formas Normais de Cantor sintáticas ou relações bem-fundadas semânticas) falham em fornecer uma hierarquia adequada: abordagens sintáticas tornam todas as comparações decidíveis (colapsando a hierarquia), enquanto abordagens semânticas muitas vezes falham em tornar as comparações semidecidíveis. O artigo aborda a necessidade de um framework que permita distinções mais finas na decidibilidade, especificamente para caracterizar proposições que requerem passos transfinitos para verificação.

Metodologia
Os autores trabalham dentro da Teoria dos Tipos Homotópicos (HoTT), utilizando os ordinais de árvores de Brouwer ( $\text{Brw}$ ) como base para sua hierarquia. Esses ordinais são definidos via um tipo indutivo-indutivo de quociente (QIIT) contendo construtores para zero, sucessores e limites de sequências estritamente crescentes. Crucialmente, o construtor de limite aceita apenas sequências estritamente crescentes, o que garante que a finitude seja decidível enquanto preserva a natureza construtiva da teoria.

A definição central introduzida é a $\alpha$ -decidibilidade: Uma proposição $P$ é $\alpha$ -decidível se existir um ordinal $y$ tal que $P \leftrightarrow (\alpha \leq y)$ . Esta definição generaliza conceitos existentes:

$1$-decidibilidade (ou $\omega$ -decidibilidade) corresponde à decidibilidade padrão.
$(\omega + 1)$ -decidibilidade (equivalente a $\omega \cdot 2$ -decidibilidade) corresponde à semidecidibilidade.

Os autores formalizam todos os resultados em Cubical Agda, aproveitando o suporte nativo para QIITs e univalência. Eles empregam técnicas específicas para lidar com a complexidade de definir funções em QIITs, como definir relações em construtores de pontos primeiro e extrair funções posteriormente para evitar a explosão combinatória no tratamento de construtores de caminhos.

Principais Contribuições e Resultados

Hierarquia de Decidibilidade:
- O artigo estabelece que a $\alpha$ -decidibilidade generaliza a decidibilidade e a semidecidibilidade.
- Demonstra-se que, para qualquer ordinal $\alpha$ , a $(\alpha+1)$ -decidibilidade é equivalente à $(\alpha+\omega)$ -decidibilidade. Consequentemente, a hierarquia pode ser efetivamente indexada por ordinais limites (não-sucessores).
- Os autores provam que, se $P$ é $\alpha$ -decidível e $Q$ é $\alpha$ -decidível, então $P \land Q$ é $\alpha$ -decidível. Isso depende da construção de uma função de mínimo binário para não-sucessores, o que não é geralmente possível para ordinais arbitrários sem implicar o Princípio do Ómnibus Limitado (LPO).
Disjunção e Máximos:
- Embora a conjunção seja fechada no mesmo nível, a disjunção binária não é fechada para $\alpha$ arbitrários. No entanto, os autores provam que proposições $(\omega \cdot k + n)$ -decidíveis são fechadas sob disjunção binária. Isso requer a construção de uma função de máximo binário relativa a ordinais da forma $\omega \cdot k$ .
- A existência de máximos binários globais para não-sucessores mostra que o LPO é implicado, um tabu construtivo.
Quantificadores Contáveis e Famílias:
- Encontros Contáveis (Meets): Para uma família de proposições semidecidíveis $P: \mathbb{N} \to \text{Prop}$ , o encontro contável $\forall i. P(i)$ é provado ser $\omega^2$ -decidível. Este resultado é aplicado à Conjectura dos Primos Gêmeos, caracterizando-a como $\omega^2$ -decidível.
- Uniões Contáveis (Joins): A união contável $\exists i. P(i)$ de proposições semidecidíveis é mostrada como sendo $(\omega \cdot 3)$ -decidível.
- Alternâncias de Quantificadores: O artigo analisa fórmulas com quantificadores alternados. Para uma família $P(n, m)$ onde $P(n, m) \to P(n, m+1)$ , a proposição $\exists m. \forall n. P(n, m)$ é mostrada como sendo $(\omega^2 + \omega)$ -decidível. Isso fornece um limite ordinal preciso para a busca de contraexemplos para a Conjectura dos Primos G gêmeos.
Relação com Princípios de Escolha:
- Os autores investigam o impacto da Escolha Contável (AC). Assumindo AC, a união contável de proposições semidecidíveis torna-se semidecidível (ou seja, $(\omega \cdot 3)$ -decidível colapsa para $(\omega \cdot 2)$ -decidível).
- No entanto, mesmo com AC, as proposições $\omega^2$ -decidíveis não colapsam para semidecidíveis a menos que o Princípio de Markov implique o LPO.
- O artigo introduz a Sierpiński-semidecidibilidade (baseada no tipo de Sierpiński, a ordem parcial $\omega$ -completa livre) como uma noção alternativa de semidecidibilidade, que é fechada sob uniões contáveis sem assumir a Escolha Contável. Mostra-se que a Sierpiński-semidecidibilidade é mais fraca que a semidecidibilidade padrão.

Significância e Alegações
Os autores posicionam este trabalho como o primeiro passo em direção a uma teoria de decidibilidade generalizada. Eles alegam fornecer um framework onde a "duração" de algoritmos (em um sentido construtivo e abstrato) pode ser precisamente especificada e provada usando aritmética de ordinais.

O artigo nota modestamente que não resolve problemas abertos como a própria Conjectura dos Primos Gêmeos; em vez disso, fornece uma linguagem formal para descrever a complexidade de tais problemas. Destaca que a hierarquia de decidibilidade não é totalmente compreendida, notando especificamente que permanece uma questão aberta se a $\alpha$ -decidibilidade implica $\beta$ -decidibilidade para todo $\alpha \leq \beta$ (embora resultados parciais sejam fornecidos). O trabalho também deixa em aberto a questão de se os ordinais de árvores de Brouwer são a noção ótima para esta teoria ou se construções de ordinais alternativas poderiam resultar em hierarquias diferentes, potencialmente mais ricas.

Todos os resultados são rigorosamente formalizados em Cubical Agda, garantindo que a natureza construtiva das provas seja mantida e que as definições de ordinais e suas propriedades sejam computacionalmente sólidas dentro da teoria dos tipos.

A Escada Mágica do Tempo

O Mistério dos Primos Gêmeos

O Problema da "Escolha"

O Que Eles Não Resolveram

A Conclusão

Mais como este