Regla de corte

En lógica matemática , la regla de corte es una regla de inferencia del cálculo de secuentes . Es una generalización de la regla de inferencia clásica del modus ponens . El significado de la regla de corte es que, si una fórmula A aparece como conclusión en una demostración y como hipótesis en otra, entonces se puede deducir otra demostración en la que la fórmula A no aparece. Esto se aplica a casos del modus ponens , como la forma en que se eliminan instancias de hombre de Todo hombre es mortal, Sócrates es un hombre para deducir Sócrates es mortal .

Las demostraciones en sistemas que incluyen la regla de corte a menudo carecen de la propiedad de subfórmula , lo que significa que puede haber fórmulas en la demostración que no sean subfórmulas de la conclusión. Esto puede causar problemas en algunos métodos de búsqueda de demostraciones. Por ello, suele ser útil razonar sobre sistemas sin la regla de corte . Esto ha dado lugar a numerosos teoremas de eliminación de cortes para muchos sistemas de demostración, tanto en lógica clásica como en lógica no clásica .

La regla de corte normalmente se escribe en notación formal en cálculo de secuentes como  :

${\displaystyle {\begin{array}{c}\Gamma \vdash A,\Delta \quad \Gamma ',A\vdash \Delta '\\\hline \Gamma ,\Gamma '\vdash \Delta ,\Delta '\end{array}}}$cortar ^{[ 1 ]}

La regla de corte es objeto de un teorema importante, el teorema de eliminación de cortes . Este teorema establece que cualquier secuencia que tenga una demostración en el cálculo de secuencias que utilice la regla de corte también tiene una demostración sin cortes, es decir, una demostración que no utiliza dicha regla.