regla estructural

Regla de la 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 . ^{[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 .

Reglas estructurales comunes

Tres reglas estructurales comunes son: ^[3]

• Debilitamiento , donde las hipótesis o conclusión de una secuencia pueden ampliarse con miembros adicionales. En forma simbólica, las reglas debilitantes se pueden escribir como a la izquierda del torniquete y a la derecha. Conocido como monotonicidad de implicación en lógica clásica. ${\displaystyle {\frac {\Gamma \vdash \Sigma }{\Gamma ,A\vdash \Sigma }}}$ ${\displaystyle {\frac {\Gamma \vdash \Sigma }{\Gamma \vdash \Sigma ,A}}}$
• 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: y . También conocido como factorización en sistemas automatizados de demostración de teoremas mediante resolución . Conocida como idempotencia de vinculación en lógica clásica. ${\displaystyle {\frac {\Gamma ,A,A\vdash \Sigma }{\Gamma ,A\vdash \Sigma }}}$ ${\displaystyle {\frac {\Gamma \vdash A,A,\Sigma }{\Gamma \vdash A,\Sigma }}}$
• Intercambio , donde se pueden intercambiar dos miembros del mismo lado de un secuente. Simbólicamente: y . (Esto también se conoce como regla de permutación ). ${\displaystyle {\frac {\Gamma _{1},A,\Gamma _{2},B,\Gamma _{3}\vdash \Sigma }{\Gamma _{1},B,\Gamma _{2},A,\Gamma _{3}\vdash \Sigma }}}$ ${\displaystyle {\frac {\Gamma \vdash \Sigma _{1},A,\Sigma _{2},B,\Sigma _{3}}{\Gamma \vdash \Sigma _{1},B,\Sigma _{2},A,\Sigma _{3}}}}$

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 .

Éstas no son las únicas reglas estructurales posibles. Una regla estructural famosa se conoce como corte . ^[1] 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 "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 (ver correspondencia Curry-Howard ); a menudo da una buena indicación de la complejidad de decidir una lógica determinada.

Ver también

• Lógica afín  : lógica subestructural cuya teoría de prueba rechaza la regla estructural de contracciónPáginas que muestran descripciones de wikidata como alternativa
• Lógica lineal  : sistema de lógica consciente de los recursos
• Lógica ordenada (lógica lineal)
• Lógica de relevancia  : sistema lógico matemático que impone ciertas restricciones a la implicación.Páginas que muestran descripciones de wikidata como alternativa
• Lógica de separación

Referencias

1. Gentzen, Gerhard (1935). "Untersuchungen über das logische Schließen. Yo, Mathematische Zeitschrift". Mathematische Zeitschrift (en alemán). 39 (1): 176–210. doi :10.1007/BF01201353. ISSN  0025-5874.
2. Szabo, YO (1969). Documentos recopilados de Gerhard Gentzen . Lugar de publicación no identificado: Elsevier. ISBN 978-0-444-53419-4.
3. Jacobs, Bart (1994). "Semántica del debilitamiento y la contracción". Anales de lógica pura y aplicada . 69 (1): 73–106. doi :10.1016/0168-0072(94)90020-5.