Teoría de la demostración

La teoría de la demostración es una rama importante ^{[ 1 ]} de la lógica matemática y la informática teórica, en la que las demostraciones se tratan como objetos matemáticos formales , lo que facilita su análisis mediante técnicas matemáticas. Las demostraciones se presentan típicamente como estructuras de datos definidas inductivamente , como listas , listas con recuadros o árboles , que se construyen según los axiomas y las reglas de inferencia de un sistema lógico dado. Por consiguiente, la teoría de la demostración es de naturaleza sintáctica , a diferencia de la teoría de modelos , que es de naturaleza semántica .

Algunas de las áreas principales de la teoría de la demostración incluyen la teoría estructural de la demostración , el análisis ordinal , la lógica de la demostrabilidad , la semántica de la teoría de la demostración , las matemáticas inversas , la minería de pruebas , la demostración automática de teoremas y la complejidad de las pruebas . 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 fue impulsada en gran medida por el trabajo de figuras como Gottlob Frege , Giuseppe Peano , Bertrand Russell y Richard Dedekind , la historia de la teoría de la demostración 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 pudiéramos dar demostraciones 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 muestra que todas sus afirmaciones puramente universales (más técnicamente sus demostrables)${\displaystyle \Pi _{1}^{0}}$Las oraciones ) son finitamente verdaderas; una vez así fundamentadas, no nos importa el significado no finito de sus teoremas existenciales, considerándolos como estipulaciones pseudosignificativas de la existencia de entidades ideales.

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

• El perfeccionamiento del resultado de Gödel, en particular el perfeccionamiento de J. Barkley Rosser , debilita el requisito anterior de consistencia ω a una consistencia simple;
• Axiomatización del núcleo del resultado de Gödel en términos de un lenguaje modal, la lógica de la demostrabilidad ;
• Iteración transfinita de teorías, debida a Alan Turing y Solomon Feferman ;
• El descubrimiento de teorías autoverificables , sistemas lo suficientemente fuertes como para hablar de sí mismos, pero demasiado débiles para llevar a cabo el argumento diagonal que es la clave del argumento de indemostrabilidad de Gödel.

Paralelamente al auge y la caída del programa de Hilbert, se sentaban las bases de la teoría de la demostración estructural . En 1926, Jan Łukasiewicz sugirió 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 supuestos en las reglas de inferencia de la lógica. En respuesta a esto, Stanisław Jaśkowski (1929) y Gerhard Gentzen (1934) proporcionaron independientemente tales sistemas, denominados cálculos de deducción natural . 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 demostrado ser muy importante en la teoría de la demostración. ^{[ 2 ]} Gentzen (1934) introdujo además la idea del cálculo de secuentes , 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 . En conjunto, la presentación de la deducción natural y el cálculo de secuentes introdujeron la idea fundamental de la prueba analítica en la teoría de la demostración.

La teoría de la demostración estructural es la subdisciplina de la teoría de la demostración que estudia las particularidades de los cálculos de demostración . Los tres estilos más conocidos de cálculos de demostración son:

• Los cálculos de Hilbert
• El cálculo de deducción natural
• Los cálculos secuenciales

Cada uno de estos cálculos puede proporcionar una formalización completa y axiomática de la lógica proposicional o de predicados, ya sea clásica o intuicionista , prácticamente cualquier lógica modal y muchas lógicas subestructurales , como la lógica de relevancia o la lógica lineal . De hecho, es raro encontrar una lógica que se resista a ser representada en uno de estos cálculos.

Los teóricos de la demostración suelen estar interesados ​​en cálculos de demostración que poseen ciertas propiedades deseables. Una familia de propiedades deseables es la analiticidad . La noción de demostración analítica fue introducida por Gentzen para el cálculo de secuentes, donde demostró que el cálculo de secuentes de las lógicas clásica e intuicionista carece de cortes .

Una noción de analiticidad es la propiedad de eliminación de cortes : un cálculo de demostración posee esta propiedad si incluye la regla de corte, pero cualquier secuente demostrable también lo es sin ella. El teorema del secuente medio de Gentzen , el teorema de interpolación de Craig y el teorema de Herbrand se derivan como corolarios de la propiedad de eliminación de cortes.

Otra noción de analiticidad es laPropiedad de subfórmula . Una demostración posee la propiedad de subfórmula si cada una de sus fórmulas es una subfórmula de su subsiguiente. Un cálculo de demostración posee la propiedad de subfórmula si todos sus subsecuentes demostrables pueden probarse mediante una demostración con la propiedad de subfórmula. En la mayoría de los cálculos de demostración, la propiedad de subfórmula se deriva de la propiedad de eliminación de cortes, aunque no necesariamentea la inversa. Un cálculo de demostración con la propiedad de subfórmula esconsistente, ya que si el subsiguiente vacío fuera derivable, tendría que ser una subfórmula de alguna premisa, lo cual no es el caso.

