Teoría de la prueba

La teoría de la prueba es una rama importante de la lógica matemática y la informática teórica que representa las pruebas como objetos matemáticos formales, lo que facilita su análisis mediante técnicas matemáticas. Las pruebas suelen presentarse 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 del sistema lógico. 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 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 demostrabilidad, las matemáticas inversas, la extracción de pruebas, la prueba 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.

Historia

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 se ve a menudo como establecida por David Hilbert, quien inició lo que se llama programa de Hilbert en las Fundaciones de Matemáticas. La idea central de este programa era que si pudiéramos dar pruebas finitarias de consistencia para todas las sofisticadas teorías formales necesarias por los matemáticos, entonces podríamos basar estas teorías mediante un argumento metamatemático, que muestra que todas sus afirmaciones puramente universales (más técnicamente sus provables ▪ ▪ 10{displaystyle Pi _{1} {0}} sentencias) son finitamente cierto; una vez tan fundados no nos importa el significado no-finitario de sus teoremas existenciales, con respecto a estos como pseudo-significantes estipulaciones de la existencia de entidades ideales.

El fracaso del programa fue inducido por los teoremas incompletos de Kurt Gödel, que demostraron que cualquier teoría consistente con ω que sea suficientemente fuerte para expresar ciertas verdades aritméticas simples, no puede demostrar su propia consistencia, que en la formulación de Gödel es una ▪ ▪ 10{displaystyle Pi _{1} {0}} sentencia. Sin embargo, surgieron versiones modificadas del programa de Hilbert y se han realizado investigaciones sobre temas relacionados. Esto ha llevado, en particular, a:

• Refinement of Gödel's result, particularly J. Barkley Rosser's refinement, weakening the above requirement of ω-consistency to simple consistency;
• Axiomatisation of the core of Gödel's result in terms of a modal language, provability logic;
• Iteración transfinita de teorías, debido a Alan Turing y Solomon Feferman;
• El descubrimiento de teorías autovergentes, sistemas lo suficientemente fuertes para hablar de sí mismos, pero demasiado débiles para llevar a cabo el argumento diagonal que es la clave del argumento de la imprevisibilidad de Gödel.

Paralelamente al auge y la caída del programa de Hilbert, se estaban asentando los cimientos 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 extraer conclusiones a partir de suposiciones 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 demostración. 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, y continuó haciendo 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.

Teoría de la prueba estructural

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:

• Hilbert Calculi
• El calculi de deducción natural
• El calculi secuente

Cada uno de estos puede brindar una formalización completa y axiomática de la lógica proposicional o de predicados del 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 los cálculos de prueba que respaldan una noción de prueba analítica. La noción de prueba analítica fue introducida por Gentzen para el cálculo secuente; allí las pruebas analíticas son las que están libres de corte. Gran parte del interés en las pruebas sin corte proviene de la propiedad de subfórmula: cada fórmula en el final de la secuencia de una prueba sin cortes es una subfórmula de una de las premisas. Esto permite mostrar fácilmente la consistencia del cálculo de secuencias; si el secuente vacío fuera derivable, tendría que ser una subfórmula de alguna premisa, que no lo es. El teorema de la secuencia media 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 corte.

El cálculo de deducción natural de Gentzen también respalda una 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. Los 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 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 de corte muestra que un sistema de prueba es sintácticamente consistente.

La teoría de prueba estructural está conectada con la teoría de tipos por medio de la correspondencia de 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 tipado. Esto proporciona la base para la teoría intuicionista de tipos 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 cartesianas cerradas.

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.

Análisis ordinal

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 las teorías de fuerza suficiente. El análisis ordinal permite medir con precisión el contenido infinito de la consistencia de las teorías. Para una teoría T recursivamente axiomatizada consistente, uno puede probar en aritmética finitista que la fundamentación de cierto ordinal transfinito implica la consistencia de T. El segundo teorema de incompletitud de Gödel implica que la fundamentación de tal ordinal no puede ser demostrado en la teoría T.

