La semántica de la teoría de la prueba es un enfoque de la semántica de la lógica que intenta ubicar el significado de las proposiciones y los conectivos lógicos no en términos de interpretaciones , como en los enfoques tarskianos de la semántica, sino en el papel que desempeña la proposición o el conectivo lógico dentro del sistema. de inferencia .
Gerhard Gentzen es el fundador de la semántica de la teoría de la prueba, proporcionando la base formal para ella en su explicación de la eliminación de cortes para el cálculo secuencial , y algunas observaciones filosóficas provocativas sobre la localización del significado de los conectivos lógicos en sus reglas de introducción dentro de la deducción natural . La historia de la semántica de la teoría de la prueba desde entonces se ha dedicado a explorar las consecuencias de estas ideas. [ cita requerida ]
Dag Prawitz extendió la noción de prueba analítica de Gentzen a la deducción natural y sugirió que el valor de una prueba en la deducción natural puede entenderse como su forma normal. [ cita requerida ] Esta idea se encuentra en la base del isomorfismo de Curry-Howard y de la teoría de tipos intuicionistas . Su principio de inversión se encuentra en el corazón de la mayoría de las explicaciones modernas de la semántica de la teoría de la prueba.
Michael Dummett introdujo la idea fundamental de la armonía lógica , basándose en una sugerencia de Nuel Belnap . En resumen, un lenguaje, que se entiende asociado a ciertos patrones de inferencia, tiene armonía lógica si siempre es posible recuperar pruebas analíticas a partir de demostraciones arbitrarias, como se puede demostrar para el cálculo secuencial mediante teoremas de eliminación de cortes y para la deducción natural mediante teoremas de normalización. Un lenguaje que carece de armonía lógica sufrirá la existencia de formas incoherentes de inferencia: probablemente será inconsistente.