Teorema de corte-eliminación
El teorema de corte-eliminación (o Gentzen Hauptsatz) es un teorema que establece la importancia del cálculo de secuentes. Fue demostrado por Gerhard Gentzen en 1934 en su artículo Investigaciones sobre la deducción lógica para los sistemas LJ y LK formalizando la lógica intuicionista y la lógica clásica, respectivamente. El teorema de corte-eliminación establece que cualquier demostración que tenga una demostración en el cálculo de secuentes y use la regla de corte, también tiene una demostración sin corte, es decir que no haga uso de la regla de corte.[1][2]
Notas y referencias
editar- ↑ Curry, 1977, pp. 208–213 da una demostración de cinco páginas.
- ↑ Kleene, 2009, pp. 453 da una demostración muy breve.
Datos: Q376166
