Ejemplo de corte en la deducción natural y cómo eliminarlo

Question

Ya había oído hablar del Corte en el Cálculo Secuencial, pero parece que también existe para la Deducción Natural. Por favor, ¿podría proporcionar una prueba en la deducción natural (lógica proposicional) que ilustra el uso de un corte?

Además, hay un teorema en el Cálculo Secuencial que transforma las pruebas que usan Cut en pruebas que no lo usan. ¿Existe un teorema equivalente para Cortes en Deducción Natural? ¿Podrías proporcionar la prueba correspondiente (de la que has dado para lo anterior) que ahora no haga uso del Corte?

He intentado encontrar información sobre el Corte para la Deducción Natural, pero parece que la mayoría de la literatura habla de ello con respecto al Cálculo Secuencial. ¿Podría deberse esto a que el Corte para la Deducción Natural tiene un nombre diferente? Se agradecen mucho los enlaces a recursos, pero no son necesarios. ¡Muchas gracias por sus respuestas de antemano!

Edición: esta pregunta se refiere más a ejemplos sencillos que ilustren los conceptos implicados, que a las pruebas formales de dichos conceptos (y a establecer la terminología correcta con respecto a estos conceptos).

Answer 1

Como puede verse en Sara Negri & Jan von Plato, Teoría de la prueba estructural (2001), página 18, en Deducción natural tenemos el regla de sustitución que es una "regla derivada":

En deducción natural, si dos derivaciones $\Gamma \vdash A$ y $A, \Delta \vdash C$ podemos unirlas en una derivación $\Gamma, \Delta \vdash C$ a través de un sustitución :

$${ \Gamma \vdash A \quad A, \Delta \vdash C \over \Gamma, \Delta \vdash C } \, \text{(Subst)}$$

La regla del cálculo secuencial correspondiente es corte :

$${ \Gamma \implies A \quad A, \Delta \implies C \over \Gamma, \Delta \implies C } \, \text{(Cut)}$$

A menudo, el corte se explica de la siguiente manera: Desglosamos la derivación de $C$ a partir de algunos supuestos en "lemas", pasos intermedios que son más fáciles de demostrar y que se encadenan de la forma que muestra la regla de corte.

Pero véase también [página 172] :

La regla [de sustitución] se parece al corte, pero es de naturaleza diferente: El cierre bajo sustitución sólo afirma que la sustitución mediante la unión de derivaciones produce una derivación correcta. Esto se ve claramente en la prueba de la admisibilidad de la sustitución.

En la deducción natural al estilo del cálculo secuencial, no hay fórmulas principales en el antecedente, y por tanto la fórmula de sustitución en la premisa derecha también aparece en al menos alguna premisa de la regla que concluye la premisa derecha. La sustitución se permuta hasta que la premisa derecha es una suposición.

La eliminación de la sustitución es muy diferente de la eliminación del corte.