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 consecuente que no se refiere a ningún conectivo lógico sino que opera sobre los consecuentes directamente. ^{[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 .

Normas estructurales comunes

Tres reglas estructurales comunes son: ^[3]

• Debilitamiento , donde las hipótesis o conclusiones de una secuencia pueden extenderse con miembros adicionales. En forma simbólica, las reglas de debilitamiento pueden escribirse como a la izquierda del torniquete y a la derecha. Se conoce como monotonía 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 , en la que dos miembros iguales (o unificables) del mismo lado de una secuencia pueden ser reemplazados por un solo miembro (o instancia común). Simbólicamente: y . También conocida como factorización en sistemas de demostración automática de teoremas mediante resolución . Conocida como idempotencia de implicació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 , en el que dos miembros del mismo lado de un secuencial pueden intercambiarse. 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 con contracción e intercambio pueden considerarse conjuntos .

Estas no son las únicas reglas estructurales posibles. Una famosa regla estructural es la conocida como cut ^[1] . Los teóricos de la demostración dedican un esfuerzo considerable a demostrar que las reglas de corte son superfluas en varias lógicas. Más precisamente, lo que se demuestra es que cut es solo (en cierto sentido) una herramienta para abreviar las demostraciones y no agrega nada a los teoremas que se pueden demostrar. 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 dada.

Véase también

• Lógica afín  : lógica subestructural cuya teoría de prueba rechaza la regla estructural de contracción.Pá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, ME (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.