Conceptual completeness for subgeometric logics

Título: Completitud Conceptual para Lógicas Subgeométricas
Autores: Ivan Di Liberti, Umberto Tarantino y Lingyuan Ye

1. Problema y Motivación

El artículo aborda la noción de completitud conceptual dentro del marco de las lógicas subgeométricas (fragmentos de la lógica geométrica). Tradicionalmente, la completitud conceptual, establecida por Makkai para la lógica coherente de primer orden [Mak87], se interpreta como un teorema de reconstrucción: la sintaxis de una teoría puede recuperarse de su semántica (la categoría de modelos) siempre que esta última esté dotada de una estructura adicional (específicamente, una "ultraestructura" derivada de los ultraproductos).

Los autores identifican una limitación en esta visión tradicional: depende fuertemente de la semántica basada en conjuntos y de la imposición de una estructura extra (ultraestructura) sobre las categorías de modelos. Además, los enfoques previos para probar la completitud conceptual para diversos fragmentos lógicos a menudo requerían técnicas independientes y ad hoc para cada fragmento. El artículo busca:

1. Reformular la completitud conceptual como un fenómeno puramente sintáctico, específicamente como una dualidad entre teorías y sus topoi clasificadores, en lugar de una reconstrucción a partir de modelos basados en conjuntos.
2. Proporcionar un marco modular para probar la completitud conceptual para diversas lógicas subgeométricas sin depender del teorema de reconstrucción original de Makkai o imponer estructuras artificiales en la semántica.
3. Clarificar la relación entre esta nueva noción sintáctica y la tradicional reconstrucción semántica de Makkai, particularmente bajo el supuesto de la completitud con respecto a modelos basados en conjuntos.

2. Metodología y Marco de Trabajo

Los autores se basan en el marco de la inyectividad de Kan por la derecha en la 2-categoría de topoi ($\mathbf{Topoi}$), desarrollado en su trabajo previo [DLY25].

• Lógicas como Clases de Morfismos: Una lógica $\mathcal{H}$ se define como una clase de morfismos geométricos entre topoi. Un topos $\mathcal{X}$ "pertenece formalmente" a $\mathcal{H}$ si es (débilmente) inyectivo por la derecha con respecto a los morfismos de $\mathcal{H}$. Esto captura la idea de que los puntos generalizados del topos admiten la estructura prescrita por la lógica.
• Categorías Sintácticas y Topoi Clasificadores:
  • Para un topos $\mathcal{X}$ formalmente en $\mathcal{H}$, la categoría sintáctica $\text{Syn}_{\mathcal{H}}(\mathcal{X})$ se define como la categoría de morfismos geométricos $\mathcal{X} \to \text{Set}[\mathcal{O}]$ (donde $\text{Set}[\mathcal{O}]$ es el clasificador de objetos).
  • Asociado con $\mathcal{H}$ hay un monada de sintaxis $T_{\mathcal{H}}$ sobre la categoría de categorías pequeñas finitamente completas ($\mathbf{Lex}$).
  • El topos clasificador $\text{Cl}_{\mathcal{H}}(A)$ se construye para un $T_{\mathcal{H}}$-álgebra $A$.
• Definición de Completitud Conceptual: Una lógica acotada $\mathcal{H}$ es conceptualmente completa si el 2-functor $\text{Cl}_{\mathcal{H}}: \text{Alg}(T_{\mathcal{H}})^{\text{op}} \to \mathbf{WRInj}(\mathcal{H})$ es 2-plenamente fiel.
• Idea Clave: Los autores muestran que la completitud conceptual es equivalente a que la adjunción $\text{Syn}_{\mathcal{H}} \dashv \text{Cl}_{\mathcal{H}}$ sea una reflexión (es decir, que la unidad sea un equivalencia). Esto significa que cada $T_{\mathcal{H}}$-álgebra es esencialmente la categoría sintáctica de su topos clasificador. Esta formulación desprende el concepto de la semántica basada en conjuntos y se centra en la relación entre la sintaxis (álgebras) y la semántica basada en la sintaxis (topoi clasificadores).

3. Contribuciones Clave y Resultados

A. Caracterización de la Completitud Conceptual

El artículo establece que una lógica $\mathcal{H}$ es conceptualmente completa si y solo si, para cada $T_{\mathcal{H}}$-álgebra pequeña $A$, la inmersión $A \hookrightarrow \text{Syn}_{\mathcal{H}}(\text{Cl}_{\mathcal{H}}(A))$ es una equivalencia de categorías (Corolario 2.2.3). Esto replantea el problema como la determinación de si la categoría sintáctica del topos clasificador recupera el álgebra original.

B. Prueba de la Completitud Conceptual para Cuatro Lógicas

Utilizando un Lema de Reducción (Proposición 3.1.2), los autores prueban la completitud conceptual para cuatro lógicas específicas, identificándolas con doctrinas conocidas y mostrando que sus categorías sintácticas recuperan las álgebras. Las pruebas utilizan subclases específicas de morfismos (sublógicas) para simplificar el análisis:

