🔢 mathematics

Generalized Decidability via Brouwer Trees

Este artículo introduce un marco en la teoría de tipos homotópicos que generaliza la decidibilidad utilizando ordinales de Brouwer para establecer una jerarquía de proposiciones $\alpha$ -decidibles, caracterizando sus propiedades de clausura bajo operaciones lógicas y cuantificadores, con todos los resultados formalizados en Cubical Agda.

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

Publicado 2026-07-10

📖 6 min de lectura🧠 Análisis profundo

CC BY 4.0

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

Artículo original bajo licencia CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Esta es una explicación generada por IA del artículo a continuación. No ha sido escrita ni avalada por los autores. Para mayor precisión técnica, consulte el artículo original. Leer descargo de responsabilidad completo

Imagina que eres un detective intentando resolver un misterio. En el mundo de la informática, solemos clasificar los misterios en tres cubos: Decidible (podemos encontrar la respuesta rápidamente), Semidecidible (podemos encontrar la respuesta si es "sí", pero si es "no", podríamos esperar para siempre) e Indecidible (no podemos resolverlo en absoluto).

Pero, ¿qué pasa si hay misterios que son "más" semidecidibles que otros? ¿Qué pasa si algunas respuestas "sí" tardan un poco más en encontrarse, pero aun así no tardan una eternidad?

Eso es exactamente lo que Tom de Jong, Nicolai Kraus, Aref Mohammadzadeh y Fredrik Nordvall Forsberg están explorando en su nuevo artículo. Sugieren una forma de medir exactamente cuánto tiempo toma encontrar una respuesta "sí", utilizando un tipo especial de sistema numérico llamado ordinales de árboles de Brouwer. Piensa en ellos no como números regulares como 1, 2, 3, sino como una escalera mágica de pasos temporales que va mucho más allá del infinito.

La Escalera Mágica del Tiempo

En su marco de trabajo, no se limitan a decir "es soluble". Diccion, dicen: "Es $\alpha$ -decidible", donde $\alpha$ es un peldaño específico en su escalera mágica.

Nivel 1 (Decidible): Si un problema es 1-decidible, significa que puedes encontrar la respuesta (o probar que es imposible) en un número finito de pasos. Es como comprobar si un número es primo; simplemente vas contando hacia arriba y, eventualmente, lo sabes con certeza.
Nivel $\omega + 1$ (Semidecidible): Si un problema es $(\omega + 1)$ -decidible, significa que si la respuesta es "sí", la encontrarás dentro de $\omega$ pasos. Pero $\omega$ no es un número normal; representa "contar para siempre". Por lo tanto, si la respuesta es "sí", eventualmente la encontrarás, pero si la respuesta es "no", podrías seguir contando para siempre sin detenerte nunca. Esta es la definición clásica de "semidecidible".

Los autores demuestran que este nuevo sistema encaja perfectamente con el antiguo. Si tienes un problema que es "decidible", encaja en el peldaño 1. Si es "semidecidible", encaja en el peldaño $\omega + 1$ . Pero la magia es que ahora pueden hablar de peldaños entre estos, o mucho por encima de ellos.

El Misterio de los Primos Gemelos

Para mostrar cómo funciona esto, utilizan un famoso acertijo matemático: la Conjetura de los Primos Gemelos. Esta pregunta: "¿Existe siempre un par de números primos (como el 3 y el 5, o el 11 y el 13) que estén separados solo por dos números, sin importar qué tan alto cuentes?)".

Comprobar si existe un par específico es fácil (decidible).
Comprobar si existe cualquier par por encima de un cierto número es semidecidible (simplemente sigues buscando; si encuentras uno, te detienes).
Pero la gran pregunta es si esto es cierto para cada número.

Los autores demuestran que esta pregunta específica es $\omega^2$ -decidible. Imagina que $\omega$ es una sola línea infinita de pasos. $\omega^2$ es como tener un número infinito de esas líneas apiladas unas sobre otras. Significa que si existiera un contraejemplo a la Conjetura de los Primos Gemelos, podrías encontrarlo, pero podría tomarte un lapso de tiempo equivalente a caminar a través de una pila infinita de líneas infinitas.

También analizaron qué sucede cuando combinas estos problemas:

AND (Y): Si tienes dos problemas que son $\alpha$ -decidibles, su "AND" (ambos deben ser ciertos) también es $\alpha-decidible$ . Es como revisar dos casillas; si puedes revisar ambas dentro del mismo límite de tiempo, estás bien.
OR (O): Esto es más complicado. Si tienes dos problemas, su "OR" (uno de los dos debe ser cierto) solo es garantizado como decidible si el límite de tiempo es lo suficientemente pequeño (específicamente, si el nivel es algo como $\omega \cdot k + n$ ). Si el límite de tiempo se vuelve demasiado grande, el "OR" podría romper las reglas de su sistema.

El Problema de la "Elección"

