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 respaldan 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 se puede utilizar 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, el tipo de tarea que se asigna con más frecuencia a la teoría de modelos . ^[1]

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 secuencial ; las pruebas analíticas son aquellas que no tienen cortes . Su cálculo de deducción natural también respalda una noción de prueba analítica, como lo demostró Dag Prawitz ; la definición es ligeramente 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 conectores

El término estructura en la teoría de la prueba estructural proviene de una noción técnica introducida en el cálculo secuencial: el cálculo secuencial representa el juicio realizado en cualquier etapa de una inferencia utilizando operadores extralógicos especiales llamados operadores estructurales: en , las comas a la izquierda del torniquete son operadores normalmente interpretados 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 conectivos lógicos por los que se interpretan en el cálculo secuencial: los operadores estructurales se utilizan en cada regla del cálculo y no se consideran cuando se pregunta si se aplica la propiedad de subfórmula. Además, las reglas lógicas van en una sola 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 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, no lógicos, no es antigua, y fue forzada por las innovaciones en la teoría de la prueba: cuando los operadores estructurales son tan simples como en el cálculo secuente 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) ^[2] admiten operadores estructurales tan complejos como los conectivos lógicos, y exigen un tratamiento sofisticado.

Eliminación de cortes en el cálculo secuencial

La deducción natural y la correspondencia entre fórmulas y tipos

Dualidad lógica y armonía

Hipersecientes

El marco hipersecuente extiende la estructura secuente ordinaria a un conjunto múltiple 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 ^{[3] [4] [5]} Una hipersecuente es una estructura

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

donde cada uno es un consecuente ordinario, llamado componente del hiperconsecuente. En cuanto a los consecuentes, los hiperconsecuentes pueden basarse en conjuntos, multiconjuntos o secuencias, y los componentes pueden ser consecuentes de conclusión única o de múltiples conclusiones . La interpretación de la fórmula de los hiperconsecuentes depende de la lógica en consideración, pero casi siempre es alguna forma de disyunción. Las interpretaciones más comunes son como una disyunción simple. ${\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 se obtiene mediante reglas que manipulan la estructura hipersecuente. Un ejemplo importante lo proporciona la regla de división modalizada ^[4].

${\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 significa que cada fórmula en 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 ^[4]

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

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 de dos caras.

Notas

1. "Teoría de la prueba estructural". www.philpapers.org . Consultado el 18 de agosto de 2024 .
2. ND Belnap. "Lógica de visualización". Revista de lógica filosófica , 11 (4), 375–417, 1982.
3. Minc, GE (1971) [Publicado originalmente en ruso en 1968]. "Sobre algunos cálculos de lógica modal". Los cálculos de lógica simbólica. Actas del Instituto Steklov de Matemáticas . 98. AMS: 97–124.
4. Avron, Arnon (1996). "El método de hipersecuentes en la teoría de la demostración de lógicas proposicionales no clásicas" (PDF) . Lógica: de los fundamentos a las aplicaciones: Coloquio europeo de lógica . Clarendon Press: 1–32.
5. Pottinger, Garrel (1983). "Formulaciones uniformes y sin cortes de T, S4 y S5". Journal of Symbolic Logic . 48 (3): 900. doi :10.2307/2273495. JSTOR  2273495. S2CID  250346853.

Referencias

• Sara Negri y Jan Von Plato (2001). Teoría de la prueba 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.