1. Lógica Coherente ($\mathcal{H}_{\text{flat}}$): Probada como conceptualmente completa. Los autores muestran que la doctrina $T_{\mathcal{H}_{\text{flat}}}$ coincide con la construcción del pretopos libre. Caracterizan la categoría sintáctica de un topos coherente como la subcategoría plena de objetos coherentes, recuperando el pretopos original.
2. Lógica Regular ($\mathcal{H}_{\text{matte}}$): Probada como conceptualmente completa. La doctrina corresponde a la construcción de la categoría (Barr-)exacta libre. Se muestra que la categoría sintáctica consiste en objetos regulares.
3. Lógica Esencialmente Algebraica con Falsum ($\mathcal{H}_{\text{dom}}$): Probada como conceptualmente completa. La doctrina corresponde a la categoría lex libre con un objeto inicial estricto. La prueba implica analizar inmersiones densas y mostrar que los objetos en la categoría sintáctica son retractos de representables.
4. Lógica Disjuntiva Finitaria ($\mathcal{H}_{\text{pure}}$): Probada como conceptualmente completa. La doctrina corresponde a la construcción de la categoría lextensiva libre. La prueba utiliza "inmersiones puras" y la unión de una categoría con su álgebra booleana de subobjetos terminales decidibles.

Estos resultados proporcionan nuevas caracterizaciones para estas lógicas que no dependen del teorema original de Makkai [Mak87].

C. Lógicas Conservativamente Embebidas

El artículo introduce la noción de lógicas conservativamente embebidas (Sección 4). Una lógica está conservativamente embebida si la adjunción $\text{Syn}_{\mathcal{H}} \dashv \text{Cl}_{\mathcal{H}}$ es idempotente.

• Resultado: Toda lógica conceptualmente completa está conservativamente embebida.
• Significado: Esta propiedad tiene una interpretación de la teoría de la prueba: la inclusión de la teoría de la categoría sintáctica en la teoría del topos clasificador es conservadora. Esto vincula la noción semántica de completitud conceptual directamente con la conservatividad de la teoría de la prueba.

D. Relación con el Teorema de Makkai

En la Sección 5, los autores reconcilian su definición sintáctica con el teorema de reconstrucción semántica tradicional de Makkai para la lógica coherente.

• Marco: Utilizan la teoría de las ultracategorías virtuales (de [Saa25, Ham25, vGMT26]) para formalizar las prescripciones semánticas.
• Equivalencia: Demuestran que, para la lógica coherente, su noción de completitud conceptual es equivalente al resultado de Makkai (Corolario 5.3.3).
• Mecanismo: La equivalencia se mantiene bajo el supuesto de que los topoi clasificadores tienen suficientes puntos (completitud con respecto a modelos basados en conjuntos). Los autores descomponen el resultado en:
  1. Un componente sintáctico: La lógica es conceptualmente completa en su sentido (dualidad entre álgebras y topoi clasificadores).
  2. Un componente semántico: La equivalencia entre topoi clasificadores y ultracategorías de modelos basados en conjuntos (inducida por el supuesto de "suficientes puntos").
• Generalización: Definen la completitud conceptual "à la Makkai" para lógicas generales (Definición 5.4.1) y prueban que es equivalente a su noción sintáctica si la lógica tiene suficientes modelos basados en conjuntos (Teorema 5.4.2).

4. Significado y Reivindicaciones

El artículo afirma ofrecer una nueva luz de la teoría de la prueba sobre la completitud conceptual.

• Modularidad: Proporciona un marco unificado (vía inyectividad de Kan) para estudiar la completitud conceptual a través de diferentes lógicas subgeométricas, reduando la necesidad de técnicas ad hoc.
• Desprendimiento de la Semántica Basada en Conjuntos: La definición primaria de completitud conceptual se presenta como una propiedad de la lógica misma (una dualidad entre teorías y topoi clasificadores), independiente de los modelos basados en conjuntos. La conexión con el teorema de Makkai se muestra como una consecuencia de la completitud con respecto a modelos basados en conjuntos, no como la definición misma.
• Recuperación de Resultados Clásicos: El artículo recupera con éxito el teorema original de Makkai para la lógica coherente como un caso especial donde la dualidad sintáctica se alinea con la reconstrucción semántica vía ultracategorías.
• Conservatividad: Establece que la completitud conceptual implica una fuerte propiedad de conservatividad, vinculando propiedades de la teoría de modelos con propiedades de la teoría de la prueba.

Los autores mantienen la modestia sobre el alcance, señalando que, aunque han probado la completitud conceptual para varios fragmentos, la cuestión de si todas las partes de la lógica geométrica son conceptualmente completas sigue abierta, y la caracterización de la columna $\mathbf{WRInj}_{pw}(\mathcal{H})$ en su tabla de resumen queda para investigaciones futuras. También señalan que sus ejemplos actuales se sitúan "por debajo" del fragmento coherente, aunque conjeturan que la teoría se aplica más ampliamente.