Las consecuencias del análisis ordinal incluyen (1) 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 probablemente totales y ordinales probablemente 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 ε₀. El análisis ordinal se ha extendido a muchos fragmentos de aritmética de primer y segundo orden y teoría de conjuntos. Un gran desafío 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 Π¹
₁-CA₀ usando el método de diagramas ordinales.

Lógica de probabilidad

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 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 relacionados con el carácter 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 (el segundo teorema de incompletitud de Gödel). También hay 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 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 (con una modalidad que representa la demostrabilidad en la teoría de objetos y otra que representa la demostrabilidad en la metateoría) y las lógicas de interpretabilidad destinadas 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ática inversa

Las matemáticas inversas son un programa de lógica matemática que busca determinar qué axiomas se requieren para probar teoremas de las matemáticas. El campo fue fundado por Harvey Friedman. Su método definitorio se puede describir como "ir hacia atrás de los teoremas a los axiomas", en contraste con la práctica matemática ordinaria de derivar teoremas de axiomas. El programa de matemáticas inversas fue presagiado por los 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. Sin embargo, el objetivo de las matemáticas inversas es estudiar los posibles axiomas de los teoremas ordinarios de las matemáticas en lugar de los posibles axiomas de la teoría de conjuntos.

En matemáticas inversas, uno comienza con 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 le pueden interesar, pero lo suficientemente poderoso como para desarrollar las definiciones necesarias para establecer estos 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 secuencias de números reales.

Para cada teorema que se puede establecer en el sistema base pero que no se puede probar en el sistema base, el objetivo es determinar el sistema de axiomas particular (más fuerte que el sistema base) que es necesario para probar ese teorema. Para mostrar 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; esta es una demostración matemática ordinaria junto con una justificación de que puede llevarse a cabo en el sistema S. La segunda prueba, conocida como reversión, muestra que T implica S; esta prueba se realiza en el sistema base. La inversión establece que ningún sistema de axiomas S′ que amplíe el sistema base puede ser más débil que S mientras sigue demostrando T.

Un fenómeno llamativo en las matemáticas inversas es la solidez de los sistemas de axiomas de los Big Five. En orden de fuerza creciente, estos sistemas se denominan con las siglas RCA₀, WKL₀, ACA₀, ATR₀, y Π¹
₁-CA₀. Casi todos los teoremas de las matemáticas ordinarias que han sido analizados matemáticamente a la inversa han demostrado ser 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 RT²
₂ (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 demostración.

Interpretaciones funcionales

Las interpretaciones funcionales son interpretaciones de teorías no constructivas en teorías funcionales. Las interpretaciones funcionales normalmente proceden en dos etapas. Primero, uno "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 de funcionales F libre de cuantificadores. 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 forma de extraer información constructiva de las pruebas en la teoría reducida. Como consecuencia directa de la interpretación se suele obtener el resultado de que cualquier función recursiva cuya totalidad pueda demostrarse en I o en C se representa mediante un término de F. Si se puede dar una interpretación adicional de F en I, que a veces es posible, esta caracterización, de hecho, suele mostrarse 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 la interpretación Dialéctica. Junto con la interpretación de 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.

Prueba formal e informal

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 prueba completamente formal es demasiado pedante y prolijo para ser de uso común.

Las demostraciones formales se construyen con la ayuda de computadoras en demostraciones interactivas de teoremas. Significativamente, estas pruebas se pueden verificar automáticamente, también por computadora. La comprobación de pruebas formales suele ser sencilla, mientras que encontrar pruebas (demostración automática de teoremas) suele ser difícil. Una prueba informal en la literatura matemática, por el contrario, requiere semanas de revisión por pares para ser revisada y aún puede contener errores.

Semántica de prueba teórica

En lingüística, la gramática tipológica, la gramática categorial y la gramática de Montague aplican formalismos basados en la teoría de la prueba estructural para dar una semántica formal del lenguaje natural.