La transformación de prueba que elimina las inferencias de corte (aplicaciones de la regla cut) de una prueba en estilo cálculo de secuentes para producir una derivación sin cortes del mismo secuente final, preservando la demostrabilidad aunque a menudo cambiando la estructura y el tamaño de la prueba.

Principio

Permutar y simplificar inferencias de modo que cada aplicación de la regla de corte se elimine sucesivamente reemplazándola por derivaciones que sólo utilicen subfórmulas del objetivo; esto preserva la demostrabilidad y produce pruebas analíticas que típicamente disfrutan de la propiedad de subfórmulas.

Demostración

En el cálculo de secuentes de Gentzen, una prueba que usa un corte sobre la fórmula A puede transformarse reemplazando el corte por derivaciones de las subfórmulas de A a partir de las premisas y componiéndolas, obteniéndose una prueba del mismo secuente sin corte; la aplicación repetida elimina todos los cortes.

Aplicación incorrecta

Asumir que la eliminación de cortes preserva la longitud de la prueba, la clase de complejidad o la factibilidad algorítmica en general; usarla para afirmar decidibilidad donde el sistema todavía tiene fragmentos indecidibles, o ignorar que la eliminación puede inflar la prueba exponencialmente o introducir pasos no constructivos en algunos marcos.

Consecuencia

La eliminación del corte produce pruebas sin corte con la propiedad de subfórmulas, permitiendo pruebas de consistencia, resultados de interpolación y un análisis más fino de las pruebas; implica que los lemas introducidos por cortes son admisibles y no esenciales para la demostrabilidad en el sistema considerado.

Inversión

En contraste, permitir cortes equivale a introducir lemas: añadir cortes puede acortar drásticamente las pruebas y proporcionar modularidad y reutilización, de modo que la inversión enfatiza la compacidad de la prueba y su estructura comprensible por humanos más que la forma analítica.

Límite

La eliminación del corte vale en muchos sistemas de prueba estructurales como LK y LJ de Gentzen bajo reglas lógicas estándar, pero puede fallar o requerir modificación en sistemas con reglas no estándar, puntos fijos o definiciones inductivas; la complejidad y la terminación deben considerarse por separado.

Tensión semántica

Existe tensión entre eliminar cortes para obtener pruebas analíticas y conservar cortes para mantener brevedad y estructura; la analiticidad sacrifica compacidad a favor de razonamiento basado en subfórmulas, y los probadores prácticos a menudo reintroducen lemas (cortes) por eficiencia.

Síntesis

La eliminación del corte es la supresión sistemática de inferencias no analíticas en pruebas del cálculo de secuentes: mediante la transformación y permutación de reglas para eliminar cortes se obtienen pruebas con estructura analítica que exponen dependencias de subfórmulas a costa, a veces, de aumento de tamaño o de cambio en el contenido constructivo.