Luis Ricardo|
Sierra Abbate|
sierra@fing.edu.uy|
Instituto de Computación|
El corte de un teorema|
Gentzen, Hauptsatz, Cálculo de secuentes, Inducción estructural|
INVESTIGACION|
|
A mitad de la década de 1930 Gentzen propone un estilo de presentación 
de pruebas que dio en llamar deducción natural. En sus "Investigaciones
sobre la deducción lógica" propone distintos lenguajes formales para las
pruebas, y demuestra el teorema del corte. Este teorema,
llamado originalmente Hauptsatz, permite justificar lo siguiente: toda
tesis se puede probar formalmente sin usar más elementos que los que
aparecen en ella.

La prueba que Gentzen propone de dicho teorema no solamente es extensa, 
sino que también es complicada, requiriendo el uso de distintas estrategias.
A pesar de su complicación, la misma prueba es presentada en distintos
textos hasta hoy.

Sin embargo, es posible otra prueba usando inducción estructural de forma
directa. En esta presentación mostraremos una versión reducida de este 
teorema, tanto en su forma original como en la que consideramos más adecuada,
abriendo un espacio para la reflexión acerca de la permanencia de formatos
inadecuados en las propuestas matemáticas más populares.

(De la Real Academia Española.

corte.
6. m. Arte y acción de cortar las diferentes piezas que requiere la hechura de un vestido, de un calzado u otras cosas.
)|