Resumen Técnico: Semántica Doctrinal de la Lógica de Primer Orden Dirigida

1. Enunciado del Problema

El artículo aborda el desafío de formalizar la igualdad dirigida dentro de un marco lógico. Si bien la perspectiva categórica de Lawvere caracterizó con éxito la igualdad clásica como un adjunto izquierdo de la contracción, este enfoque depende de la simetría. En la teoría de tipos dirigida, donde los tipos se interpretan como categorías (o preórdenes) en lugar de grupoides (o conjuntos), la igualdad se convierte en una relación asimétrica (por ejemplo, una reescritura $a \to b$ o un orden $a \le b$).

La dificultad central radica en manejar la varianza (polaridad). En un entorno dirigido, una variable puede aparecer en una posición "negativa" (contravariante, por ejemplo, la fuente de un morfismo) o en una posición "positiva" (covariante, por ejemplo, el objetivo). Las reglas lógicas estándar para la igualdad (reflexividad y la regla J/eliminación) fallan en este contexto porque asumen implícitamente la simetría o permiten que las variables aparezcan en ambas polaridades simultáneamente de maneras que derivarían la simetría ($a \le b \vdash b \le a$), lo cual es inválido en la lógica dirigida. Los intentos anteriores de teoría de tipos dirigida a menudo luchan con estas restricciones de polaridad, particularmente en el contexto de la lógica irrelevante para pruebas (donde la igualdad es una proposición, no un tipo con múltiples habitantes).

2. Metodología

Los autores desarrollan una lógica de primer orden dirigida (dFOL) y su semántica doctrinal generalizando el marco de las hiperdoctrinas de Lawvere.

Sintaxis: Contextos Polarizados

La sintaxis introduce un contexto polarizado $[\Theta \mid \Delta \mid \Gamma]$, que particiona las variables en tres conjuntos basados en su varianza:

• $\Theta$ (Negativo): Variables que aparecen solo en posiciones contravariantes.
• $\Gamma$ (Positivo): Variables que aparecen solo en posiciones covariantes.
• $\Delta$ (Dinatural): Variables que aparecen en ambas posiciones (o que se permite tratarlas como tales).

Las características sintácticas clave incluyen:

• Igualdad Dirigida ($\le_A$): Una relación primitiva $s \le_A t$ donde $s$ está tipificada en el contexto negativo y $t$ en el contexto positivo.
• Implicación Polarizada: La implicación $\psi \Rightarrow \phi$ intercambia la polaridad del contexto para $\psi$ (moviéndolo de la izquierda a la derecha del turno), reflejando la contravarianza del primer argumento.
• Cuantificadores Polarizados: Los cuantificadores ($\forall^p, \exists^p$) están indexados por polaridad $p \in \{-, \Delta, +\}$ para rastrear la varianza de la variable ligada.
• Reglas de Sustitución: Un mecanismo de sustitución especializado (Definición 2.7) maneja la reindexación de términos a través de contextos polarizados, asegurando que las variables dinaturales se sustituyan consistentemente.

Semántica: Doctrinas Dirigidas

La semántica se captura mediante doctrinas dirigidas, una generalización de las doctrinas de Lawvere.

• Categoría Base: En lugar de una categoría estándar de tipos, la base es una categoría de polarización $ndp(\mathcal{C})$, cuyos objetos son ternas $(\Theta, \Delta, \Gamma)$ y cuyos morfismos respetan la estructura de varianza.
• Estructura Fibrada: Un funtor $P: ndp(\mathcal{C})^{op} \to \mathbf{Pos}$ mapea contextos polarizados a conjuntos parcialmente ordenados de fórmulas.
• Condiciones Clave:
  • Sin Varianza Dinatural (ndv): Una condición que asegura que las variables dinaturales en predicados surjan únicamente de colapsar variables positivas y negativas, previniendo "terceros" tipos de varianza.
  • Adjunciones Relativas: La igualdad dirigida se caracteriza no como un adjunto izquierdo estándar, sino como un adjunto izquierdo relativo a una operación similar a la contracción que colapsa dos variables de polaridad opuesta en una sola variable dinatural. Esto captura la restricción sintáctica que impide derivar la simetría.
  • Implicación Polarizada: Caracterizada como un coadjunto relativo.

