Teorema de la Deducción

Un metateorema que relaciona la demostrabilidad sintáctica con la implicación: si una fórmula B es demostrable a partir de la suposición A (posiblemente junto con otras suposiciones), entonces la implicación A → B es demostrable en el sistema formal circundante, sujeto a condiciones propias del sistema sobre la descarga de supuestos.