¿Hasta qué punto son ciertos los teoremas demostrados por Coq?

Question

En tono menos irónico, ¿se sabe cuál es la consistencia relativa de los teoremas demostrados con un demostrador automático de teoremas? Por supuesto, esto depende en cierta medida de las suposiciones que se hagan con respecto a la predicatividad y demás. Pero para concretar, tomemos uno de los paquetes populares con su instalación estándar.

Tal vez se trate de una lata de gusanos, o de un trozo de cuerda de longitud indeterminada, pero el reciente aumento del interés por la Fundamentos univalentes de Voevodsky plantea dudas sobre la solidez de la coherencia del sistema HoTT que él (y otros) proponen.

Answer 1

Para sistemas como Coq, que se basan en la teoría de tipos, esta pregunta es más difícil de responder de lo que cabría esperar.

En primer lugar, ¿qué hace falta para "conocer" la fuerza de consistencia de algún sistema? Clásicamente, los sistemas lógicos más estudiados se basan en la lógica de primer orden, utilizando el lenguaje de la aritmética elemental o el de la teoría de conjuntos. Así que si eres capaz de decir: "El sistema X es equiconsistente con ZF" (o con PA, o PRA, o ZFC + infinitos inaccesibles, etc.), entonces la mayoría de la gente sentirá que "conoce" la fuerza de consistencia de X, porque lo has calibrado contra una jerarquía familiar de sistemas.

Coq, sin embargo, se basa en algo llamado Cálculo de Construcciones Inductivas (CIC). Sin entrar en una explicación detallada de lo que es, permítanme mencionar que el núcleo de CIC no tiene ningún axioma, pero por lo general la gente añade axiomas según sea necesario. Por ejemplo, si quieres lógica clásica, puedes añadir la ley del medio excluido como axioma. Para obtener más potencia se pueden añadir más axiomas (aunque hay que tener cuidado porque se sabe que ciertas combinaciones de axiomas son inconsistentes). Pero intentar comparar los distintos sistemas que se pueden obtener de este modo con sistemas aritméticos o de teoría de conjuntos más familiares es una tarea complicada. Normalmente, no podemos esperar una calibración exacta, pero podemos interpretar varios fragmentos de la teoría de conjuntos en la teoría de tipos y viceversa, mostrando que la consistencia de la CIC más ciertos axiomas se intercala entre dos sistemas diferentes en el lado de la teoría de conjuntos. Si quieres profundizar en los detalles, te recomiendo el artículo Conjuntos en Coq, Coq en Conjuntos de Bruno Barras como punto de partida.

Answer 2

En folclore resultado es que existe un modelo "simple" de la teoría subyacente de Coq en $\mathrm{ZFC}+\omega$ -muchos inaccesibles.

Una buena introducción a este modelo es "El modelo no tan simple de prueba irrelevante de CC" por Miquel y Werner.

Benjamin Werner también esbozado una prueba de consistencia para el sistema más general con universos: Sobre la fuerza de las teorías de tipos irrelevantes para la prueba . Creo que la comunidad está suplicando una construcción formal y limpia de este modelo. Creo que esto es lo que está haciendo Bruno Barras (como menciona Tim Chow en su respuesta).

En límite inferior es aún más difícil de alcanzar. Sólo conozco 2 resultados para límites inferiores:

Werner construye de nuevo una interpretación de ZFC en CIC + algunos axiomas plausibles desde el punto de vista de la teoría de conjuntos. Conjuntos en tipos, tipos en conjuntos .

Miquel (de nuevo) construye una interpretación de Teoría de conjuntos de Zermelo en $\mathrm{F}_{\omega^2}$ el fragmento no dependiente de $\mathrm{CoC}$ con universos. El artículo es de lectura obligada: $\lambda Z$ : Teoría de conjuntos de Zermelo como PTS con 4 Sorts .

Si no me falla la memoria, en su doctorado muestra el resultado más general de que $\mathrm{CoC}$ con universos es equi-consistente con la teoría de Zermelo con $\omega$ -muchos universos (Zermelo). Lamentablemente, la tesis está en francés.

