Teorema de eliminación de cortes

Teorema en lógica formal

El teorema de eliminación de cortes (o Hauptsatz de Gentzen ) es el resultado central que establece la importancia del cálculo secuencial . Fue demostrado originalmente por Gerhard Gentzen en su artículo de referencia de 1934 "Investigaciones en deducción lógica" para los sistemas LJ y LK que formalizaban la lógica intuicionista y clásica respectivamente. El teorema de eliminación de cortes establece que cualquier juicio que posea una prueba en el cálculo secuencial que haga uso de la regla de cortes también posee una prueba libre de cortes , es decir, una prueba que no haga uso de la regla de cortes. ^{[1] [2]}

La regla del corte

Un consecuente es una expresión lógica que relaciona múltiples fórmulas, en la forma " " ${\displaystyle A_{1},A_{2},A_{3},\ldots \vdash B_{1},B_{2},B_{3},\ldots }$ , que debe leerse como " ${\displaystyle A_{1},A_{2},A_{3},\ldots }$ prueba " , y (como lo explica Gentzen) debe entenderse como equivalente a la función de verdad "Si ( y y …) entonces ( o o …)". ^[3] Nótese que el lado izquierdo (LHS) es una conjunción (y) y el lado derecho (RHS) es una disyunción (o). ${\displaystyle B_{1},B_{2},B_{3},\ldots }$ ${\displaystyle A_{1}}$ ${\displaystyle A_{2}}$ ${\displaystyle A_{3}}$ ${\displaystyle B_{1}}$ ${\displaystyle B_{2}}$ ${\displaystyle B_{3}}$

El LHS puede tener arbitrariamente muchas o pocas fórmulas; cuando el LHS está vacío, el RHS es una tautología . En LK, el RHS también puede tener cualquier número de fórmulas; si no tiene ninguna, el LHS es una contradicción , mientras que en LJ el RHS puede tener solo una fórmula o ninguna: aquí vemos que permitir más de una fórmula en el RHS es equivalente, en presencia de la regla de contracción derecha, a la admisibilidad de la ley del medio excluido . Sin embargo, el cálculo secuencial es un marco bastante expresivo, y se han propuesto cálculos secuenciales para la lógica intuicionista que permiten muchas fórmulas en el RHS. A partir de la LC de lógica de Jean-Yves Girard es fácil obtener una formalización bastante natural de la lógica clásica donde el RHS contiene como máximo una fórmula; es la interacción de las reglas lógicas y estructurales la clave aquí.

"Cortar" es una regla de inferencia en el enunciado normal del cálculo secuencial , y equivalente a una variedad de reglas en otras teorías de prueba , que, dadas

1. ${\displaystyle \Gamma \vdash A,\Delta }$

y

2. ${\displaystyle \Pi ,A\vdash \Lambda }$

permite inferir

3. ${\displaystyle \Gamma ,\Pi \vdash \Delta ,\Lambda }$

Es decir, “corta” las ocurrencias de la fórmula fuera de la relación inferencial. ${\displaystyle A}$

Eliminación de cortes

El teorema de eliminación de cortes establece que (para un sistema dado) cualquier secuencia demostrable usando la regla de Corte puede demostrarse sin el uso de esta regla.

Para los cálculos secuenciales que tienen solo una fórmula en el lado derecho, la regla de "Corte" dice:

1. ${\displaystyle \Gamma \vdash A}$

y

2. ${\displaystyle \Pi ,A\vdash B}$

permite inferir

3. ${\displaystyle \Gamma ,\Pi \vdash B}$

Si pensamos en un teorema, entonces la eliminación de cortes en este caso simplemente dice que un lema usado para demostrar este teorema puede incluirse en línea. Siempre que la prueba del teorema mencione el lema , podemos sustituir las ocurrencias por la prueba de . En consecuencia, la regla de corte es admisible . ${\displaystyle B}$ ${\displaystyle A}$ ${\displaystyle A}$ ${\displaystyle A}$

Consecuencias del teorema

Para los sistemas formulados en el cálculo secuencial, las pruebas analíticas son aquellas que no utilizan Cut. Por lo general, estas pruebas serán más largas, por supuesto, y no necesariamente triviales. En su ensayo "Don't Eliminar Cut!" ^[4] George Boolos demostró que había una derivación que podía completarse en una página utilizando cut, pero cuya prueba analítica no podía completarse durante la vida del universo.

El teorema tiene muchas y valiosas consecuencias:

• Un sistema es inconsistente si admite una prueba del absurdo. Si el sistema tiene un teorema de eliminación de cortes, entonces si tiene una prueba del absurdo, o del consecuente vacío, también debería tener una prueba del absurdo (o del consecuente vacío), sin cortes. Normalmente es muy fácil comprobar que no existen tales pruebas. Por lo tanto, una vez que se demuestra que un sistema tiene un teorema de eliminación de cortes, normalmente es inmediato que el sistema es consistente.
• Normalmente el sistema también tiene, al menos en lógica de primer orden, la propiedad de subfórmula , una propiedad importante en varios enfoques de la semántica de teoría de pruebas .

La eliminación de cortes es una de las herramientas más poderosas para demostrar teoremas de interpolación . La posibilidad de realizar una búsqueda de pruebas basada en la resolución , la idea esencial que dio origen al lenguaje de programación Prolog , depende de la admisibilidad de Cut en el sistema apropiado.

Para los sistemas de prueba basados ​​en el cálculo lambda tipado de orden superior a través de un isomorfismo de Curry-Howard , los algoritmos de eliminación de cortes corresponden a la propiedad de normalización fuerte (cada término de prueba se reduce en un número finito de pasos a una forma normal ).

Véase también

• Teorema de deducción
• Prueba de consistencia de Gentzen para los axiomas de Peano

Notas

1. Curry 1977, pp. 208-213, ofrece una demostración de cinco páginas del teorema de eliminación. Véanse también las páginas 188 y 250.
2. Kleene 2009, págs. 453, ofrece una prueba muy breve del teorema de eliminación de cortes.
3. Wilfried Buchholz, Beweistheorie (apuntes de clase universitaria sobre eliminación de cortes, alemán, 2002-2003)
4. Boolos 1984, págs. 373–378

Referencias

• Gentzen, Gerhard (1935). "Untersuchungen über das logische Schließen. I.". Mathematische Zeitschrift . 39 : 176-210. doi :10.1007/BF01201353.
  • Untersuchungen über das logische Schließen I (Archive.org)
  • Gentzen, Gerhard (1964). "Investigaciones sobre la deducción lógica". American Philosophical Quarterly . 1 (4): 249–287.
• Gentzen, Gerhard (1935). "Untersuchungen über das logische Schließen. II". Mathematische Zeitschrift . 39 : 405–431. doi :10.1007/BF01201363.
  • Untersuchungen über das logische Schließen II (Archive.org)
  • Gentzen, Gerhard (1965). "Investigaciones sobre la deducción lógica". American Philosophical Quarterly . 2 (3): 204–218.
• Curry, Haskell Brooks (1977) [1963]. Fundamentos de lógica matemática . Nueva York: Dover Publications Inc. ISBN 978-0-486-63462-3.
• Kleene, Stephen Cole (2009) [1952]. Introducción a las metamatemáticas . Ishi Press International. ISBN 978-0-923891-57-2.
• Boolos, George (1984). "No elimines el corte". Revista de lógica filosófica . 13 (4): 373–378.

Enlaces externos

• Alex Sakharov. "Teorema de eliminación de cortes". MathWorld .
• Dragalin, AG (2001) [1994], "Cálculo secuencial", Enciclopedia de Matemáticas , EMS Press