Regla estructural

En la disciplina lógica de la teoría de la demostración , una regla estructural es una regla de inferencia de un cálculo de secuentes que no hace referencia a ningún conector lógico , sino que opera directamente sobre los secuentes . ^{[ 1 ] [ 2 ]} Las reglas estructurales a menudo imitan las propiedades metateóricas previstas de la lógica. Las lógicas que niegan una o más de las reglas estructurales se clasifican como lógicas subestructurales .

Tres reglas estructurales comunes son: ^{[ 3 ]}

• Debilitamiento , donde las hipótesis o la conclusión de una secuencia pueden extenderse con miembros adicionales. En forma simbólica, las reglas de debilitamiento pueden escribirse como${\displaystyle {\frac {\Gamma \vdash \Sigma }{\Gamma ,A\vdash \Sigma }}}$a la izquierda del torniquete y${\displaystyle {\frac {\Gamma \vdash \Sigma }{\Gamma \vdash \Sigma ,A}}}$A la derecha. Conocida como monotonicidad de la implicación en lógica clásica.
• Contracción , donde dos miembros iguales (o unificables) en el mismo lado de un secuente pueden ser reemplazados por un solo miembro (o instancia común). Simbólicamente:${\displaystyle {\frac {\Gamma ,A,A\vdash \Sigma }{\Gamma ,A\vdash \Sigma }}}$y${\displaystyle {\frac {\Gamma \vdash A,A,\Sigma }{\Gamma \vdash A,\Sigma }}}$También conocido como factorización en sistemas automatizados de demostración de teoremas mediante resolución . Conocido como idempotencia de la implicación en lógica clásica.
• Intercambio , donde dos miembros del mismo lado de una secuencia pueden intercambiarse. 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 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, pueden considerarse multiconjuntos ; y con contracción e intercambio pueden considerarse conjuntos .

Estas no son las únicas reglas estructurales posibles. Una regla estructural famosa se conoce como corte . ^{[ 1 ]} Los teóricos de la demostración dedican un esfuerzo considerable a demostrar que las reglas de corte son superfluas en diversas lógicas. Más precisamente, lo que se demuestra es que el corte es solo (en cierto sentido) una herramienta para abreviar las demostraciones, y no añade teoremas que se pueden probar. La "eliminación" exitosa de las reglas de corte, conocida como eliminación de corte , está directamente relacionada con la filosofía de la computación como normalización (véase la correspondencia Curry-Howard ); a menudo proporciona una buena indicación de la complejidad de decidir una lógica dada.

• Lógica afín : lógica sensible a los recursos que permite que cada suposición se utilice como máximo una vez. 
• Lógica lineal : sistema de lógica sensible a los recursos. 
• Lógica ordenada (lógica lineal) – Extensión de la lógica lineal Páginas que muestran descripciones breves de los destinos de redireccionamiento 
• Lógica de relevancia : un tipo de lógica no clásica. 
• Lógica de separación : un concepto en informática.