Conferencia
La Correspondencia Curry-Howard como semántica de la Lógica Intuicionista​

Resumen

La correspondencia Curry-Howard es la (sorprendente) observación de que el tipeo de términos funcionales en cálculo lambda (una teoría matemática relacionada con la computación abstracta) es un procedimiento que “coincide”, punto por punto, con la derivación en el cálculo de deducción natural de la lógica intuicionista. De esta manera, las reglas para componer y destruir tipos son equivalentes a las reglas de introducción y eliminación de las conectivas. Este resultado ha sido muy importante para el desarrollo de la teoría de la computación de los últimos sesenta años, y ha ayudado a poner en valor a la lógica intuicionista para esta ciencia. Sin embargo, a pesar de su incuestionable interés matemático, ella ha pasado más o menos desapercibida para la Filosofía. A fin de remediar este hecho, en esta exposición presentaré la correspondencia desde un punto de vista filosófico, teniendo sobre todo a la vista el debate entre la validez relativa de las lógicas clásica e intuicionista. De esta manera, espero mostrar por qué conocer y comprender este resultado puede ser útil y relevante para la investigación en filosofía de la lógica y de las matemáticas.