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 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 puede usarse para demostrar cosas tales como 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 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 secuencial ; las pruebas analíticas son las 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 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 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 las conectivas lógicas por las que son interpretados en el cálculo secuencial: 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 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.
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 secuencial original de Getzen, hay poca necesidad de analizarlos. , pero los cálculos de prueba de inferencia profunda como la lógica de visualización (introducido por Nuel Belnap en 1982) [1] apoyan operadores estructurales tan complejos como los conectivos lógicos y exigen un tratamiento sofisticado.
Eliminación de cortes en el cálculo posterior
Deducción natural y correspondencia de fórmulas como tipos
Dualidad lógica y armonía
Hipersecuentes
El marco hipersecuente extiende la estructura secuencial ordinaria a un conjunto múltiple de secuencias, 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] Una hipersecuente es una estructura
donde cada es un secuente ordinario, llamado componente del hipersecuente. En cuanto a los secuentes, los hipersecuentes pueden basarse en conjuntos, conjuntos múltiples o secuencias, y los componentes pueden ser secuentes de conclusión única o de conclusión múltiple . La interpretación de la fórmula de las 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.
para lógicas intermedias, o como disyunción de cajas
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
y la regla de contracción externa
La expresividad adicional del marco hipersecuente es proporcionada por reglas que manipulan la estructura hipersecuente. Un ejemplo importante lo proporciona la regla de división modalizada [3].
para lógica modal S5 , donde significa que cada fórmula en es de la forma .
Otro ejemplo lo da la regla de comunicación para lógica intermedia LC [3]
Tenga en cuenta que en la regla de comunicación los componentes son secuencias de una sola conclusión.
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 lados.
Notas
- ^ ND Belnap. "Mostrar lógica". Journal of Philosophical Logic , 11 (4), 375–417, 1982.
- ^ 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 de Matemáticas Steklov . AMS. 98 : 97-124.
- ^ a b c Avron, Arnon (1996). "El método de las 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.
- ^ 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 .
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.