Estoy tratando de abrirme camino en la Teoría de Tipos de Homotopía (HoTT) donde un matemático puede ver las pruebas como caminos. Intuitivamente, esto me lleva a la idea de una métrica en el espacio de las proposiciones matemáticas. ¿Se ha desarrollado esto?
En concreto, ¿existe una forma de analizar las pruebas cortas como geodésicas dentro del espacio de proposiciones matemáticas desde la perspectiva de la HoTT? Si es así, ¿podría formular esta métrica mediante la complejidad de Kolmogorov?
La respuesta corta es no .
La noción de longitud está relacionada con la distancia y la métrica, y todos estos son conceptos que la topología borra, por no hablar de la teoría de la homotopía. Las explicaciones populares de la teoría de tipos de homotopía en términos de caminos topológicos (mapas continuos $[0,1] \to X$ ) pretenden ayudar a la intuición, pero no deben ni pueden entenderse literalmente. Los espacios topológicos no constituyen un modelo de teoría de tipos de homotopía.
Dado que estás intentando abrirte camino en la teoría de tipos de homotopía, podrías sacar tu intuición de varios lugares, dependiendo de tu formación, en orden decreciente de abstracción y corrección:
Teoría de las categorías superiores: un $(\infty,1)$ -topos es más o menos un modelo de teoría de tipos de homotopía, mientras que un $\infty$ -groupoid es como un tipo único.
Teoría de la homotopía: Los conjuntos simpliciales, y más concretamente Complejos Kan forman un modelo de teoría de tipos de homotopía , por lo que se puede pensar en un tipo como un complejo Kan. En general, ciertos tipos de categorías de modelos puede utilizarse para interpretar (partes de) la teoría de tipos de homotopía .
Groupoides: a groupoid es como un tipo 1 en la teoría de tipos de homotopía. Se puede pensar en $\mathsf{Id}_A(a,b)$ como la colección de todos los isomorfismos de $a$ a $b$ en un grupúsculo $A$ .
En todos los casos, los "caminos" son de carácter abstracto. Por ejemplo, los isomorfismos en un groupoide no tienen por qué ser caminos, al igual que los morfismos en una categoría no tienen por qué ser funciones.
Hay adaptaciones de la teoría de tipos de homotopía que hacer relacionar los modelos homotópicos abstractos con modelos topológicos, e incluso lisos. Éstos reciben el nombre de teoría de la homotopía cohesiva pero no estoy seguro de que sea el mejor punto de partida para aprender la teoría de tipos de homotopía.
Déjeme intentar una respuesta más larga. (La respuesta de @Andrej Bauer trata sobre todo de aprender la teoría de tipos de homotopía, en lugar de profundizar en tu pregunta).
Como es lógico, la respuesta sigue siendo no . Se podría intentar definir la longitud de un camino por el tamaño del más pequeño de sus testigos. Pero esa definición se basa en sintaxis Es decir, hay que tener un "lenguaje" en el que se expresan los testigos. La cuestión es que, aunque la HoTT da lugar a lenguajes de programación de forma bastante natural (véase mi trabajo con Amr Sabry), todavía no son realmente "canónicos". Mientras que $\left(\infty,1\right)$ -topos ciertamente apuntan en la dirección correcta, no está resuelto aún si no queremos de hecho un poco más de estructura (ver el trabajo de Shulman, Riehl, etc. si quieres bucear en lo realmente profundo de eso). Así que ni siquiera sabemos en qué estructura externa trabajar, ni siquiera en la lenguaje interno que acabaremos teniendo dentro de esa estructura.
Incluso si todo eso se resolviera, ¿por qué esperar que el lenguaje interno sea Turing-completo? Esa es una de las piedras angulares de la validez de la complejidad de Kolmogorov. Sin ella, longitud se convierte en una noción bastante caprichosa. Incluso con la complejidad de Kolmogorov, longitud sigue siendo una noción "difusa", porque sólo está definida hasta una constante. Así que, aunque existiera, no nos diría mucho sobre las pruebas "cortas", sólo nos dice algo interesante cuando tenemos una prueba que es significativamente más corta que las demás. Ciertamente, no hay esperanza de que tal noción de longitud sea una métrica, y mucho menos de que pueda esculpir geodésicas.
No obstante, mantengo la esperanza de que haya alguna noción de "tamaño" que resulte informativa y significativa. Sólo que no va a ser sencillo, ni tan informativo como uno quisiera.
I-Ciencias es una comunidad de estudiantes y amantes de la ciencia en la que puedes resolver tus problemas y dudas.
Puedes consultar las preguntas de otros usuarios, hacer tus propias preguntas o resolver las de los demás.
1 votos
En cambio, los lógicos suelen analizar las proposiciones matemáticas por sus clases de equivalencia, a veces de forma grosera (por ejemplo, los cinco subsistemas de la aritmética de segundo orden en la matemática inversa), a veces de forma más fina (por ejemplo, la jerarquía de fuerza de consistencia en la teoría de conjuntos).