No estoy nada seguro de que $\mathrm{CIC}$ con universos es más poderoso que $\mathrm{CoC}$ con universos si no se añaden axiomas adicionales . Intuitivamente, esto se debe a que los tipos de datos inductivos pueden construirse en el "2º nivel" utilizando el truco de codificación habitual y, AFAIK, tienen la misma fuerza que los tipos de datos inductivos "incorporados" (pero son significativamente menos cómodos de utilizar).

Como puede ver, queda mucho por hacer para despejar estas incógnitas.

Answer 3

He aquí algunas publicaciones relacionadas con su pregunta:

• Robert Pollack. Cómo creer una prueba verificada por una máquina . En G. Sambin y J. Smith, editores, Twenty Five Years of Constructive Type Theory. Oxford Univ. Press, 1998. doi: 10.1093/oso/9780198501275.003.0013 (también disponible gratuitamente como BRICS Report Series, 4(18) (1997) doi: 10.7146/brics.v4i18.18945 ) ( Wayback Machine del archivo gzipped ps del autor )

En Inconsistencia de Pollack ( publicado en Electronic Notes in Theoretical Computer Science ), Freek Wiedijk demuestra que los asistentes de pruebas más populares son inconsistentes con Pollack.

En un puesto de internet Pollack habla de las coacciones de Coq:

El problema es que las coerciones de Coq se especifican de manera informal y se comportan un tanto impredecibles. Una teoría formal de las coerciones, como la de Luo Coercive subtyping (con teoría de la prueba y semántica) eliminaría esta cuestión del significado de las afirmaciones que utilizan coerciones. Sin embargo, la teoría de la prueba de las coerciones es complicada.

---

Añadido más tarde

La coherencia y la capacidad expresiva de Coq dependen del tiempo y de los errores corregidos frente a los introducidos.

Algunas versiones de Coq no consiguen demostrar teoremas demostrables, por ejemplo, comprobar ¿Cómo verifico la prueba de Coq de Feit-Thompson?

El error que obtienes es real, pero no está en la demostración del teorema del orden de impar. Está en Coq. Seré más claro: un error en el núcleo de Coq

Los fallos de inconsistencia parecen más comunes, Recopilación preliminar de errores críticos en las versiones estables de Coq . En Alrededor de 2008 informé de un error de incoherencia y para mi sorpresa Los desarrolladores de Coq llamaron al código de prueba de concepto exploit .

Answer 4

Algunos comprobadores de pruebas/probadores automáticos como Mizar utilizan teorías bastante fuertes: Teoría de Conjuntos (ZFC o algo así) junto con la suposición de que existe un cardinal inaccesible, si no recuerdo mal.

@Snark: Creo que al OP no le preocupa tanto la posibilidad de que el prover automático tenga bugs, sino que el sistema de axiomas subyacente sea realmente defectuoso, es decir, inconsistente.

Answer 5

Hay varias cosas que decir: en primer lugar, un demostrador automático de teoremas no sólo dice "Esto es cierto", sino que dice "Es cierto y aquí hay una prueba: ...".

El hecho de que exista una prueba ya es algo que da confianza al resultado, porque significa que se puede comprobar de forma independiente. Y con eso me refiero a que un comprobador automático de pruebas puede ir a la prueba y buscar errores. O los humanos pueden comprobar cada paso (aunque eso sería muy, muy aburrido comparado con las pruebas escritas por humanos).

Debo insistir en que si la comprobación la hace un programa, entonces debería hacerse sobre una base de código diferente a la del prover -- porque existe el riesgo de que si un bug hizo defectuosa la prueba, ese mismo bug hará defectuoso al comprobador de forma similar.

A partir de estas consideraciones, creo que las pruebas automáticas pueden ser tan convincentes como las humanas. No tan satisfactorias, pero sí convincentes.

Confío en los libros y los artículos que leo porque compruebo su coherencia básica, y sé que otros también lo hicieron. ¿Por qué no iba a fiarme de los resultados que se han comprobado de la misma manera?