Teorema de la deducción

El teorema de la deducción es un metateorema de la lógica proposicional, la lógica de primer orden y otros sistemas lógicos, que es bastante utilizado para demostrar otros metateoremas.​ Se trata de una formalización de la técnica de demostración ordinaria según la cual para demostrar que de A se sigue B, basta con suponer A y a partir de ello llegar a la conclusión de que B. Más formalmente, el teorema establece que si una fórmula B es deducible (en un sistema deductivo S) a partir del conjunto de fórmulas , entonces A → B es deducible a partir de solamente.​ En símbolos: implica O alternativamente, en la notación del cálculo de secuentes: implica En el caso especial donde es el conjunto vacío, el teorema de la deducción dice que:​ implica El teorema de la deducción parece haber sido demostrado por primera vez por Alfred Tarski en 1921, pero la primera demostración publicada es de Jacques Herbrand en 1930.​