Four Paradoxes and a Proof Assistant: Burali-Forti, Diaconescu, Reynolds, and Hurkens in the coq-paradoxes library

Resumen Técnico: Cuatro Paradojas y un Asistente de Pruebas

Enunciado del Problema
El artículo aborda los límites fundamentales del Cálculo de Construcciones Inductivas (CIC), la teoría de tipos que sustenta al asistente de pruebas Rocq (anteriormente Coq). Si bien la consistencia del CIC está bien establecida, las decisiones de diseño específicas que previenen la inconsistencia —particularmente en lo que respecta a la impredicatividad, las restricciones de universos y la eliminación grande— a menudo se tratan como restricciones abstractas de ingeniería. La biblioteca coq-paradoxes, distribuida con Rocq, contiene cuatro derivaciones mecanizadas de False (Burali-Forti, Diaconescu, Reynolds y Hurkens) que dependen de hipótesis rechazadas por el núcleo de Rocq. El problema central es interpretar estas derivaciones no meramente como curiosidades históricas o inconsistencias aisladas, sino como una "especificación negativa" que delimita con precisión dónde el núcleo debe trazar sus líneas para mantener la solidez.

Metodología
El artículo emplea una lectura detallada del código fuente dentro de la biblioteca coq-paradoxes, analizando específicamente cuatro archivos: BuraliForti.v, diaconescu.v, Reynolds.v y Hurkens_Set.v. La metodología incluye:

1. Descomposición de la Mecánica Compartida: Analizar Logics.v para comprender el predicado de accesibilidad (ACC) y la infraestructura de buena fundación utilizados por múltiples paradojas.
2. Rastreo de Derivaciones: Seguir los pasos lógicos en cada archivo para identificar la hipótesis específica (por ejemplo, un tipo universal de relaciones, un principio de elección o una inyección desde Prop hacia una única proposición) que conduce a una contradicción.
3. Mapeo a Rechazos del Núcleo: Correlacionar el punto de contradicción en la formalización con el mecanismo específico en el núcleo de Rocq (aritmética de universos, reglas de eliminación o verificaciones de impredicatividad) que impide que la construcción se compile.
4. Síntesis de Decisiones de Diseño: Agregar los hallazgos para extraer tres condiciones de frontera unificadas que gobiernan el comportamiento del núcleo.

Contribuciones y Resultados Clave

El artículo analiza cuatro paradojas específicas, demostrando cómo cada una expone una vulnerabilidad distinta en la teoría de tipos si ciertas decisiones de diseño fueran alteradas:

1. Paradoja de Burali-Forti (BuraliForti.v):

   • Mecanismo: Asume un tipo universal de relaciones $A_0$ y una inyección $i_0$ que mapea relaciones a elementos de $A_0$. Esto permite la construcción de un "ordinal de todos los ordinales" ($\Omega$) que se incrusta en sí mismo.
   • Rechazo del Núcleo: La paradoja depende de instanciar $A_0$ consigo mismo. El núcleo de Rocq impone una estricta estratificación de universos ($Type_j < Type_i$) para evitar que un tipo contenga su propia imagen. La construcción desencadena un error de "Inconsistencia de Universo" porque el nivel de universo requerido para el tipo interno debe ser al menos tan grande como el tipo externo, violando las restricciones acumulativas del núcleo.
   • Resultado: Establece la necesidad de restricciones de jerarquía de universos para evitar definiciones de tipos autorreferenciales que conduzcan a contradicciones de punto fijo.

2. Paradoja de Diaconescu (diaconescu.v):

   • Mecanismo: Utiliza una versión tipada del Axioma de Elección (Tchoice) sobre una relación de equivalencia sobre bool definida por una proposición $P$. La función de elección $f: bool \to bool$ se utiliza para decidir $P$ comparando $f(\text{true})$ y $f(\text{false})$.
   • Rechazo del Núcleo: El argumento extrae una decisión computacional (una función en Set) de una prueba existencial en Prop. Esto constituye una "eliminación grande" desde Prop hacia Set.
   • Resultado: Demuestra que permitir el Axioma de Elección en Set (o la eliminación grande desde Prop hacia Set) fuerza la Ley del Excluido Medio (LEM) dentro del sistema constructivo. El núcleo restringe la eliminación grande para evitar esta importación de lógica clásica a la capa computacional.

