Aplicaciones de la Lógica Categórica a la Lógica

Question

Esta es definitivamente una pregunta muy abierta.

He estado estudiando Lógica Categórica por un tiempo ahora --- he leído Sheaves in Geometry and Logic, Presentable Categories de Adámek & Rosický, Sketches of an Elephant y algunos otros textos fundamentales, lo suficiente como para quizás poder decir que estoy familiarizado con las ideas fundamentales de la lógica categórica -- y estoy teniendo una pequeña crisis de fe con respecto a cualquier aplicación real de la lógica categórica. Dado que vengo de la Teoría de Modelos, originalmente deseaba alguna nueva forma de entender resultados antiguos, pero reconozco que la Lógica Categórica es un campo diferente y por lo tanto no debería ser juzgada como un diccionario del pasado.

Aún así, parece que después de al menos 60 años -- contando desde la tesis de Lawvere -- no se ha producido una teoría real. Sí, los funtores pueden verse como modelos; sí, las categorías presentables son dibujables y sí, las categorías con suficiente estructura tienen una lógica interna. ¿Pero qué? Parece que todos los resultados que conectan la lógica con las categorías son curiosidades aisladas. Este párrafo es definitivamente polémico, pero realmente no entiendo cómo la Teoría de Categorías o los Topos nos ayudan a entender mejor la lógica. ¿Hay alguna conjetura de lógica dura que se haya demostrado usando categorías?

Answer 1

Hay muchas aplicaciones de la lógica categórica para la comprensión de la lógica en sí misma, incluyendo algunas que proporcionan conexiones e ideas inesperadas. No es cierto que no se haya producido ninguna teoría real, como puede atestiguar el libro de Makkai-Reyes "Lógica categórica de primer orden". Hay otros ejemplos de categorías que han clarificado la lógica en el sentido de haber demostrado cosas en lógica para las cuales no se conocen otras pruebas. Dado que estoy seguro de que hay instancias de las que no tengo conocimiento, a continuación solo citaré mi propio trabajo, dejando quizás que otras respuestas nos hablen sobre algunos otros ejemplos que podría no conocer.

Si bien es cierto que la lógica categórica puede proporcionar nuevas formas de comprender resultados antiguos, también ha contribuido a producir nuevos resultados en la lógica pura.

Uno de ellos son una serie de resultados sobre lógica infinitaria que fueron posibles después de un teorema de completitud para $\mathcal{L}_{\kappa^+, \kappa}$ (ver mi artículo "Generalizaciones infinitarias del teorema de completitud de Deligne"). Aunque Karp tenía teoremas de completitud para lógicas infinitarias, los esquemas que utilizaba estaban técnicamente fuera del fragmento $\mathcal{L}_{\kappa^+, \kappa}$ ya que algunos permiten que $\kappa$ muchas variables libres ocurran dentro de ellos. Resulta que sus resultados son un corolario del "correcto" teorema de completitud para el fragmento con la regla correcta (regla de transitividad transfinita) que es simplemente una manifestación de una generalización infinitaria de la regla de transitividad para las topologías de Grothendieck. Si no hubiera sido por el enfoque topos-teórico, no habría encontrado el esquema correcto para obtener la completitud.

Este teorema de completitud ha permitido obtener un teorema de omisión de tipos para lenguajes con cuantificadores infinitos, siempre que la categoría de modelos tenga colimitas dirigidas. De la misma manera en que el teorema de omisión de tipos para lógica finitaria e incluso para $\mathcal{L}_{\omega_1, \omega}$ permite aplicaciones a, por ejemplo, la teoría de modelos atómicos y primos, la versión para $\mathcal{L}_{\kappa^+, \kappa}$ tiene varias aplicaciones en la teoría de modelos de la lógica infinitaria más allá de $\mathcal{L}_{\omega_1, \omega}$. Y sin embargo, la demostración de este teorema de omisión de tipos es de naturaleza topos-teórica, ya que las demostraciones habituales de las versiones previamente conocidas no se generalizan, por lo que tuvo que utilizarse una nueva idea.

