La teoría de pruebas es una rama importante [1] de la lógica matemática y la informática teórica dentro de la cual las pruebas se tratan como objetos matemáticos formales , lo que facilita su análisis mediante técnicas matemáticas. Las pruebas se presentan típicamente como estructuras de datos definidas inductivamente, como listas , listas en cajas o árboles , que se construyen de acuerdo con los axiomas y las reglas de inferencia de un sistema lógico dado. En consecuencia, la teoría de pruebas es de naturaleza sintáctica , en contraste con la teoría de modelos , que es de naturaleza semántica .
Algunas de las principales áreas de la teoría de la prueba incluyen la teoría de la prueba estructural , el análisis ordinal , la lógica de la demostrabilidad , las matemáticas inversas , la minería de pruebas , la demostración automatizada de teoremas y la complejidad de las pruebas . Gran parte de la investigación también se centra en las aplicaciones en la informática, la lingüística y la filosofía.
Aunque la formalización de la lógica fue muy avanzada por el trabajo de figuras como Gottlob Frege , Giuseppe Peano , Bertrand Russell y Richard Dedekind , la historia de la teoría de la prueba moderna a menudo se considera establecida por David Hilbert , quien inició lo que se llama el programa de Hilbert en los Fundamentos de las matemáticas . La idea central de este programa era que si podíamos dar pruebas finitas de consistencia para todas las teorías formales sofisticadas que necesitaban los matemáticos, entonces podríamos fundamentar estas teorías por medio de un argumento metamatemático, que muestra que todas sus afirmaciones puramente universales (más técnicamente, sus oraciones demostrables ) son finitamente verdaderas; una vez fundamentadas de esa manera, no nos preocupamos por el significado no finito de sus teoremas existenciales, considerándolos como estipulaciones pseudo-significativas de la existencia de entidades ideales.
El fracaso del programa fue inducido por los teoremas de incompletitud de Kurt Gödel , que mostraban que cualquier teoría ω-consistente que sea lo suficientemente fuerte como para expresar ciertas verdades aritméticas simples, no puede demostrar su propia consistencia, que en la formulación de Gödel es una oración. Sin embargo, surgieron versiones modificadas del programa de Hilbert y se han llevado a cabo investigaciones sobre temas relacionados. Esto ha llevado, en particular, a:
En paralelo al ascenso y caída del programa de Hilbert, se estaban sentando las bases de la teoría de la prueba estructural . Jan Łukasiewicz sugirió en 1926 que se podrían mejorar los sistemas de Hilbert como base para la presentación axiomática de la lógica si se permitía extraer conclusiones a partir de supuestos en las reglas de inferencia de la lógica. En respuesta a esto, Stanisław Jaśkowski (1929) y Gerhard Gentzen (1934) proporcionaron de forma independiente tales sistemas, llamados cálculos de deducción natural , con el enfoque de Gentzen introduciendo la idea de simetría entre los fundamentos para afirmar proposiciones, expresados en reglas de introducción , y las consecuencias de aceptar proposiciones en las reglas de eliminación , una idea que ha demostrado ser muy importante en la teoría de la prueba. [2] Gentzen (1934) introdujo además la idea del cálculo secuencial , un cálculo desarrollado con un espíritu similar que expresaba mejor la dualidad de los conectivos lógicos, [3] y continuó realizando avances fundamentales en la formalización de la lógica intuicionista y proporcionó la primera prueba combinatoria de la consistencia de la aritmética de Peano . Juntos, la presentación de la deducción natural y el cálculo secuencial introdujeron la idea fundamental de la teoría analítica de prueba a prueba.
La teoría de la prueba estructural es la subdisciplina de la teoría de la prueba que estudia los aspectos específicos de los cálculos de prueba . Los tres estilos más conocidos de cálculos de prueba son:
Cada uno de ellos puede dar una formalización completa y axiomática de la lógica proposicional o de predicados , ya sea de tipo clásico o intuicionista , de casi cualquier lógica modal y de muchas lógicas subestructurales , como la lógica de relevancia o la lógica lineal . De hecho, es inusual encontrar una lógica que se resista a ser representada en uno de estos cálculos.
Los teóricos de la prueba suelen estar interesados en cálculos de prueba que respalden una noción de prueba analítica . La noción de prueba analítica fue introducida por Gentzen para el cálculo secuencial; allí, las pruebas analíticas son aquellas que no requieren cortes . Gran parte del interés en las pruebas sin cortes proviene de laPropiedad de la subfórmula : cada fórmula en el consecuente final de una prueba sin cortes es una subfórmula de una de las premisas. Esto permite demostrar fácilmente la consistencia del cálculo consecuente; si el consecuente vacío fuera derivable, tendría que ser una subfórmula de alguna premisa, lo cual no es así. El teorema de la consecuente intermedia de Gentzen, el teorema de interpolación de Craig y el teorema de Herbrand también se derivan como corolarios del teorema de eliminación de cortes.
El cálculo de deducción natural de Gentzen también respalda una noción de prueba analítica, como lo demuestra Dag Prawitz . La definición es ligeramente más compleja: decimos que las pruebas analíticas son las formas normales , que están relacionadas con la noción de forma normal en la reescritura de términos. Cálculos de prueba más exóticos, como las redes de prueba de Jean-Yves Girard, también respaldan una noción de prueba analítica.
Una familia particular de pruebas analíticas que surgen en la lógica reductiva son las pruebas focalizadas , que caracterizan a una gran familia de procedimientos de búsqueda de pruebas orientados a un objetivo. La capacidad de transformar un sistema de pruebas en una forma focalizada es un buen indicador de su calidad sintáctica, de manera similar a cómo la admisibilidad de corte muestra que un sistema de pruebas es sintácticamente consistente. [4]
La teoría de la prueba estructural está conectada con la teoría de tipos por medio de la correspondencia Curry-Howard , que observa una analogía estructural entre el proceso de normalización en el cálculo de deducción natural y la reducción beta en el cálculo lambda tipificado . Esto proporciona la base para la teoría de tipos intuicionista desarrollada por Per Martin-Löf , y a menudo se extiende a una correspondencia de tres vías, cuyo tercer tramo son las categorías cerradas cartesianas .
Otros temas de investigación en teoría estructural incluyen el cuadro analítico, que aplica la idea central de la prueba analítica de la teoría de la prueba estructural para proporcionar procedimientos de decisión y procedimientos de semi-decisión para una amplia gama de lógicas, y la teoría de la prueba de lógicas subestructurales.
El análisis ordinal es una técnica poderosa para proporcionar pruebas de consistencia combinatoria para subsistemas de aritmética, análisis y teoría de conjuntos. El segundo teorema de incompletitud de Gödel se interpreta a menudo como una demostración de que las pruebas de consistencia finitista son imposibles para teorías con suficiente solidez. El análisis ordinal permite medir con precisión el contenido infinitario de la consistencia de las teorías. Para una teoría recursivamente axiomatizada T consistente, se puede probar en aritmética finitista que la fundamentación de un cierto ordinal transfinito implica la consistencia de T. El segundo teorema de incompletitud de Gödel implica que la fundamentación de dicho ordinal no se puede probar en la teoría T.
Las consecuencias del análisis ordinal incluyen (1) la consistencia de los subsistemas de la aritmética clásica de segundo orden y la teoría de conjuntos en relación con las teorías constructivas, (2) resultados de independencia combinatoria y (3) clasificaciones de funciones recursivas demostrablemente totales y ordinales demostrablemente bien fundados.
El análisis ordinal fue creado por Gentzen, quien demostró la consistencia de la aritmética de Peano mediante inducción transfinita hasta el ordinal ε 0 . El análisis ordinal se ha extendido a muchos fragmentos de la aritmética de primer y segundo orden y la teoría de conjuntos. Un desafío importante ha sido el análisis ordinal de las teorías impredicativas. El primer avance en esta dirección fue la prueba de Takeuti de la consistencia de Π1
1-CA 0 utilizando el método de diagramas ordinales.
La lógica de demostrabilidad es una lógica modal , en la que el operador de caja se interpreta como 'es demostrable que'. El punto es capturar la noción de un predicado de prueba de una teoría formal razonablemente rica . Como axiomas básicos de la lógica de demostrabilidad GL ( Gödel - Löb ), que captura lo demostrable en la aritmética de Peano , se toman análogos modales de las condiciones de derivabilidad de Hilbert-Bernays y el teorema de Löb (si es demostrable que la demostrabilidad de A implica A, entonces A es demostrable).
Algunos de los resultados básicos relativos a la incompletitud de la aritmética de Peano y teorías relacionadas tienen análogos en la lógica de la demostrabilidad. Por ejemplo, un teorema de la GL sostiene que si una contradicción no es demostrable, entonces no es demostrable que una contradicción no sea demostrable (segundo teorema de incompletitud de Gödel). También existen análogos modales del teorema del punto fijo. Robert Solovay demostró que la lógica modal GL es completa con respecto a la aritmética de Peano. Es decir, la teoría proposicional de la demostrabilidad en la aritmética de Peano está completamente representada por la lógica modal GL. Esto implica directamente que el razonamiento proposicional sobre la demostrabilidad en la aritmética de Peano es completo y decidible.
Otras investigaciones en el campo de la lógica de la demostrabilidad se han centrado en la lógica de la demostrabilidad de primer orden, la lógica de la demostrabilidad polimodal (en la que una modalidad representa la demostrabilidad en la teoría de objetos y otra la representa en la metateoría) y las lógicas de interpretabilidad destinadas a captar la interacción entre la demostrabilidad y la interpretabilidad. Algunas investigaciones muy recientes han involucrado aplicaciones de álgebras de demostrabilidad graduadas al análisis ordinal de teorías aritméticas.
La matemática inversa es un programa de lógica matemática que busca determinar qué axiomas se requieren para probar teoremas de matemáticas. [5] El campo fue fundado por Harvey Friedman . Su método definitorio puede describirse como "ir hacia atrás desde los teoremas a los axiomas ", en contraste con la práctica matemática ordinaria de derivar teoremas a partir de axiomas. El programa de matemática inversa fue prefigurado por resultados en teoría de conjuntos como el teorema clásico de que el axioma de elección y el lema de Zorn son equivalentes sobre la teoría de conjuntos ZF . El objetivo de la matemática inversa, sin embargo, es estudiar los posibles axiomas de los teoremas ordinarios de las matemáticas en lugar de los posibles axiomas para la teoría de conjuntos.
En las matemáticas inversas, se parte de un lenguaje marco y una teoría base (un sistema de axiomas central) que es demasiado débil para demostrar la mayoría de los teoremas que nos pueden interesar, pero lo suficientemente potente como para desarrollar las definiciones necesarias para enunciar esos teoremas. Por ejemplo, para estudiar el teorema "Toda sucesión acotada de números reales tiene un supremo ", es necesario utilizar un sistema base que pueda hablar de números reales y sucesiones de números reales.
Para cada teorema que se puede enunciar en el sistema base pero no es demostrable en el sistema base, el objetivo es determinar el sistema axiomático particular (más fuerte que el sistema base) que es necesario para demostrar ese teorema. Para demostrar que se requiere un sistema S para demostrar un teorema T , se requieren dos pruebas. La primera prueba muestra que T es demostrable a partir de S ; esta es una prueba matemática ordinaria junto con una justificación de que se puede llevar a cabo en el sistema S . La segunda prueba, conocida como inversión , muestra que T en sí implica S ; esta prueba se lleva a cabo en el sistema base. La inversión establece que ningún sistema axiomático S′ que extienda el sistema base puede ser más débil que S y al mismo tiempo demostrar T .
Un fenómeno sorprendente en las matemáticas inversas es la robustez de los sistemas de axiomas de los Cinco Grandes . En orden de fortaleza creciente, estos sistemas se nombran con las siglas RCA 0 , WKL 0 , ACA 0 , ATR 0 y Π1
1-CA 0 . Casi todos los teoremas de las matemáticas ordinarias que se han analizado matemáticamente de forma inversa han demostrado ser equivalentes a uno de estos cinco sistemas. Muchas investigaciones recientes se han centrado en principios combinatorios que no encajan perfectamente en este marco, como el RT2
2(Teorema de Ramsey para pares).
La investigación en matemáticas inversas a menudo incorpora métodos y técnicas de la teoría de la recursión , así como de la teoría de la prueba.
Las interpretaciones funcionales son interpretaciones de teorías no constructivas en teorías funcionales. Las interpretaciones funcionales suelen proceder en dos etapas. En primer lugar, se "reduce" una teoría clásica C a una intuicionista I. Es decir, se proporciona una aplicación constructiva que traduce los teoremas de C a los teoremas de I. En segundo lugar, se reduce la teoría intuicionista I a una teoría de funcionales libre de cuantificadores F. Estas interpretaciones contribuyen a una forma del programa de Hilbert, ya que prueban la consistencia de las teorías clásicas en relación con las constructivas. Las interpretaciones funcionales exitosas han producido reducciones de teorías infinitarias a teorías finitarias y de teorías impredicativas a predicativas.
Las interpretaciones funcionales también proporcionan una manera de extraer información constructiva de las pruebas en la teoría reducida. Como consecuencia directa de la interpretación, normalmente se obtiene el resultado de que cualquier función recursiva cuya totalidad pueda probarse en I o en C está representada por un término de F. Si se puede proporcionar una interpretación adicional de F en I, lo que a veces es posible, esta caracterización suele demostrarse exacta. A menudo resulta que los términos de F coinciden con una clase natural de funciones, como las funciones recursivas primitivas o las funciones computables en tiempo polinómico. Las interpretaciones funcionales también se han utilizado para proporcionar análisis ordinales de teorías y clasificar sus funciones recursivas demostrables.
El estudio de las interpretaciones funcionales comenzó con la interpretación de Kurt Gödel de la aritmética intuicionista en una teoría de funcionales de tipo finito sin cuantificadores. Esta interpretación se conoce comúnmente como la interpretación de Dialéctica . Junto con la interpretación de la doble negación de la lógica clásica en la lógica intuicionista, proporciona una reducción de la aritmética clásica a la aritmética intuicionista.
Las pruebas informales de la práctica matemática cotidiana no se parecen a las pruebas formales de la teoría de la demostración. Son más bien como bocetos de alto nivel que permitirían a un experto reconstruir una prueba formal al menos en principio, si se le da suficiente tiempo y paciencia. Para la mayoría de los matemáticos, escribir una prueba totalmente formal es demasiado pedante y prolijo para ser de uso común.
Las demostraciones formales se construyen con la ayuda de computadoras en la demostración interactiva de teoremas . Es significativo que estas demostraciones se puedan verificar automáticamente, también por computadora. La verificación de demostraciones formales suele ser simple, mientras que la búsqueda de demostraciones ( demostración automática de teoremas ) es generalmente difícil. En cambio, una demostración informal en la literatura matemática requiere semanas de revisión por pares para ser revisada y aún puede contener errores.
En lingüística , la gramática tipológica, la gramática categorial y la gramática Montague aplican formalismos basados en la teoría de la prueba estructural para dar una semántica formal del lenguaje natural .
