Teoría de la demostración estructural

En lógica matemática , la teoría de la demostración estructural es la subdisciplina de la teoría de la demostración que estudia los cálculos de demostración que sustentan una noción de demostración analítica , un tipo de demostración cuyas propiedades semánticas se exponen. Cuando todos los teoremas de una lógica formalizada en un cálculo de demostración tienen demostraciones analíticas, entonces el cálculo de demostración puede usarse para demostrar cosas como la consistencia , proporcionar procedimientos de decisión y permitir que se extraigan evidencias matemáticas o computacionales como contrapartes de los teoremas, el tipo de tarea que se suele asignar a la teoría de modelos . ^{[ 1 ]}

La noción de prueba analítica fue introducida en la teoría de la demostración por Gerhard Gentzen para el cálculo de secuentes ; las pruebas analíticas son aquellas que no tienen cortes . Su cálculo de deducción natural también admite una noción de prueba analítica, como demostró Dag Prawitz ; la definición es un poco más compleja : 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 .

El término estructura en la teoría de la prueba estructural proviene de una noción técnica introducida en el cálculo de secuencias: el cálculo de secuencias representa la afirmación hecha en cualquier etapa de una inferencia utilizando operadores especiales, extralógicos, llamados operadores estructurales: en${\displaystyle A_{1},\dots ,A_{m}\vdash B_{1},\dots ,B_{n}}$Las comas a la izquierda del torniquete son operadores que normalmente se interpretan como conjunciones, las de la derecha como disyunciones, mientras que el símbolo del torniquete en sí se interpreta como una implicación. Sin embargo, es importante señalar que existe una diferencia fundamental en el comportamiento entre estos operadores y los conectores lógicos que los interpretan en el cálculo de secuencias: los operadores estructurales se utilizan en todas las reglas del cálculo y no se consideran al determinar si se aplica la propiedad de la subfórmula. Además, las reglas lógicas solo funcionan en una dirección: la estructura lógica se introduce mediante reglas lógicas y no se puede eliminar una vez creada, mientras que los operadores estructurales se pueden introducir y eliminar durante una derivación.

La idea de considerar las características sintácticas de los secuentes como operadores especiales y no lógicos no es antigua, y fue impulsada por innovaciones en la teoría de la demostración: cuando los operadores estructurales son tan simples como en el cálculo de secuentes original de Getzen, hay poca necesidad de analizarlos, pero los cálculos de demostración de inferencia profunda , como la lógica de visualización (introducida por Nuel Belnap en 1982) ^{[ 2 ],} admiten operadores estructurales tan complejos como los conectores lógicos y exigen un tratamiento sofisticado.

El teorema de eliminación de cortes (Hauptsatz) es un resultado clave para el cálculo de secuentes. El teorema establece que cualquier secuente derivable mediante la regla de corte puede derivarse sin ella. La regla de corte, que generaliza el principio lógico del modus ponens , se formula como

${\displaystyle {\frac {\Gamma \vdash \Delta ,A\quad A,\Pi \vdash \Sigma }{\Gamma ,\Pi \vdash \Delta ,\Sigma }}\quad ({\text{Corte}}),}$

dónde,${\displaystyle \Gamma,\Delta,\Pi,}$y${\displaystyle \Sigma }$son secuencias de fórmulas. La fórmula de corte${\displaystyle A}$Se utiliza eficazmente como un lema intermedio que se introduce y luego se elimina. La importancia de eliminar esta regla radica en que las pruebas resultantes sin cortes poseen la propiedad de subfórmula, que garantiza que toda fórmula que aparezca en cualquier parte de una derivación sin cortes es una subfórmula de una fórmula en el secuente final y concluyente. Por lo tanto, la prueba es completamente analítica, ya que no requiere la introducción de ningún concepto externo, aparte de los ya presentes en el enunciado que se está demostrando. Esta propiedad de corte se utiliza para demostrar la consistencia de la lógica clásica e intuicionista y se emplea en la semántica de la teoría de la demostración .

