Teoría de la demostración

La teoría de la demostración o teoría de la prueba es una rama de la lógica matemática que trata a las demostraciones como objetos matemáticos, facilitando su análisis mediante técnicas matemáticas. Las demostraciones suelen presentarse como estructuras de datos inductivamente definidas que se construyen de acuerdo con los axiomas y reglas de inferencia de los sistemas lógicos. En este sentido, la teoría de la demostración se ocupa de la sintaxis, en contraste con la teoría de modelos, que trata con la semántica. Junto con la teoría de modelos, la teoría de conjuntos axiomática y la teoría de la recursión, la teoría de la demostración es uno de los "cuatro pilares" de los fundamentos de las matemáticas[ cita requerida].

Demostraciones formales e informales

Dentro de la teoría de la demostración es muy importante distinguir entre las demostraciones «informales» encontradas en la práctica cotidiana de los matemáticos y en los libros comunes sobre matemáticas, de las demostraciones puramente «formales» de la teoría de la demostración formal. Las primeras tienen el objetivo de mostrar rigurosamente un resultado matemático de manera clara, pero al mismo tiempo intuitiva e inteligible, las segundas de estas demostraciones son como una especie de esquemas de alto-nivel escritos en lenguaje formal, que en principio, pueden permitir a un experto o un lógico construir una demostración puramente formal del mismo resultado, dado el suficiente tiempo y paciencia. Para la mayoría de matemáticos, escribir una demostración completamente formal es demasiado pedante y un gasto de tiempo innecesario como para ser práctica común.

Las demostraciones formales pueden ser construidas con ayuda de ordenadores mediante métodos de demostración de teoremas interactivos u otras técnicas. Es significativo, que estas demostraciones puramente formales basadas en la manipulación de signos puden ser verificadas automáticamente, también por ordenador. Verificar una demostración puramente formal es simple, mientras que encontrar demostraciones es generalmente mucho más difícil. Una demostración informal en en artículo matemático, por el contrario, requiere semanas de revisión por pares para ser verificada, y frecuentemente puede contener errores que pasen inadvertidos incluso para matemáticos profesionales en temas de investigación suficientemente complejos.

La teoría de la demostración formal se ocupa de las propiedades de los sistemas deductivos, su complejidad, el poder expresivo de dichos sistemas y está íntimamente conectada a la lógica matemática, la teoría de modelos y la fundamentación de las matemáticas. Por el contrario el desarrollo de demostraciones informales es un terreno altamente creativo y si bien existen familias enteras de esquemas de demostración en diferentes áreas, son un ejercicio básicamente humano en el que no existen algoritmos generales para construir demostraciones.

Other Languages