Evidencia y Normalización: Análisis Constructivo en Deducción Natural

Ponente(s): Eduardo Ugalde Reyes, Favio Ezequiel Miranda Perea, Lourdes del Carmen González Huesca.

Este trabajo aborda una tensión explicativa en las pruebas de normalización dentro de la lógica intuicionista: los enfoques algebraicos (cálculo-lambda) privilegian garantías formales, mientras que los diagramáticos (deducción natural) preservan la articulación constructiva del razonamiento. Aunque correctas, las pruebas estándar en cálculo-lambda suelen oscurecer el curso constructivo de las derivaciones y el papel epistémico de la normalización. Proponemos un marco de prueba transicional que entrelaza reglas del cálculo-lambda con el razonamiento diagramático de la deducción natural. Revirtiendo y refinando gramáticas de códigos de prueba a partir de la correspondencia Curry–Howard, otorgamos a dichos códigos una lectura diagramática que recupera su contenido inferencial explícito. Así, cada paso reductivo se muestra como una continuación necesaria del proceso demostrativo, no como una reescritura sintáctica externa. En un caso de lógica intuicionista proposicional , mostramos cómo una formalización guiada por la estructura del razonamiento permite una traducción más “fiel” entre prueba informal y formalización asistida, apuntando a formalizaciones computacionalmente verificables pero conceptualmente claras.