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 están expuestas. Cuando todos los teoremas de una lógica formalizada en una teoría de prueba estructural tienen pruebas analíticas, entonces la teoría de prueba se puede usar 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 le da más a menudo a la teoría de modelos .
La noción de prueba analítica fue introducida en la teoría de la prueba por Gerhard Gentzen para el cálculo de secuencias ; las pruebas analíticas son las que están libres de corte . 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 .
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 usando operadores extralógicos especiales llamados operadores estructurales: en , las comas a la izquierda de los torniquetes son operadores que normalmente se interpretan como conjunciones, los de la derecha como disyunciones, mientras que el propio símbolo del torniquete se interpreta como una implicación. Sin embargo, es importante notar que existe una diferencia fundamental en el comportamiento entre estos operadores y los conectivos lógicosse interpretan en el cálculo secuente: los operadores estructurales se utilizan en todas las reglas del cálculo y no se tienen en cuenta al preguntar si se aplica la propiedad de la 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.
La idea de ver las características sintácticas de los secuentes como operadores especiales no lógicos no es vieja y fue forzada por las innovaciones en la teoría de la demostración: 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) [1] admiten operadores estructurales tan complejos como los conectores lógicos y exigen un tratamiento sofisticado.
El marco hipersecuente extiende la estructura secuente ordinaria a un conjunto múltiple de secuentes , utilizando un conectivo estructural adicional | (llamada la barra hipersecuente ) para separar diferentes secuencias. Se ha utilizado para proporcionar cálculos analíticos para, por ejemplo, lógica modal , intermedia y subestructural [2] [3] [4] Una hipersecuente es una estructura