Aquí es donde se pone realmente interesante. Los autores descubrieron que si quieres combinar un número infinito de problemas "semidecidibles" (como comprobar la Conjetura de los Primos Gemelos para cada número inicial), te topas con un muro. Sin una regla matemática especial llamada Elección Contable, no puedes probar que el resultado combinado sea semidecidible.

De hecho, demostraron que si pudieras probarlo sin esa regla, romperías otras leyes fundamentales de la lógica. Así que sugieren que, para que las matemáticas funcionen fluidamente para las combinaciones infinitas, necesitas asumir la Elección Contable.

Sin embargo, ¡también encontraron una solución alternativa! Miraron un tipo diferente de "semidecidible" llamado Sierpiński-semidecidible. Es una versión ligeramente más débil de la semidecidibilidad que sí permite combinar listas infinitas sin necesidad de la regla de Elección Contable. Es como tener un tipo diferente de linterna que no brilla tan intensamente como la original, pero que no necesita una batería (la regla de Elección) para encenderse.

Lo Que No Resolvieron

Es importante saber qué es lo que este artículo no hace. Los autores son muy claros: no han resuelto la Conjetura de los Primos Gemelos. Simplemente la usaron como un ejemplo de juguete para mostrar cómo funciona su nueva vara de medir.

También admiten que aún no conocen la forma completa de su escalera. Sospechan que si tienes un problema en el peldaño $\alpha$ y otro en el $\beta$ , y $\alpha$ es más bajo que $\beta$ , entonces el problema en $\alpha$ también debería ser soluble en $\beta$ . Pero aún no han probado esto para cada uno de los peldaños de la escalera. Es una "conjetura" (una suposición fuerte), no un hecho.

La Conclusión

Este artículo sugiere una nueva forma de hablar sobre qué tan difícil es encontrar una respuesta "sí" en las matemáticas y la informática. En lugar de solo decir "podemos encontrarla" o "no podemos", nos dan una regla precisa hecha de pasos infinitos. Demostraron que esta regla funciona para lo que ya conocemos (decidible y semidecidible), y la usaron para medir problemas complejos como la Conjetura de los Primos Gemelos, encontrando que se sitúan en una altura específica de $\omega^2$ .

También demostraron que, aunque esta regla es poderosa, tiene límites: combinar listas infinitas de problemas requiere un supuesto específico (Elección Contable), a menos que cambies a un tipo de regla ligeramente diferente (Sierpiński-semidecidibilidad).

Todo esto fue construido y verificado dentro de un programa informático llamado Cubical Agda, que actúa como un árbitro súper estricto para asegurar que cada uno de los pasos de su lógica sea perfecto. Así que, aunque las ideas son nuevas y emocionantes, la matemática detrás de ellas es sólida como una roca.

Resumen Técnico: Decidibilidad Generalizada mediante Árboles de Brouwer

Planteamiento del Problema
En la matemática constructiva y la teoría de la computabilidad sintética, la clasificación estándar de las proposiciones en "decidibles", "semidecidibles" o "indecidibles" suele ser demasiado gruesa. Por ejemplo, mientras que la decidibilidad de la primalidad es clara, el estatus de la Conjetura de los Primos Gemelos (si existe un par de primos gemelos por encima de cualquier $n$ ) involucra una estructura de $\omega$ -muchos subproblemas semidecidibles. Clásicamente, esto podría verse como un límite de límites, pero los marcos constructivos requieren una forma más precisa de medir la "duración" o complejidad de la búsqueda de evidencia. Las nociones existentes de ordinales (por ejemplo, formas normales de Cantor sintácticas o relaciones bien fundadas semánticas) no proporcionan una jerarquía adecuada: los enfoques sintácticos hacen que todas las comparaciones sean decidibles (colapsando la jerarquía), mientras que los enfoques semánticos a menudo fallan en hacer que las comparaciones sean semidecidibles. El artículo aborda la necesidad de un marco que permita distinciones más finas en la decidibilidad, específicamente para caracterizar proposiciones que requieren pasos transfinitos para su verificación.

Metodología
Los autores trabajan dentro de la Teoría de Tipos Homotópicos (HoTT), utilizando los ordinales de árboles de Brouwer ( $\text{Brw}$ ) como base para su jerarquía. Estos ordinales se definen mediante un tipo inductivo-inductivo de cociente (QIIT) que contiene constructores para cero, sucesores y límites de secuencias estrictamente crecientes. Crucialmente, el constructor de límite acepta solo secuencias estrictamente crecientes, lo que asegura que la finitud sea decidible preservando al mismo tiempo la naturaleza constructiva de la teoría.

La definición central introducida es la $\alpha$ -decidibilidad: Una proposición $P$ es $\alpha$ -decidible si existe un ordinal $y$ tal que $P \leftrightarrow (\alpha \leq y)$ . Esta definición generaliza conceptos existentes:

La $1$-decidibilidad (o $\omega$ -decidibilidad) corresponde a la decidibilidad estándar.
La $(\omega + 1)$ -decidibilidad (equivalente a la $\omega \cdot 2$ -decidibilidad) corresponde a la semidecidibilidad.