Estos nuevos teoremas de completitud también han permitido nuevas versiones de los teoremas de definibilidad de Beth para lógicas infinitarias, en las cuales el lenguaje de la fórmula explícita que define un predicado implícitamente definible se encuentra un nivel más alto en la jerarquía de lógicas. Estos se obtienen a través de técnicas topos-teóricas, y a su vez hicieron posible el análisis de antiguas conjeturas modelísticas (ver mi preprint "Teoremas de preservación para lógicas de primer orden fuertes"). No diría que es una conjetura difícil de probar una vez que se tienen las herramientas topos-teóricas adecuadas, pero la verdad es que ha permanecido intratable durante mucho tiempo cuando la gente intentaba abordarla utilizando técnicas descriptivas de teoría de conjuntos.

Finalmente, también debo mencionar mi trabajo tanto en la conjetura de categoricidad eventual de Shelah como en la conjetura de categoricidad de Shelah, así como extensiones de la conjetura a clases más generales de estructuras. Aunque este trabajo aún está bajo revisión, la idea clave que hizo posible tal análisis topos-teórico de las conjeturas y que ha sido verificada de forma independiente es la observación de que los modelos saturados están vinculados a la topología de doble negación en una categoría de presheaves, siendo la subtópica de doble negación la subtópica clasificada por $\kappa$ cuyo $\kappa$-punto es precisamente el modelo $\kappa$-saturado de la teoría. Toda la estrategia para probar la categoricidad eventual se basa en este hecho, que es de naturaleza topos-teórica. Además, algunas instancias de eliminación de hipótesis modelísticas como la amalgamación (que en este contexto coincide con la condición de Ore derecha para la categoría de modelos) son posibles considerando en su lugar la topología densa en los presheaves en esa categoría (que es otra presentación de la topología de doble negación).

Answer 2

Dudé mucho antes de escribir esta respuesta, porque siento que la pregunta actual ("¿Hay alguna conjetura lógica difícil que haya sido demostrada usando categorías?") depende de cómo se define la lógica dura. Idealmente, la pregunta debería haber definido el término, o al menos delimitado a través de algunos ejemplos/no ejemplos de lo que cuenta como conjeturas de "lógica dura".

Al final, opté por traer mi propia definición, que puede no ser del agrado de todos. Pero está bien: todos son bienvenidos a compartir sus definiciones en sus propias respuestas.

En mi interpretación, la lógica dura se refiere principalmente a teorías fundamentales, es decir, teorías que pueden servir de fundamento para las matemáticas, pero no preguntas sobre teorías domesticadas, el ámbito de la teoría clásica de modelos. Por ejemplo, examinar si ciertos sistemas de razonamiento formales (como cálculos secuenciales de proposiciones de segundo orden, formas de lógica lineal, teoría de tipos dependientes, etc.) o teorías axiomáticas de fuerza fundacional (por ejemplo, HA, PA, CZF, IZF, diversas extensiones, etc.) tienen propiedades algorítmicas y metateóricas clave (que van desde la consistencia, no demostrando ciertos principios malos, propiedades de existencia, canonicidad, existencia proyectiva, parametricidad, etc.) se consideraría lógica dura; definitivamente quedan fuera del alcance cosas como teorías de primer orden domesticadas (como ACF0, DCF0, la teoría del grafo de Farey, etc.) y propiedades domesticadas (como eliminación de cuantificadores, estabilidad, distalidad, o-minimalidad, etc.).

Resolver preguntas de interés en matemáticas tiende a requerir una combinación de ideas ad hoc con teoría general. Un ejemplo muy simple: se puede probar la consistencia de PA en ZFC produciendo un buen viejo modelo tarskiano (teoría general reutilizable), pero en realidad producir este modelo requiere construir $(\mathbb{N},+,\cdot)$ y verificar que satisface PA (una idea específica del problema).