La deducción natural es un sistema formal para derivar conclusiones lógicas a partir de premisas basado en un conjunto de reglas de inferencia que reflejan fielmente el razonamiento intuitivo humano. La conexión directa entre lógica y computación se establece a través de la correspondencia de Curry-Howard , que establece un isomorfismo directo entre fórmulas en lógica intuicionista y tipos en cálculo lambda tipado . En esta correspondencia, cada proposición puede verse como un tipo , y una prueba de esa proposición es análoga a un programa de ese tipo correspondiente. En esencia, una prueba es una construcción que demuestra la existencia de un tipo. Por ejemplo, una prueba de una implicación${\displaystyle A\to B}$corresponde a una función que toma un término de tipo${\displaystyle A}$como entrada y produce un término de tipo${\displaystyle B}$como resultado. De manera similar, una prueba de una conjunción${\displaystyle A\land B}$(un tipo de producto ) corresponde a un par que contiene un término de tipo${\displaystyle A}$y un término de tipo${\displaystyle B}$Esta relación no es meramente superficial. El proceso de normalización de pruebas, donde se eliminan pasos lógicos redundantes para simplificar una prueba, se corresponde directamente con el proceso de ejecución de programas, es decir, la beta-reducción, en el cálculo lambda tipado. Este isomorfismo vincula el contenido computacional de las pruebas lógicas con la teoría de tipos moderna y guía el diseño de asistentes de prueba. El siguiente diagrama ilustra esta correspondencia.

La dualidad lógica y la armonía están vinculadas a través de las simetrías del cálculo de secuencias . La arquitectura de una secuencia,${\displaystyle \Gamma \vdash \Delta }$, dónde${\displaystyle \Gamma,\Delta}$son multiconjuntos finitos de fórmulas, establece una dualidad fundamental entre antecedentes (izquierda) y concesiones (derecha). Esta dualidad se realiza explícitamente mediante las reglas de introducción izquierda y derecha para cada conector lógico. Por ejemplo, las reglas para la conjunción (${\displaystyle \land }$) y disyunción (${\displaystyle \lor }$) son duales:

${\displaystyle {\begin{array}{ccc}{\text{(}}{\land }{\text{L)}}&{\dfrac {A,B,\Gamma \vdash \Delta }{A\land B,\Gamma \vdash \Delta }}&{\text{(}}{\land }{\text{R)}}&{\dfrac {\Gamma \vdash \Delta ,A\qquad \Gamma \vdash \Delta ,B}{\Gamma \vdash \Delta ,A\land B}}\\\\{\text{(}}{\lor }{\text{L)}}&{\dfrac {A,\Gamma \vdash \Delta \qquad B,\Gamma \vdash \Delta }{A\lor B,\Gamma \vdash \Delta }}&{\text{(}}{\lor }{\text{R)}}&{\dfrac {\Gamma \vdash \Delta ,A,B}{\Gamma \vdash \Delta ,A\lor B}}\end{array}}}$

Esta simetría izquierda-derecha refleja una armonía más profunda entre el significado sintáctico de un conector, definido únicamente por sus reglas de introducción, a través del principio de inversión, y su comportamiento eliminativo. El teorema de corte-eliminación garantiza esta armonía metateórica. La regla de corte, ${\displaystyle {\text{(Corte)}}\quad {\dfrac {\Gamma \vdash \Delta ,A\qquad A,\Sigma \vdash \Lambda }{\Gamma ,\Sigma \vdash \Delta ,\Lambda }},}$ representa una forma de cohesión semántica; su admisibilidad demuestra que el sistema de prueba es internamente consistente y analítico, es decir, las pruebas no necesitan hacer referencia a conceptos extraños, por ejemplo, fórmulas.${\displaystyle A}$, que no están presentes en la conclusión. La reducción exitosa de un corte en una fórmula compleja a cortes en sus subfórmulas, a través de reducciones de casos clave entre reglas izquierda y derecha, por ejemplo, reduciendo un corte en${\displaystyle A\land B}$introducido por ambos (${\displaystyle \land }$R) y (${\displaystyle \land }$L), es la manifestación computacional del equilibrio perfecto entre el potencial de introducción y eliminación de un conector. Así, la eliminación por corte valida que las reglas operacionales estén en armonía, asegurando que el sistema lógico sea consistente y que sus pruebas posean buenas propiedades de normalización.

