Regla estructural

format_list_bulleted Contenido keyboard_arrow_down

ImprimirCitar

Regla de lógica matemática

En la disciplina lógica de la teoría de la prueba, una regla estructural es una regla de inferencia de un cálculo de secuentes que no se refiere a ningún conectivo lógico sino que opera directamente sobre los secuentes. Las reglas estructurales a menudo imitan las propiedades metateóricas pretendidas de la lógica. Las lógicas que niegan una o más reglas estructurales se clasifican como lógicas subestructurales.

Reglas estructurales comunes

Tres reglas estructurales comunes son:

Debilitamiento, donde las hipótesis o conclusión de una secuencia se pueden extender con miembros adicionales. En forma simbólica las reglas de debilitamiento pueden ser escritas como ${displaystyle {frac {Gamma vdash Sigma }{GammaAvdash Sigma }}}$ a la izquierda del torntil, y ${displaystyle {frac {Gamma vdash Sigma }{Gamma vdash SigmaA}}}$ a la derecha. Conocido como monotónica de implicación en la lógica clásica.
Contracciones, donde dos miembros iguales (o no identificables) del mismo lado de un secuenciador pueden ser reemplazados por un solo miembro (o instancia común). Simbólicamente: ${displaystyle {frac {GammaA,Avdash Sigma }{GammaAvdash Sigma }}}$ y ${displaystyle {frac {Gamma vdash A,A,Sigma }{Gamma vdash A,Sigma }}}$ . También conocido como factorización en sistemas de prueba de teorema automatizados mediante resolución. Conocido como idempotencia de la implicación en la lógica clásica.
Cambio, donde dos miembros en el mismo lado de un secuenciador pueden ser intercambiados. Simbólicamente: ${displaystyle {frac {Gamma _{1},A,Gamma _{2},B,Gamma _{3}vdash Sigma }{Gamma _{1},B,Gamma _{2},A,Gamma _{3}vdash Sigma }}}$ y ${displaystyle {frac {Gamma vdash Sigma _{1},A,Sigma _{2},B,Sigma _{3}}{Gamma vdash Sigma _{1},B,Sigma _{2},A,Sigma _{3}}}}$ . (Esto también se conoce como el 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, pueden considerarse multiconjuntos; y tanto con contracción como con intercambio se pueden considerar conjuntos.

Estas no son las únicas reglas estructurales posibles. Una regla estructural famosa se conoce como cortar. Los teóricos de la prueba dedican un esfuerzo considerable a demostrar que las reglas de corte son superfluas en diversas 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 aumenta los teoremas que pueden demostrarse. La exitosa 'eliminación' de reglas de corte, conocida como eliminación de corte, 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 determinada.

Contenido relacionado

Más resultados...