Los autores formalizan todos los resultados en Cubical Agda, aprovechando el soporte nativo para QIITs y la univalencia. Emplean técnicas específicas para manejar la complejidad de definir funciones sobre QIITs, como definir primero relaciones sobre los constructores de puntos y extraer las funciones después para evitar la explosión combinatoria en el manejo de los constructores de caminos.

Contribuciones Clave y Resultados

Jerarquía de Decidibilidad:
- El artículo establece que la $\alpha$ -decidibilidad generaliza la decidibilidad y la semidecidibilidad.
- Se demuestra que, para cualquier ordinal $\alpha$ , la $(\alpha+1)$ -decidibilidad es equivalente a la $(\alpha+\omega)$ -decidibilidad. En consecuencia, la jerarquía puede ser indexada efectivamente por ordinales límite (ordinales no sucesores).
- Los autores prueban que si $P$ es $\alpha$ -decidible y $Q$ es $\alpha$ -decidible, entonces $P \land Q$ es $\alpha$ -decidible. Esto se basa en la construcción de una función de mínimo binario para ordinales no sucesores, lo cual no es generalmente posible para ordinales arbitrarios sin implicar el Principio de Omnisciencia Limitada (LPO).
Disyunción y Máximos:
- Aunque la conjunción es cerrada en el mismo nivel, la disyunción binaria no es cerrada para un $\alpha$ arbitrario. Sin embargo, los autores prueban que las proposiciones $(\omega \cdot k + n)$ -decidibles son cerradas bajo disyunción binaria. Esto requiere la construcción de una función de máximo binario relativa a ordinales de la forma $\omega \cdot k$ .
- Se muestra que la existencia de máximos binarios globales para no sucesores implica LPO, un tabú constructivo.
Cuantificadores Contables y Familias:
- Ínfimos Contables: Para una familia de proposiciones semidecidibles $P: \mathbb{N} \to \text{Prop}$ , el ínfimo contable $\forall i. P(i)$ se demuestra que es $\omega^2$ -decidible. Este resultado se aplica a la Conjetura de los Primos Gemelos, caracterizándola como $\omega^2$ -decidible.
- Supremos Contables: El supremo contable $\exists i. P(i)$ de proposiciones semidecidibles se muestra que es $(\omega \cdot 3)$ -decidible.
- Alternancias de Cuantificadores: El artículo analiza fórmulas con cuantificadores alternos. Para una familia $P(n, m)$ donde $P(n, m) \to P(n, m+1)$ , la proposición $\exists m. \forall n. P(n, m)$ se muestra que es $(\omega^2 + \omega)$ -decidible. Esto proporciona un límite ordinal preciso para la búsqueda de contraejemplos a la Conjetura de los Primos Gemelos.
Relación con los Principios de Elección:
- Los autores investigan el impacto de la Elección Contable (AC). Asumiendo AC, el supremo contable de proposiciones semidecidibles se vuelve semidecidible (es decir, la $(\omega \cdot 3)$ -decidibilidad colapsa a $(\omega \cdot 2)$ -decidibilidad).
- Sin embargo, incluso con AC, las proposiciones $\omega^2$ -decidibles no colapsan a semidecidibles a menos que el Principio de Markov implique LPO.
- El artículo introduce la semidecidibilidad de Sierpiński (basada en el tipo de Sierpiński, el orden parcial $\omega$ -completo libre) como una noción alternativa de semidecidibilidad que es cerrada bajo supremos contables sin asumir la Elección Contable. Se muestra que la semidecidibilidad de Sierpiński es más débil que la semidecidibilidad estándar.

Significado y Reivindicaciones
Los autores posicionan este trabajo como el primer paso hacia una teoría de la decidibilidad generalizada. Reivindican haber proporcionado un marco donde la "duración" de los algoritmos (en un sentido constructivo y abstracto) puede especificarse y probarse con precisión utilizando la aritmética de ordinales.

El artículo señala modestamente que no resuelve problemas abiertos como la propia Conjetura de los Primos Gemelos; más bien, proporciona un lenguaje formal para describir la complejidad de tales problemas. Destaca que la jerarquía de decidibilidad no está totalmente comprendida, señalando específicamente que sigue siendo una pregunta abierta si la $\alpha$ -decidibilidad implica la $\beta$ -decidibilidad para todo $\alpha \leq \beta$ (aunque se proporcionan resultados parciales). El trabajo también deja abierta la cuestión de si los ordinales de árboles de Brouwer son la noción óptima para esta teoría o si construcciones de ordinales alternativas podrían producir jerarquías diferentes y potencialmente más ricas.

Todos los resultados están formalizados rigurosamente en Cubical Agda, asegurando que la naturaleza constructiva de las pruebas se mantenga y que las definiciones de los ordinales y sus propiedades sean computacionalmente sólidas dentro de la teoría de tipos.

La Escalera Mágica del Tiempo

El Misterio de los Primos Gemelos

El Problema de la "Elección"

Lo Que No Resolvieron

La Conclusión

Más como este