En lógica matemática , la regla de corte es una regla de inferencia del cálculo secuencial . Es una generalización de la regla de inferencia clásica del modus ponens . Su significado es que, si una fórmula A aparece como conclusión en una prueba y una hipótesis en otra, entonces se puede deducir otra prueba en la que no aparece la fórmula A. En el caso particular del modus ponens, por ejemplo , se eliminan las ocurrencias del hombre. Todo hombre es mortal, Sócrates es un hombre para deducir que Sócrates es mortal .
Notación formal
Notación formal en notación de cálculo secuencial:
- cortar
Eliminación
La regla de corte es objeto de un teorema importante, el teorema de eliminación de cortes . Establece que cualquier juicio que posea una prueba en el cálculo posterior que haga uso de la regla de corte también posee una prueba libre de cortes, es decir, una prueba que no hace uso de la regla de corte.