Teoría de la prueba estructural

En lógica matemática , la teoría de la prueba estructural es la subdisciplina de la teoría de la prueba que estudia los cálculos de prueba que apoyan una noción de prueba analítica , un tipo de prueba cuyas propiedades semánticas quedan expuestas. Cuando todos los teoremas de una lógica formalizados en una teoría de la prueba estructural tienen pruebas analíticas, entonces la teoría de la prueba puede usarse para demostrar cosas como la consistencia , proporcionar procedimientos de decisión y permitir que se extraigan testigos matemáticos o computacionales como contrapartes de los teoremas, los tipo de tarea que se asigna más a menudo a la teoría de modelos .

prueba analítica

La noción de prueba analítica fue introducida en la teoría de la prueba por Gerhard Gentzen para el cálculo siguiente ; las pruebas analíticas son aquellas que están libres de cortes . Su cálculo de deducción natural también apoya una noción de prueba analítica, como lo 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 .

Estructuras y conectivos

El término estructura en la teoría de la prueba estructural proviene de una noción técnica introducida en el cálculo secuente: el cálculo secuente representa el juicio realizado en cualquier etapa de una inferencia utilizando operadores extralógicos especiales llamados operadores estructurales: en , las comas a la izquierda de los del torniquete son operadores normalmente interpretados como conjunciones, los 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 conectivos lógicos mediante los cuales se interpretan en el cálculo secuencial: los operadores estructurales se utilizan en todas las reglas del cálculo y no se consideran al preguntar si se aplica la propiedad de la subfórmula. Además, las reglas lógicas funcionan en un solo sentido: la estructura lógica se introduce mediante reglas lógicas y no puede eliminarse una vez creada, mientras que los operadores estructurales pueden introducirse y eliminarse en el curso de una derivación. ${\displaystyle A_{1},\dots ,A_{m}\vdash B_{1},\dots ,B_{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 forzada por innovaciones en la teoría de la prueba: 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 prueba de inferencia profunda como la lógica de visualización (introducida por Nuel Belnap en 1982) ^[1] respaldan operadores estructurales tan complejos como los conectivos lógicos y exigen un tratamiento sofisticado.

Eliminación de cortes en el cálculo siguiente.

Deducción natural y correspondencia de fórmulas como tipos

Dualidad lógica y armonía.

hipersecuentes

El marco hipersecuente extiende la estructura secuente ordinaria a un conjunto múltiple de secuentes, utilizando un conectivo estructural adicional | (llamada barra hipersecuente ) para separar diferentes secuencias. Se ha utilizado para proporcionar cálculos analíticos para, por ejemplo, lógicas modales , intermedias y subestructurales ^{[2] [3] [4]} Un hipersecuente es una estructura

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

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

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

para lógicas intermedias, o como 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 hipersecuente, esencialmente todos los cálculos hipersecuentes incluyen las reglas estructurales externas , en particular la regla de debilitamiento externo.

${\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 hipersecuente la proporcionan las reglas que manipulan la estructura hipersecuente. Un ejemplo importante lo proporciona la regla de división modalizada ^[3]

${\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 lógica modal S5 , donde significa que cada fórmula tiene la forma . ${\displaystyle \Box \Sigma }$ ${\displaystyle \Box \Sigma }$ ${\displaystyle \Box A}$

Otro ejemplo lo da la regla de comunicación para la lógica intermedia LC ^[3]

${\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}}}$

Tenga en cuenta que en la regla de comunicación los componentes son secuenciales de conclusión única.

Cálculo de estructuras

Cálculo secuencial anidado

El cálculo secuencial anidado es una formalización que se asemeja a un cálculo de estructuras bilateral.

Notas

1. ND Belnap. "Mostrar lógica". Revista de lógica filosófica , 11 (4), 375–417, 1982.
2. Minc, GE (1971) [Publicado originalmente en ruso en 1968]. "Sobre algunos cálculos de lógica modal". Los cálculos de la lógica simbólica. Actas del Instituto Steklov de Matemáticas . 98 . AMS: 97-124.
3. Avron, Arnon (1996). "El método de los hipersecuentes en la teoría de la prueba de la lógica proposicional no clásica" (PDF) . Lógica: de los fundamentos a las aplicaciones: Coloquio europeo de lógica . Prensa de Clarendon: 1–32.
4. Pottinger, Garrel (1983). "Formulaciones uniformes y sin cortes de T, S4 y S5". Revista de Lógica Simbólica . 48 (3): 900. doi : 10.2307/2273495. JSTOR  2273495. S2CID  250346853.

Referencias

• Sara Negri ; Jan Von Platón (2001). Teoría de la prueba estructural . Prensa de la Universidad de Cambridge. 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.