3. Contribuciones Clave

1. Sintaxis de dFOL: Un sistema preciso de deducción natural para la lógica de primer orden con igualdad dirigida, que presenta un sistema riguroso de polaridades inspirado en la dinaturalidad. Este sistema prohíbe explícitamente la derivación de la simetría para la igualdad dirigida mientras mantiene los conectivos lógicos estándar.
2. Caracterización de la Igualdad Dirigida: El artículo generaliza la "igualdad como adjunto izquierdo" de Lawvere a la igualdad dirigida como adjunto izquierdo relativo. Esto proporciona una propiedad universal categórica precisa para la igualdad dirigida que da cuenta de la asimetría de la relación.
3. Doctrinas Dirigidas: La introducción de doctrinas dirigidas como un marco semántico. Los autores demuestran que la sintaxis de dFOL es sana y completa con respecto a esta semántica.
4. Completitud para Preórdenes: Se prueba un resultado de completitud específico para el fragmento clásico de dFOL con respecto al modelo estándar de preórdenes ($\mathbf{Preord}$). Esto establece que cualquier consecuencia válida en todos los modelos de preórdenes es derivable en la sintaxis.
5. Manejo de la Polaridad: El artículo demuestra cómo manejar la varianza en un entorno irrelevante para pruebas, distinguiéndolo de las teorías de tipos dirigidas relevantes para pruebas (como las de $\mathbf{Cat}$) mediante el uso de fibraciones posetales y fibras con valores en conjuntos parcialmente ordenados.

4. Resultados

• Sana y Completitud: Los autores establecen una bi-adjunción entre la categoría de teorías ($\mathbf{Theory}$) y la 2-categoría de doctrinas dirigidas ($\mathbf{DDoctrine}$). Esto implica que dFOL es el lenguaje interno de las doctrinas dirigidas.
• Completitud para Preórdenes: Utilizando una construcción al estilo de Henkin adaptada para contextos polarizados, el artículo demuestra que el fragmento clásico de dFOL es completo con respecto al modelo de preórdenes. La construcción define el dominio del modelo como el conjunto de términos cerrados ordenados por la derivabilidad de la igualdad dirigida ($\le_A$).
• Reglas Derivadas: El sistema soporta reglas derivadas para la transitividad, reflexividad y congruencia de la igualdad dirigida, así como reglas de interacción entre cuantificadores polarizados e implicación.
• Contraejemplos: El artículo ilustra que la simetría ($a \le b \vdash b \le a$) no es derivable, y el modelo de preórdenes sirve como contramodelo para tales derivaciones.

5. Significado y Afirmaciones

El artículo afirma avanzar en el trabajo de Lawvere sobre el papel de la varianza y los funtores hom en la lógica. Específicamente:

• Proporciona una caracterización sintáctica y semántica precisa de la igualdad dirigida en un entorno irrelevante para pruebas, llenando un vacío entre la lógica clásica y la teoría de tipos dirigida.
• Generaliza el concepto de igualdad como adjunto al caso dirigido mediante adjunciones relativas, ofreciendo una nueva herramienta categórica para comprender estructuras dirigidas.
• Demuestra que la lógica dirigida puede tratarse con técnicas lógicas estándar (como la completitud de Henkin) gestionando cuidadosamente las polaridades a través de contextos polarizados, en lugar de requerir maquinaria geométrica compleja o de categoría superior.
• El trabajo se posiciona como un paso fundamental para el razonamiento sobre sistemas de reescritura y fenómenos dirigidos (procesos, transiciones) dentro de un marco lógico, distinto de los enfoques relevantes para pruebas de la Teoría de Tipos Homotópica.

Los autores declaran explícitamente que su enfoque está en el caso irrelevante para pruebas, justificado por la naturaleza de la lógica de reescritura (donde una reescritura ocurre o no ocurre) y el uso de fibraciones posetales en la lógica categórica. No afirman resolver la complejidad completa de la teoría de tipos dirigida dependiente, sino proporcionar una base sólida para el caso de primer orden basado en preórdenes.