Pueden todos los resultados de matemáticas, que han sido debidamente probado hasta ahora, formalizarse y revisada por un equipo? Si es así, ¿qué tipo de lógica tendría que ser utilizado allí?
He oído que la lógica de primer orden no es expresiva suficiente: hay ciertos hechos que no pueden ser expresados en ella, y a veces las pruebas puede ser dado, pero ellos tienen asintóticamente tamaño grande (no la mera sintácticamente inconveniente).
En primer lugar, la buena noticia:
Hay una fuerte creencia entre los matemáticos, en particular entre los matemáticos, lógicos, que casi todos (correcta) de las pruebas en la literatura se podría formalizar hasta el punto de que un equipo completo podría verificar la prueba.
Hay muchos automatizado teorema de los verificadores ("a prueba de asistentes") que se han desarrollado para este propósito. Los desarrollos recientes incluyen una verificación completa de las pruebas del Teorema de los números Primos (dos independientes formalizaciones), el Jordán de la Curva de Teorema, y el Teorema de los Cuatro Colores. Sin duda, es posible completamente formalizar trivial de las matemáticas.
La mala noticia es que
El proceso de tomar una prueba en un diario y convertirlo en una prueba que puede ser verificada por el equipo es tedioso, ardua, y no trivial.
Aunque una prueba de programa asistente para la toma de pruebas en un formato de alto nivel como entrada, el formato es todavía mucho más detallada y prolija que un lenguaje natural, la prueba sería alguna vez. Por otra parte, la norma fundamental (como la de ZFC) son particularmente difíciles de trabajar con escribir formalizado pruebas.
Avigad (2007) informaron acerca de la prueba del Teorema de los números Primos, que fue escrito en el mucho más conveniente sistema de Isabelle, que:
"A las cinco de la línea de derivación de la Mobius inversión de la fórmula en la Sección 3.1 se traduce en alrededor de 40 líneas, y la prueba de la forma de la Selberg simetría fórmula discutido allí, llevado a cabo en alrededor de dos y medio de páginas en Shapiro del libro, toma cerca de 600 líneas, o de 13 páginas. Estas proporciones son más típicos."
También informó de
"Este proceso de estabilizado, sin embargo, y hacia el final [I] encontraron que la [I] podría formalizar acerca de una página de Shapiro del texto por día."
Así que, a pesar de que todos creen que es posible completamente de formalizar una prueba, el esfuerzo requerido con la tecnología actual hace que sea poco práctico. La mayoría de los top-tier matemáticos de investigación puede asimilar mucho más que una página de un libro de texto en un día completo de trabajo. Tal vez la tecnología va a mejorar.
También hay una cuestión de propósito. Algunos (tal vez influenciado por la tecnología) de la vista de equipo verificado pruebas a trabajar por un objetivo. Pero otros, incluyendo a Bourbaki, lo han visto como una distracción. Muchos de los de este último tipo de sensación de que el propósito de las pruebas es comunicar ideas con otros matemáticos. Mientras el equipo verificado las pruebas más certeza, la forma en que se escriben no es en absoluto adecuado para comunicar ideas a otros matemáticos. Después de todo, lo que los matemáticos están generalmente interesados en que no es sólo la "prueba", sino también la "idea" o "método" que subyace a la prueba, debido a que es lo que puede ser usado para demostrar otros teoremas.
I-Ciencias es una comunidad de estudiantes y amantes de la ciencia en la que puedes resolver tus problemas y dudas.
Puedes consultar las preguntas de otros usuarios, hacer tus propias preguntas o resolver las de los demás.
