El teorema de eliminación de cortes (o Hauptsatz de Gentzen ) es el resultado central que establece la importancia del cálculo secuente . Fue probado originalmente por Gerhard Gentzen en su histórico artículo de 1934 "Investigaciones en deducción lógica" para los sistemas LJ y LK que formalizan 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 secuente que haga uso de la regla de corte también posee una prueba sin cortes , es decir, una prueba que no haga uso de la regla de corte. [1] [2]
Un secuente es una expresión lógica que relaciona múltiples fórmulas, en la forma " " , que debe leerse como " prueba " y (según lo glosado por Gentzen) debe entenderse como equivalente a la función de verdad "Si ( y y ...) entonces ( o o …)." [3] Tenga en cuenta que el lado izquierdo (LHS) es una conjunción (y) y el lado derecho (RHS) es una disyunción (o).
El LHS puede tener muchas o pocas fórmulas arbitrariamente; 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 del derecho, a la admisibilidad de la ley del tercero 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. De la lógica LC de Jean-Yves Girard es fácil obtener una formalización bastante natural de la lógica clásica donde la RHS contiene como máximo una fórmula; la clave aquí es la interacción de las reglas lógicas y estructurales.
"Cortar" es una regla en el enunciado normal del cálculo secuente , y equivalente a una variedad de reglas en otras teorías de demostración , que, dadas
y
permite inferir
Es decir, "corta" las apariciones de la fórmula fuera de la relación inferencial.
El teorema de eliminación de cortes establece que (para un sistema dado) cualquier secuente demostrable usando la regla Corte se puede demostrar sin el uso de esta regla.
Para cálculos sucesivos que tienen una sola fórmula en el RHS, la regla de "Corte" dice, dada
y
permite inferir
Si lo pensamos como un teorema, entonces la eliminación por corte en este caso simplemente dice que un lema utilizado para demostrar este teorema puede incluirse. Siempre que la prueba del teorema mencione el lema , podemos sustituir las ocurrencias por la prueba de . En consecuencia, la norma de corte es admisible .
Para sistemas formulados en el cálculo siguiente, las pruebas analíticas son aquellas pruebas que no utilizan Cut. Normalmente, una prueba de este tipo será más larga, por supuesto, y no necesariamente trivial. En su ensayo "¡No elimines el corte!" [4] George Boolos demostró que había una derivación que podía completarse en una página usando corte, pero cuya prueba analítica no podía completarse en la vida útil del universo.
El teorema tiene muchas y ricas consecuencias:
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 , el conocimiento esencial que conduce al lenguaje de programación Prolog , depende de la admisibilidad de Cut en el sistema apropiado.
Para sistemas de prueba basados en cálculo lambda tipado de orden superior mediante 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 ).