3. Paradoja de Reynolds (Reynolds.v):

   • Mecanismo: Reformula el resultado de Reynolds de que System F no tiene un modelo teórico de conjuntos. Asume una inyección $I: Prop \to Heyt$ (donde $Heyt$ es una única proposición) y construye un álgebra preinicial (codificación de Church) para un funtor $\Phi$. Utilizando el teorema de punto fijo de Lawvere, deriva un punto fijo para la negación, conduciendo a False.
   • Rechazo del Núcleo: La construcción depende de la impredicatividad de Prop (cuantificar sobre todas las proposiciones dentro de Prop). Sin embargo, la paradoja requiere una inyección desde Prop hacia una única proposición, lo cual el núcleo rechaza por motivos de universo antes de que se pueda alcanzar la contradicción lógica.
   • Resultado: Destaca el papel de la impredicatividad en Prop. Aunque Prop es impredicativo, el núcleo previene las inyecciones estructurales específicas que permitirían que el argumento diagonal de Cantor colapse el universo de proposiciones.

4. Paradoja de Hurkens (Hurkens_Set.v):

   • Mecanismo: Una adaptación de la simplificación de Hurkens de la paradoja de Girard. Asume un retrato entre Prop y bool (vía doble negación) y utiliza la impredicatividad de Set (si está habilitada) combinada con la eliminación grande para construir una relación bien fundada autorreferencial que conduce a False.
   • Rechazo del Núcleo: La paradoja requiere tanto impredicatividad en Set como eliminación grande (extraer booleanos del contenido proposicional). El núcleo predeterminado de Rocq mantiene Set predicativo y restringe la eliminación grande desde Prop.
   • Resultado: Muestra que la combinación de impredicatividad y eliminación grande en Set es inconsistente con la lógica clásica (LEM). La decisión del núcleo de mantener Set predicativo y restringir la eliminación es la salvaguarda.

Significado y Afirmaciones

El artículo argumenta que el paquete coq-paradoxes sirve como una especificación negativa del núcleo de Rocq. En lugar de simplemente listar inconsistencias, el paquete proporciona una prueba formal mediante ejemplos fallidos de la solidez del núcleo.

• Tres Condiciones de Frontera: El artículo sintetiza las cuatro paradojas en tres decisiones de diseño específicas impuestas por el núcleo:

  1. Jerarquía de Universos: Evita que los tipos se cuantifiquen sobre sí mismos de una manera que cree puntos fijos (Burali-Forti).
  2. Ubicación de la Impredicatividad: Confina la cuantificación impredicativa a Prop (y opcionalmente a Set con advertencias), previniendo las contradicciones de Reynolds y Hurkens.
  3. Disciplina de la Eliminación Grande: Restringe la extracción de contenido computacional (como bool o funciones en Set) de pruebas proposicionales, previniendo las contradicciones de Diaconescu y Hurkens.

• Rol Meta-matemático: El artículo afirma que el paquete es una pieza única de meta-matemática escrita dentro del sistema que documenta. No prueba teoremas para aplicación, sino que prueba la insatisfacibilidad de hipótesis específicas. Se demuestra que la "negativa" del núcleo es una consecuencia de políticas uniformes (aritmética de universos, reglas de eliminación) en lugar de soluciones ad hoc.

• Conclusión: El significado radica en demostrar que la negativa del núcleo de Rocq a compilar estas construcciones no es arbitraria, sino el mecanismo estructural preciso requerido para mantener la consistencia del CIC. El paquete valida que las decisiones de diseño del núcleo se toman por las "razones correctas", dibujando efectivamente el límite del sistema desde el exterior hacia el interior.