Ciertas reglas de inferencia son locales , lo cual es una propiedad deseada. ^{[ 3 ]} 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.

Como ejemplo más familiar, en el cálculo de secuencias clásico LK, las reglas de inferencia para OR son:$${\displaystyle {\frac {A,\Gamma \vdash \Delta \quad B,\Gamma \vdash \Delta }{A\lor B,\Gamma \vdash \Delta }}(\lor \vdash ),\quad {\frac {\Gamma \vdash A,\Delta }{\Gamma \vdash A\lor B,\Delta }}(\vdash \lor _{1}),\quad {\frac {\Gamma \vdash B,\Delta }{\Gamma \vdash A\lor B,\Delta }}(\vdash \lor _{2})}$$La regla${\displaystyle \lor \vdash }$no es local, ya que para comprobar que se ha aplicado correctamente en un paso$${\displaystyle {\frac {A,\Gamma \vdash \Delta \quad B,\Gamma '\vdash \Delta '}{C,\Gamma \vdash \Delta }}}$$uno debe comprobar no solo eso${\displaystyle C=A\lor B}$, pero también que${\displaystyle \Gamma =\Gamma ',\Delta =\Delta '}$Las reglas${\displaystyle \vdash \lor _{1},\vdash \lor _{2}}$son locales. ^{[ 4 ]}

La localidad fue motivada originalmente por consideraciones de programación lógica paralela . La idea es la siguiente: una secuencia larga${\displaystyle \Gamma \vdash \Delta }$podría almacenarse de forma distribuida, en varios procesadores y varias ubicaciones de memoria. Un paso de inferencia local puede realizarse con una cantidad limitada de interacción, mientras que los pasos de inferencia no locales pueden realizarse con una cantidad arbitrariamente grande de interacción. Por ejemplo, específicamente, para realizar${\displaystyle {\frac {\Gamma \vdash B,\Delta }{\Gamma \vdash A\lor B,\Delta }}}$, un procesador necesita producir una nueva secuencia${\displaystyle \Gamma '\vdash \Delta '}$, de tal manera que${\displaystyle \Gamma '}$simplemente apunta a la misma dirección de memoria que${\displaystyle \Gamma }$, y${\displaystyle \Delta '}$apunta a${\displaystyle A\lor B}$, seguido de la segunda dirección de memoria de${\displaystyle B,\Delta }$En cambio, aplicar una regla${\displaystyle \lor \vdash }$requiere comprobar que dos secuencias son idénticas, lo que lleva${\displaystyle O(n)}$operaciones, donde${\displaystyle n}$es el número de fórmulas en la secuencia.

El marco hipersecuente extiende la estructura secuente ordinaria a un multiconjunto de secuentes, utilizando un conector estructural adicional | (llamado barra hipersecuente ) para separar diferentes secuentes. Se ha utilizado para proporcionar cálculos analíticos para, por ejemplo, lógicas modales , intermedias y subestructurales ^{[ 5 ] [ 6 ] [ 7 ]} Un hipersecuente es una estructura

${\displaystyle \Gamma _{1}\vdash \Delta _{1}\mid \dots \mid \Gamma _{n}\vdash \Delta _{n}}$

donde cada${\displaystyle \Gamma _{i}\vdash \Delta _{i}}$es un secuente ordinario, llamado componente del hipersecuente. Al igual que los secuentes, los hipersecuentes pueden basarse en conjuntos, multiconjuntos o secuencias, y los componentes pueden ser secuentes de una sola conclusión o de múltiples conclusiones . La interpretación de la fórmula de los hipersecuentes depende de la lógica que se esté considerando, pero casi siempre es alguna forma de disyunción. Las interpretaciones más comunes son como una disyunción simple.