El cálculo de deducción natural de Gentzen también admite la noción de prueba analítica, como demostró 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 admiten la 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 una gran familia de procedimientos de búsqueda de pruebas orientados a objetivos. 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 como la admisibilidad de corte muestra que un sistema de pruebas es sintácticamente consistente. ^{[ 4 ]}

Existe una noción de armonía . En un sistema de deducción natural, cada conector lógico tiene un par de reglas: reglas de introducción y reglas de eliminación. Se dice que el par de reglas está en armonía si, en cualquier demostración, las fórmulas máximas pueden eliminarse normalizando la demostración. Una fórmula máxima es aquella que se introduce y luego se elimina. La idea es que dichas fórmulas máximas se comportan de forma similar a los lemas y, si bien pueden facilitar y abreviar la demostración, no son estrictamente necesarias. Una demostración normalizada solo debe introducir conectores lógicos y nunca eliminarlos.

Ciertas reglas de inferencia son locales , lo cual es una propiedad deseada. ^{[ 5 ]} Por ejemplo, considérese la  regla ! en lógica lineal :$${\displaystyle {\frac {\vdash A,?B_{1},\dots ,?B_{n}}{\vdash !A,?B_{1},\dots ,?B_{n}}}}$$Para comprobar que la  regla ! se ha aplicado correctamente a un determinado paso secuencial del cálculo${\displaystyle {\frac {\vdash A,B_{1},\dots ,B_{n}}{\vdash A',B_{1},\dots ,B_{n}}}}$, no solo es necesario comprobar que${\displaystyle A'=?A}$, pero también es necesario comprobar que cada uno de${\displaystyle B_{i}}$tiene  ! como su conector lógico más externo. En este sentido, la regla no es local , ya que para aplicarla hay que comprobar un número ilimitado de fórmulas.

La teoría de la demostración estructural se conecta con la teoría de tipos mediante la correspondencia de Curry-Howard , que observa una analogía estructural entre el proceso de normalización en el cálculo deductivo natural y la reducción beta en el cálculo lambda tipado . 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 triple, cuyo tercer componente son las categorías cartesianas cerradas .

Otros temas de investigación en teoría estructural incluyen el tableau 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 semidecisió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 finitistas son imposibles para 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 consistente axiomatizada recursivamente, se puede demostrar en aritmética finitista que la buena fundamentación de cierto ordinal transfinito implica la consistencia de T. El segundo teorema de incompletitud de Gödel implica que la buena fundamentación de dicho ordinal no puede demostrarse 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 originado por Gentzen, quien demostró la consistencia de la aritmética de Peano mediante inducción transfinita hasta el ordinal ε₀ _{. El análisis ordinal se ha extendido a numerosos 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 este sentido fue la demostración de Takeuti de la consistencia de Π₁₁ ^- _CA₀ mediante 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 objetivo es capturar 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 la demostrabilidad en la aritmética de Peano , se toman análogos modales de las condiciones de derivabilidad de Hilbert-Bernays y del 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 la incompletitud de la aritmética de Peano y teorías relacionadas tienen análogos en la lógica de la demostrabilidad. Por ejemplo, en la lógica de Gödel existe un teorema que establece 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 de Gödel 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 de Gödel. 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 la demostrabilidad se han centrado en la lógica de la demostrabilidad de primer orden, la lógica de la demostrabilidad polimodal (donde una modalidad representa la demostrabilidad en la teoría de objetos y otra en la metateoría), y las lógicas de la interpretabilidad, que buscan capturar la interacción entre demostrabilidad e interpretabilidad. Algunas investigaciones recientes han aplicado á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 demostrar teoremas matemáticos. ^{[ 6 ]} Este campo fue fundado por Harvey Friedman . Su método definitorio puede describirse como "ir hacia atrás desde los teoremas hasta 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 anticipado por resultados en teoría de conjuntos, como el teorema clásico que establece que el axioma de elección y el lema de Zorn son equivalentes en la teoría de conjuntos ZF . Sin embargo, el objetivo de la matemática inversa es estudiar posibles axiomas de teoremas matemáticos ordinarios, en lugar de posibles axiomas para la teoría de conjuntos.

En matemáticas inversas, se parte de un lenguaje marco y una teoría base —un sistema axiomático fundamental— que, si bien es demasiado débil para demostrar la mayoría de los teoremas de interés, es lo suficientemente potente como para desarrollar las definiciones necesarias para enunciar dichos 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 permita hablar de números reales y sucesiones de números reales.

Para cada teorema que puede enunciarse en el sistema base pero no es demostrable en él, el objetivo es determinar el sistema axiomático particular (más fuerte que el sistema base) que es necesario para demostrar dicho teorema. Para demostrar que se requiere un sistema S para demostrar un teorema T , se requieren dos demostraciones. La primera demuestra 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 demostración, conocida como inversión , demuestra que T implica S ; esta demostración 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 sin dejar de demostrar T. 

Un fenómeno notable en matemáticas inversas es la robustez de los cinco grandes sistemas axiomáticos. 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 se han analizado matemáticamente de forma inversa se han demostrado 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 ² ₂ (el 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.

Las interpretaciones funcionales consisten en la interpretación de teorías no constructivas en teorías funcionales. Suelen desarrollarse en dos etapas. Primero, se «reduce» una teoría clásica C a una intuicionista I. Es decir, se proporciona una correspondencia constructiva que traduce los teoremas de C a los de I. Segundo, se reduce la teoría intuicionista I a una teoría de funcionales F sin cuantificadores. Estas interpretaciones contribuyen a una forma del programa de Hilbert, ya que demuestran la consistencia de las teorías clásicas con respecto a las constructivas. Las interpretaciones funcionales exitosas han dado lugar a reducciones de teorías infinitas a teorías finitas y de teorías impredicativas a teorías predicativas.

Las interpretaciones funcionales también proporcionan una forma de extraer información constructiva de las demostraciones en la teoría reducida. Como consecuencia directa de la interpretación, se suele obtener 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 cual a veces es posible, esta caracterización suele ser exacta. A menudo, los términos de F coinciden con una clase natural de funciones, como las funciones recursivas primitivas o las funciones computables en tiempo polinomial. 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 la Dialectica . 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 demostraciones informales de la práctica matemática cotidiana difieren de las demostraciones formales de la teoría de la demostración. Se asemejan más a esbozos generales que, con tiempo y paciencia suficientes, permitirían a un experto reconstruir una demostración formal, al menos en principio. Para la mayoría de los matemáticos, escribir una demostración completamente formal resulta demasiado pedante y prolijo para su uso común.

Las demostraciones formales se construyen con la ayuda de ordenadores en la demostración interactiva de teoremas . Es importante destacar que estas demostraciones pueden verificarse automáticamente, también mediante ordenador. La verificación de las demostraciones formales suele ser sencilla, mientras que la búsqueda de demostraciones ( demostración automatizada de teoremas ) generalmente resulta difícil. En cambio, una demostración informal en la literatura matemática requiere semanas de revisión por pares para su verificación y aún puede contener errores.

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 .

• Lógica intermedia
• Teoría de modelos
• Prueba (verdad)
• Técnicas de demostración
• Cálculo de secuencias

• J. Avigad y EH Reck (2001). "'Aclarando la naturaleza del infinito': el desarrollo de la metamatemática y la teoría de la demostración ". Informe técnico Carnegie-Mellon CMU-PHIL-120.
• Barwise, Jon (1977). Manual de lógica matemática . Estudios en lógica y fundamentos de las matemáticas. Vol.  90. North-Holland Publishing Company. ISBN 072042285XLCCN 76026032 . OCLC 2347202 .​  ( Accesible para usuarios con discapacidades visuales )
• S. Buss, ed. (1998) Manual de teoría de la demostración . Elsevier.
• G. Gentzen (1935/1969). " Investigaciones sobre la deducción lógica ". En ME Szabo, ed. Documentos recopilados de Gerhard Gentzen . Holanda del Norte. Traducido por Szabo de "Untersuchungen über das logische Schliessen", Mathematisches Zeitschrift v. 39, págs.  176–210, 405  431.
• Girard, J.-Y.; Taylor, P.; Lafont, Y. (2003) [1989]. Pruebas y tipos (PDF) . Cambridge University Press. ISBN 0521371813.
• Prawitz, Dag (1965). Deducción natural: un estudio de teoría de la prueba . Acta Universitatis Stockholmiensis; Estudios de Filosofía de Estocolmo, 3 . Estocolmo, Gotemburgo, Uppsala: Almqvist & Wiksell . OCLC 912927896 . 
• Simpson, SG (2010). Subsistemas de la aritmética de segundo orden . Perspectivas en lógica (2.ª  ed.). Cambridge University Press. ISBN 9780521150149OCLC 528432422​​ 
• AS Troelstra y H. Schwichtenberg (1996). Teoría básica de la demostración , Cambridge Tracts in Theoretical Computer Science, Cambridge University Press, ISBN 0-521-77911-1.
• Wang, Hao (1981). Conferencias populares sobre lógica matemática . Van Nostrand Reinhold Company . ISBN 9780442231095OCLC 6087107​​ 

• "Teoría de la demostración" , Enciclopedia de Matemáticas , EMS Press , 2001 [1994]
• J. von Plato (2008). El desarrollo de la teoría de la demostración . Enciclopedia de filosofía de Stanford .