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
[1] En símbolos: O alternativamente, en la notación del cálculo de secuentes: En el caso especial donde
es el conjunto vacío, el teorema de la deducción dice que:[1] 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.
[1] Simbólicamente: Esto, junto con el teorema de la deducción, permite establecer el metateorema:[1] Y cuando
La regla dice que si suponiendo A se llega a la conclusión de que B, entonces se puede afirmar que A → B, introduciendo así un condicional material.