¿Existe una base de datos para rastrear las dependencias de los teoremas matemáticos?

Question

Dada una prueba de un resultado, uno podría denotar la prueba como un nodo en un gráfico y, a continuación, dibuje flechas para el nodo a partir de los axiomas de los resultados anteriores y que la prueba de los usos, y, a continuación, dibuje flechas desde el nodo resultados que el resultado se utiliza para probar. Las fuentes de una gráfica sería axiomas matemáticos y los sumideros sería de resultados en los que aún no tienen consecuencias. Esto está relacionado con los hechos que finito de categorías puede ser dibujado como gráficos y que las pruebas forman una categoría.

Pregunta: ¿hay una existente ontológico/relacional de la base de datos en algún lugar que intenta hacer uso de tal idea formalmente codificar algunos de los presentes-día de la matemática?

A menudo puede ser difícil rastrear todas las dependencias lógicas de un determinado resultado. Por ejemplo, ¿cómo se puede mostrar si las pruebas del Teorema de la Función Implícita el uso de la Ley del Medio Excluido o no? En lugar de pasar un par de días va a través de decenas de libros de texto y tratar de analizar las pruebas, no por su contenido, sino sólo para ver qué supuestos están utilizando, ¿no sería más fácil preguntar una computadora para hacer la tarea?

Un sistema para el seguimiento de la lógica de las dependencias de los conocidos pruebas existentes teoremas podría ser útil no sólo para los principiantes ("Lo importante teoremas uso de la integridad de la propiedad de los números reales? Me voy a revisar la base de datos."), pero también podría ser útil para los constructivistas o intuitionists que quieren seguir la pista de que los resultados existentes de hacer uso del Axioma de Elección o de la Ley del Medio Excluido. Y tal vez sería posible utilizar una lo suficientemente completa base de datos para ejecutar las pruebas para ver si los fundamentos de las matemáticas son consistentes? Yo en realidad no sé, pero suena a un ingenuo nivel de algo que podría ser muy útil, incluso si tomaría mucho tiempo para construir.

Nota: no estoy seguro de lo que la etiqueta esta pregunta o si es que en tema.

Answer 1

El reverso de las matemáticas zoológico, fundada por Damir Dzhafarov y con el reciente desarrollo de Eric Astor, pretende ser una base de datos que muestra las relaciones y dependencias de teoremas matemáticos, como se describe en la teoría de la inversa de las matemáticas. Un enorme número de los teoremas clásicos de las matemáticas ahora se incluyen en el reverso de matemática de la jerarquía, y los que aparecen en esta base de datos.

El sistema acepta las nuevas contribuciones, y es capaz de generar diagramas que muestran las relaciones.

Por ejemplo, el actual results.txt el archivo y la base de datos está disponible en la rmzoo.zip archivo. Hay varios diagramas disponibles http://rmzoo.math.uconn.edu/diagrams/, que se generan automáticamente a partir de la base de datos.

Aquí en la foto es la Implicaciones y Estricto Implicaciones diagrama.

Answer 2

Es importante distinguir entre dos tipos de "dependencias".

El más limpio tipo de dependencia es la que se estudia en el reverso de las matemáticas: el Teorema de T depende del Axioma de Una si T es realmente improbable en la ausencia de A. la Gente que estudio inversa matemáticas hacen su trabajo de seguimiento de las dependencias de este tipo. Prueba de asistentes como el Coq también permiten realizar el seguimiento de algunas de estas dependencias; por ejemplo, el certificado de no tener la ley del medio excluido incorporado, así que usted puede confirmar de forma definitiva (en algunos casos) que algunos teorema de la no necesidad de la ley del medio excluido. Así que si este es el tipo de dependencia que usted está interesado, entonces hay personas que están trabajando duro en el seguimiento (pero una base de datos completa de la especie que usted está buscando no está disponible todavía).

Hay otro tipo de dependencia que es menos formal. Un ejemplo podría ser "La única prueba del Teorema se basa en la clasificación de los finitos simples grupos (CFSG)." Entendemos intuitivamente lo que esto significa, pero es difícil de formalizar. CFSG no es un axioma, y no conocemos ninguna forma plausible para formalizar "un sistema de matemáticas en la que CFSG es improbable pero muchas otras de las matemáticas es demostrable." Por lo tanto lo mejor que podemos hacer es proporcionar el equipo con todos los conocidos de las pruebas y, a continuación, se pudo verificar que cada prueba de T utiliza CFSG como un lexema. Esta es mucho más ambiciosa tarea de la formalización de al menos una prueba de cada teorema matemático, e incluso el último proyecto es de al menos décadas de distancia. Por ahora, los expertos humanos el conocimiento es una mejor guía para este tipo de cosas que las computadoras son.

Answer 3

Las Pilas de Proyecto proporciona un ejemplo de lo que usted está buscando. Cada definición, lema, teorema, etc. se da una etiqueta y las etiquetas se utilizan como referencias en las pruebas. Incluso proporcionan un API para la visualización de la etiqueta de la gráfica con d3.js. Por supuesto, el alcance del proyecto se limita a la geometría algebraica y temas relacionados, y no estoy seguro de si son o no perforar todo el camino hacia abajo a los axiomas de la teoría de conjuntos, pero es un buen inicio.

Answer 4

No es una respuesta, sólo un diagrama de las Pilas de Proyecto, mencionado por Paul Siegel, ilustrando las dependencias de "los resultados necesarios para probar la Comida del Lexema" (el Noetherian caso):

---

     

          ^{(Imagen de MathBabe blog.)}

---

Y aquí un enlace a una imagen más grande.

Answer 5

Mientras que las otras respuestas son muy buenas, hay un par de cuestiones que me gustaría traer a colación.

(1) ¿Cómo podemos evitar acabando con el sistema irrelevantes piezas de matemáticas?

(2) Que axiomática del sistema utilizamos? Si hacemos uso de ZFC, de hecho, hay un número infinito de axiomas. Por otra parte, probando algunos conocidos los resultados pueden ser bastante desordenado a la hora de ver las cosas usando el lenguaje de la teoría de conjuntos, o incluso en algunos nativos de la teoría. (Por ejemplo, ver cuánto tiempo tomó para formalizar la Feit-Thompson teorema de la Coq!)

Por otro lado, si usamos varios idiomas/axiomática de los sistemas, nos topamos con el hecho de que no se hunde. Para cualquier axioma en Un sistema, hay otro axioma B en otro sistema, el cual puede ser demostrado equivalente, utilizando los axiomas de un sistema de tercera! A continuación, obtener en el reverso de las matemáticas, que es bastante interesante, pero también (y con razón) limitada a algunos de los principales teoremas y sus equivalencias.