Las matemáticas han logrado aislar cierta teoría general y reutilizable sobre sistemas fundamentales, bajo amplios paraguas como la teoría de conjuntos y la lógica categórica. Estos paraguas no son completamente independientes, por supuesto, por ejemplo, es ampliamente conocida la correspondencia entre el forcing y las categorías de haces.

Quisiera argumentar que para preguntas de tipo fundamental, los resultados generales de la lógica categórica son de hecho herramientas reutilizables fantásticas (aunque, como siempre, también se necesitan ideas e intuiciones ad-hoc para resolver problemas difíciles). Y en respuesta a su consulta específica, la lógica categórica ha sido de hecho protagonista en soluciones de conjeturas importantes. Permítame mencionar un ejemplo reciente.

La normalización para la teoría cúbica de tipos es tan "difícil" como puede ser una pregunta de lógica: es literalmente una pregunta algorítmica sobre un sistema formal de razonamiento que puede servir de fundamento para las matemáticas. Conjeturada por primera vez en 2016 y establecida por Sterling y Angiuli en 2021, la prueba de normalización para la teoría cúbica de tipos se basa esencialmente en el pegado de Artin, una técnica importante de la lógica categórica, realizada en el contexto de las categorías locamente cerradas cartesianas.

Hay muchos más ejemplos, por supuesto, esperemos que sean mencionados en otras respuestas por otras personas.

Ahora, al cuestionar el impacto de la lógica categórica, no es suficiente estar impresionado por los resultados estándar del tema. Se puede argumentar que, incluso a pesar de las contribuciones mencionadas anteriormente, los resultados generales de la lógica categórica siguen siendo de alguna manera demasiado superficiales para contar. Quizás así sea. Pero es crucial enfrentar la realidad de que las contribuciones son no obstante sin precedentes: al introducir algunos resultados clave de la lógica categórica parece ayudar en muchas situaciones, y en esas situaciones específicas ningún otro cuerpo general de resultados parece ayudar más, ni siquiera de manera comparable.

Es cierto que no todos los lógicos encontrarán que los tipos de preguntas mencionadas anteriormente estén alineadas con sus intereses de investigación (por ejemplo, si su enfoque principal son las teorías estables, entonces probablemente tendrá mejores y más poderosas alternativas a cualquier herramienta que la lógica categórica pueda ofrecer para las preguntas que le interesan). Pero muchos lógicos están interesados específicamente en preguntas de este tipo, y ese interés se ve reforzado por los continuos desarrollos en áreas adyacentes de la ciencia de la computación.

Finalmente, es importante reconocer no solo las conjeturas resueltas utilizando herramientas de lógica categórica, sino también las aplicaciones que previenen posibles conjeturas por completo, es decir, el uso proactivo de herramientas categóricas en investigaciones recientes. Por ejemplo, el sistema de este reciente preimpreso habría sido lo suficientemente interesante por sí solo para convertirse en objeto de conjeturas; afortunadamente, las herramientas provenientes principalmente de la lógica categórica permitieron a los autores construir un modelo del sistema y demostrar los teoremas de interés sobre la teoría justo cuando fue presentada. Esto sucede con mucha más frecuencia en entornos de bajo riesgo: numerosas preguntas del tipo "¿es X derivable en una teoría fundamental débil T" han sido desechadas en mi propio trabajo y enseñanza cuando pude construir modelos topos para refutarlas directamente. Muchos de nosotros tenemos la necesidad práctica de, por ejemplo, la semántica constructiva al menos ocasionalmente, y sería mucho menos agradable si desconocemos el resultado básico de que los modelos topos existen, o que las categorías con suficiente estructura tienen una lógica interna. Del mismo modo, ni siquiera necesitamos resultados particularmente profundos en lógica categórica (como teoremas de existencia sutiles) para construir un modelo de, digamos, Geometría Diferencial Sintética: no obstante, dudo que sepan si es consistente en el universo paralelo en el que la lógica categórica nunca llegó a existir.