La teoría de la prueba 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 , facilitando su análisis mediante técnicas matemáticas. Las pruebas generalmente se presentan como estructuras de datos definidas inductivamente, como listas , listas en cuadros o árboles , que se construyen de acuerdo con los axiomas y reglas de inferencia de un sistema lógico determinado. En consecuencia, la teoría de la prueba es de naturaleza sintáctica , en contraste con la teoría de modelos , que es de naturaleza semántica .
Algunas de las áreas principales de la teoría de la prueba incluyen la teoría de la prueba estructural , el análisis ordinal , la lógica de demostrabilidad , las matemáticas inversas , la extracción de pruebas , la demostración automatizada de teoremas y la complejidad de la prueba . Gran parte de la investigación también se centra en aplicaciones en informática, lingüística y filosofía.
Aunque la formalización de la lógica avanzó mucho gracias al trabajo de figuras como Gottlob Frege , Giuseppe Peano , Bertrand Russell y Richard Dedekind , a menudo se considera que la historia de la teoría de la prueba moderna fue establecida por David Hilbert , quien inició lo que se llama la teoría de Hilbert. programa en Fundamentos de Matemáticas . La idea central de este programa era que si pudiéramos dar pruebas finitas de consistencia para todas las teorías formales sofisticadas que necesitan los matemáticos, entonces podríamos fundamentar estas teorías por medio de un argumento metamatemático, que demuestre que todas sus afirmaciones puramente universales (más técnicamente sus oraciones demostrables ) son finitamente verdaderas; una vez fundamentados así, no nos importa 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 demostraron que cualquier teoría ω-consistente que sea lo suficientemente fuerte como para expresar ciertas verdades aritméticas simples, no puede probar su propia consistencia, que según 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:
Paralelamente 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 permitiera sacar 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 , y el enfoque de Gentzen introdujo 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 resultado muy importante en la teoría de la prueba. [2] Gentzen (1934) introdujo además la idea del cálculo secuente , un cálculo avanzado con un espíritu similar que expresaba mejor la dualidad de los conectivos lógicos, [3] y realizó avances fundamentales en la formalización de la lógica intuicionista, y proporcionar 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 consiguiente 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 detalles de los cálculos de prueba . Los tres estilos más conocidos de cálculos de prueba son:
Cada uno de estos puede dar una formalización completa y axiomática de la lógica proposicional o de predicados, ya sea de estilo clásico o intuicionista , casi cualquier lógica modal y 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 . Gentzen introdujo la noción de prueba analítica para el cálculo siguiente; allí las pruebas analíticas son las que están libres de cortes . Gran parte del interés por las pruebas sin cortes proviene de laPropiedad de la subfórmula : cada fórmula al final de una prueba sin cortes es una subfórmula de una de las premisas. Esto permite mostrar fácilmente la coherencia del cálculo siguiente; si el secuente vacío fuera derivable, tendría que ser una subfórmula de alguna premisa, lo cual no es así. El teorema del secuente medio de Gentzen, el teorema de interpolación de Craig y el teorema de Herbrand también siguen como corolarios del teorema de eliminación de cortes.
El cálculo de deducción natural de Gentzen también apoya la noción de prueba analítica, como lo muestra Dag Prawitz . La definición es un poco 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 apoyan la noción de prueba analítica.
Una familia particular de pruebas analíticas que surgen en la lógica reductiva son las pruebas enfocadas que caracterizan una gran familia de procedimientos de búsqueda de pruebas dirigidos a objetivos. La capacidad de transformar un sistema de prueba en una forma enfocada es una buena indicación de su calidad sintáctica, de manera similar a cómo la admisibilidad del corte muestra que un sistema de prueba es sintácticamente consistente. [4]
La teoría de la prueba estructural está conectada con la teoría de tipos mediante 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, la tercera parte de la cual 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 prueba analítica de la teoría de prueba estructural para proporcionar procedimientos de decisión y procedimientos de semidecisión para una amplia gama de lógicas, y la teoría de prueba de lógica subestructural.
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 a menudo se interpreta como una demostración de que las pruebas de consistencia finitistas son imposibles para teorías de suficiente solidez. El análisis ordinal permite medir con precisión el contenido infinito de la consistencia de las teorías. Para una teoría T consistente recursivamente axiomatizada, se puede probar en aritmética finitista que el fundamento de un cierto ordinal transfinito implica la consistencia de T. El segundo teorema de incompletitud de Gödel implica que el fundamento de tal ordinal no se puede probar en la teoría T.
Las consecuencias del análisis ordinal incluyen (1) consistencia de subsistemas de aritmética clásica de segundo orden y teoría de conjuntos en relación con teorías constructivas, (2) resultados de independencia combinatoria y (3) clasificaciones de funciones recursivas demostrablemente totales y ordinales demostrablemente bien fundamentados.
El análisis ordinal fue originado por Gentzen, quien demostró la consistencia de la aritmética de Peano usando 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 de 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 cuadro se interpreta como "es demostrable que". El punto es captar la noción de 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 sobre lo incompleto de la aritmética de Peano y teorías relacionadas tienen análogos en la lógica de demostrabilidad. Por ejemplo, es un teorema en GL 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 lógica de demostrabilidad se han centrado en la lógica de demostrabilidad de primer orden, la lógica de demostrabilidad polimodal (donde una modalidad representa la demostrabilidad en la teoría de objetos y otra representa la demostrabilidad en la metateoría) y la lógica de interpretabilidad destinada a capturar la interacción entre demostrabilidad e interpretabilidad. . Algunas investigaciones muy recientes han involucrado aplicaciones de álgebras de demostrabilidad graduada al análisis ordinal de teorías aritméticas.
Matemáticas inversas es un programa de lógica matemática que busca determinar qué axiomas se requieren para demostrar teoremas de las matemáticas. [5] El campo fue fundado por Harvey Friedman . Su método de definición puede describirse como "regresar de 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áticas inversas fue presagiado por resultados en la 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 las matemáticas inversas, sin embargo, es estudiar posibles axiomas de teoremas ordinarios de las matemáticas en lugar de posibles axiomas de la teoría de conjuntos.
En matemáticas inversas, se comienza con un lenguaje marco y una teoría base (un sistema de axiomas centrales) que es demasiado débil para demostrar la mayoría de los teoremas que podrían interesarle, pero aún lo suficientemente poderoso como para desarrollar las definiciones necesarias para enunciar estos teoremas. Por ejemplo, para estudiar el teorema "Toda secuencia acotada de números reales tiene un supremo " es necesario utilizar un sistema base que pueda hablar de números reales y secuencias de números reales.
Para cada teorema que puede enunciarse en el sistema base pero que no es demostrable en el sistema base, el objetivo es determinar el sistema de axiomas 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 demostraciones. La primera prueba muestra que T es demostrable a partir de S ; ésta es una prueba matemática ordinaria junto con una justificación de que puede llevarse a cabo en el sistema S. La segunda prueba, conocida como inversión , muestra que T en sí implica S ; Esta prueba se realiza en el sistema base. La inversión establece que ningún sistema de axiomas 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 matemáticas inversas es la solidez de los sistemas de axiomas de los Cinco Grandes . En orden de fuerza creciente, estos sistemas se nombran con las iniciales RCA 0 , WKL 0 , ACA 0 , ATR 0 y Π.1
1-CA 0 . Se ha demostrado que casi todos los teoremas de las matemáticas ordinarias que han sido analizados matemáticamente a la inversa son equivalentes a uno de estos cinco sistemas. Gran parte de la investigación reciente se ha centrado en principios combinatorios que no encajan perfectamente en este marco, como 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 recursividad , 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 desarrollarse en dos etapas. Primero, se "reduce" una teoría clásica C a una intuicionista I. Es decir, se proporciona un mapeo constructivo que traduce los teoremas de C a los teoremas de I. Segundo, se reduce la teoría intuicionista I a una teoría libre de cuantificadores de funcionales F. Estas interpretaciones contribuyen a una forma del programa de Hilbert, ya que prueban la coherencia de las teorías clásicas en relación con las constructivas. Las interpretaciones funcionales exitosas han producido reducciones de teorías infinitas a teorías finitarias y de teorías impredicativas a predicativas.
Las interpretaciones funcionales también proporcionan una forma de extraer información constructiva de las pruebas de 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 demostrarse 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, que a veces es posible, de hecho se suele demostrar que esta caracterización es exacta. A menudo resulta que los términos de F coinciden con una clase natural de funciones, como las funciones primitivas recursivas o computables en tiempo polinomial. Las interpretaciones funcionales también se han utilizado para proporcionar análisis ordinales de teorías y clasificar sus funciones demostrablemente recursivas.
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 interpretación 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 aritmética intuicionista.
Las pruebas informales de la práctica matemática cotidiana son diferentes a las pruebas formales de la teoría de la prueba. Son más bien como bocetos de alto nivel que permitirían a un experto reconstruir una prueba formal, al menos en principio, con suficiente tiempo y paciencia. Para la mayoría de los matemáticos, escribir una demostración completamente 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 . Cabe destacar que estas pruebas pueden comprobarse automáticamente, también por ordenador. Verificar pruebas formales suele ser sencillo, mientras que encontrar pruebas ( demostración automatizada de teoremas ) suele ser difícil. Por el contrario, una prueba informal en la literatura matemática requiere semanas de revisión por pares y aún puede contener errores.
En lingüística , la gramática lógica de tipos, 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 .
