En la teoría de la prueba , una regla estructural es una regla de inferencia que no se refiere a ningún conectivo lógico , sino que opera directamente sobre el juicio o las secuencias . Las reglas estructurales a menudo imitan las propiedades metateóricas pretendidas de la lógica. Las lógicas que niegan una o más de las reglas estructurales se clasifican como lógicas subestructurales .
Reglas estructurales comunes
Tres reglas estructurales comunes son:
- Debilitamiento , donde la hipótesis o conclusión de un secuente puede extenderse con miembros adicionales. En forma simbólica, las reglas de debilitamiento se pueden escribir comoa la izquierda del torniquete , y a la derecha.
- Contracción , donde dos miembros iguales (o unificables) en el mismo lado de una secuencia pueden ser reemplazados por un solo miembro (o instancia común). Simbólicamente: y . También conocido como factorización en sistemas automatizados de prueba de teoremas usando resolución . Conocido como idempotencia de vinculación en lógica clásica.
- Intercambio , donde se pueden intercambiar dos miembros del mismo lado de una secuencia. Simbólicamente: y . (Esto también se conoce como la regla de permutación ).
Una lógica sin ninguna de las reglas estructurales anteriores interpretaría los lados de un secuente como secuencias puras ; con intercambio, son multijuegos ; y tanto con contracción como con cambio son conjuntos .
Éstas no son las únicas reglas estructurales posibles. Una famosa regla estructural se conoce como corte . Los teóricos de la prueba dedican un esfuerzo considerable a demostrar que las reglas de corte son superfluas en varias lógicas. Más precisamente, lo que se muestra es que cortar es sólo (en cierto sentido) una herramienta para abreviar demostraciones y no se suma a los teoremas que pueden demostrarse. La "eliminación" exitosa de las reglas de corte, conocida como eliminación de cortes , está directamente relacionada con la filosofía de la computación como normalización (ver correspondencia Curry-Howard ); a menudo da una buena indicación de la complejidad de decidir una lógica dada.
Ver también
- Lógica afín
- Lógica lineal
- Lógica ordenada
- Lógica estricta
- Lógica de separación