${\displaystyle (\bigwedge \Gamma _{1}\rightarrow \bigvee \Delta _{1})\lor \dots \lor (\bigwedge \Gamma _{n}\rightarrow \bigvee \Delta _{n})}$

para lógicas intermedias, o como una disyunción de cajas

${\displaystyle \Box (\bigwedge \Gamma _{1}\rightarrow \bigvee \Delta _{1})\lor \dots \lor \Box (\bigwedge \Gamma _{n}\rightarrow \bigvee \Delta _{n})}$

para lógicas modales.

De acuerdo con la interpretación disyuntiva de la barra hipersecuencial, prácticamente todos los cálculos hipersecuenciales incluyen las reglas estructurales externas , en particular la regla de debilitamiento externa.

${\displaystyle {\frac {\Gamma _{1}\vdash \Delta _{1}\mid \dots \mid \Gamma _{n}\vdash \Delta _{n}}{\Gamma _{1}\vdash \Delta _{1}\mid \dots \mid \Gamma _{n}\vdash \Delta _{n}\mid \Sigma \vdash \Pi }}}$

y la regla de contracción externa

${\displaystyle {\frac {\Gamma _{1}\vdash \Delta _{1}\mid \dots \mid \Gamma _{n}\vdash \Delta _{n}\mid \Gamma _{n}\vdash \Delta _{n}}{\Gamma _{1}\vdash \Delta _{1}\mid \dots \mid \Gamma _{n}\vdash \Delta _{n}}}}$

La expresividad adicional del marco hipersecuencial se proporciona mediante reglas que manipulan la estructura hipersecuencial. Un ejemplo importante lo proporciona la regla de división modalizada ^{[ 6 ].}

${\displaystyle {\frac {\Gamma _{1}\vdash \Delta _{1}\mid \dots \mid \Gamma _{n}\vdash \Delta _{n}\mid \Box \Sigma ,\Omega \vdash \Box \Pi ,\Theta }{\Gamma _{1}\vdash \Delta _{1}\mid \dots \mid \Gamma _{n}\vdash \Delta _{n}\mid \Box \Sigma \vdash \Box \Pi \mid \Omega \vdash \Theta }}}$

para la lógica modal S5 , donde${\displaystyle \Box \Sigma }$significa que cada fórmula en${\displaystyle \Box \Sigma }$es de la forma${\displaystyle \Box A}$.

Otro ejemplo lo proporciona la regla de comunicación para la lógica intermedia LC ^{[ 6 ].}

${\displaystyle {\frac {\Gamma _{1}\vdash \Delta _{1}\mid \dots \mid \Gamma _{n}\vdash \Delta _{n}\mid \Omega \vdash A\qquad \Sigma _{1}\vdash \Pi _{1}\mid \dots \mid \Sigma _{m}\vdash \Pi _{m}\mid \Theta \vdash B}{\Gamma _{1}\vdash \Delta _{1}\mid \dots \mid \Gamma _{n}\vdash \Delta _{n}\mid \Sigma _{1}\vdash \Pi _{1}\mid \dots \mid \Sigma _{m}\vdash \Pi _{m}\mid \Omega \vdash B\mid \Theta \vdash A}}}$

Nótese que en la regla de comunicación los componentes son secuencias de conclusión única.

El cálculo de secuencias anidadas es una formalización que se asemeja a un cálculo de estructuras de dos lados .

• Sara Negri y Jan Von Plato (2001). Teoría de la demostración estructural . Cambridge University Press. ISBN 978-0-521-79307-0.
• Anne Sjerp Troelstra ; Helmut Schwichtenberg (2000). Teoría básica de la prueba (2ª  ed.). Prensa de la Universidad de Cambridge. ISBN 978-0-521-77911-1.