Eliminación de Cortes

La eliminación de cortes es el teorema de Gentzen que establece que la regla de corte, que formaliza el uso de lemas, puede ser eliminada de cualquier prueba de cálculo de secuentes, dejando una prueba construida únicamente a partir de las fórmulas que le conciernen.

Definition

La eliminación de cortes es el teorema y el procedimiento constructivo que demuestra que cualquier derivación de cálculo de secuentes que utilice la regla de corte puede transformarse en una que no la utilice, de modo que cada secuente demostrable tiene una prueba en la que solo aparecen subfórmulas del secuente final.

Scope

Este tema abarca la regla de corte y su papel en el cálculo de secuentes, el procedimiento de eliminación de cortes y su terminación, la propiedad de subfórmula de las pruebas sin cortes, las consecuencias resultantes en términos de consistencia y decidibilidad, y los límites en el tamaño de la prueba que la eliminación puede implicar.

Core questions

• ¿Qué expresa la regla de corte y por qué es significativa su eliminación?
• ¿Cómo termina el procedimiento de eliminación de cortes?
• ¿Qué es la propiedad de subfórmula y qué implica para la búsqueda de pruebas?
• ¿Cuál es el costo computacional de eliminar cortes?

Key theories

Hauptsatz de Gentzen

El teorema principal de Gentzen establece que la regla de corte es admisible en el cálculo de secuentes, por lo que cualquier prueba que utilice cortes puede convertirse en una prueba sin cortes del mismo secuente final.

Propiedad de subfórmula

Cada fórmula que aparece en una prueba sin cortes es una subfórmula del secuente final, lo que restringe la forma de la prueba y subyace a los procedimientos de decisión y los argumentos de consistencia.

Consistencia mediante eliminación de cortes

Dado que una prueba sin cortes del secuente vacío es imposible, la eliminación de cortes proporciona una prueba directa de que el cálculo, y por lo tanto la teoría que formaliza, es consistente.

Clinical relevance

La eliminación de cortes es un resultado fundamental con amplias consecuencias: produce pruebas de consistencia, la propiedad de subfórmula esencial para la demostración automática de teoremas y los métodos de tableau, teoremas de interpolación y, a través de la correspondencia pruebas-como-programas, la normalización de programas tipados.

History

Gentzen demostró la eliminación de cortes, su Hauptsatz, en 1934 para la lógica de primer orden, y el método se convirtió en la piedra angular de la teoría de la prueba estructural. Tait y Girard extendieron la técnica a sistemas más potentes y a la lógica de orden superior, y los límites del crecimiento del tamaño de la prueba bajo la eliminación de cortes se convirtieron en un tema de estudio por derecho propio.

Key figures

• Gerhard Gentzen
• William Tait
• Jean-Yves Girard
• Gaisi Takeuti

Seminal works

• takeuti1987
• troelstra2000
• negri2001

Frequently asked questions

¿Qué es un corte en una prueba?

La regla de corte permite demostrar un lema y luego usarlo: a partir de una derivación que establece una fórmula y otra que usa esa fórmula como premisa, concluye el resultado combinado. La eliminación de cortes demuestra que tales lemas intermedios siempre pueden eliminarse en principio.

¿Por qué la eliminación de cortes puede hacer que las pruebas sean mucho más largas?

La eliminación de un corte puede requerir la duplicación de grandes partes de una derivación, y la iteración de esto puede aumentar el tamaño de la prueba en una torre de exponenciales. Por lo tanto, las pruebas sin cortes son conceptualmente más simples, pero pueden ser mucho más grandes que las pruebas originales con cortes.