## [Teorema de la Deducción](/es/node/59998) Definició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. ## Principio Principio Interiorización del razonamiento condicional: las pruebas que usan una suposición temporal pueden convertirse en pruebas de una proposición condicional al descargar esa suposición, reflejando así la consecuencia metateórica como una implicación a nivel objeto. ## Demostración Demostración En lógica proposicional, si al suponer P se deriva Q mediante una prueba finita, entonces puede construirse una prueba de P → Q sin suponer P; por ejemplo, un sub-razonamiento que parte de «Supongamos P» y concluye Q da el teorema «P implica Q». ## Aplicación incorrecta Aplicación incorrecta Aplicar el teorema de la deducción en sistemas donde falla o requiere restricciones (p. ej., ciertas lógicas modales, sistemas con supuestos globales no descargables, o contextos donde las reglas de inferencia impiden la descarga), conduciendo a implicaciones a nivel objeto inválidas. ## Consecuencia Consecuencia Permite la construcción modular de pruebas, la formación de teoremas a partir de razonamientos condicionales y la mecanización de pruebas basadas en hipótesis; posibilita el paso entre derivaciones hipotéticas y teoremas incondicionales. ## Inversión Inversión La inversa —si A → B es demostrable entonces B es demostrable a partir de A— no se deduce del teorema mismo; derivar B desde A todavía requiere que A sea supuesto o demostrable de forma independiente, normalmente aplicando modus ponens en el sistema. ## Límite Límite Se cumple en muchos sistemas estándar como las lógicas proposicional y de primer orden clásicas e intuicionistas con las reglas habituales de introducción/ eliminación de la implicación, pero falla o necesita modificación en ciertas lógicas modales, subestructurales o de relevancia y en sistemas con restricciones de inferencia especiales. ## Tensión semántica Tensión semántica Surge tensión entre la transformabilidad sintáctica garantizada por el teorema de la deducción y la consecuencia semántica: la demostrabilidad desde una suposición es una noción sintáctica sensible a las reglas de prueba, mientras que la implicación semántica puede mantenerse incluso cuando el teorema de la deducción no es aplicable en un cálculo dado. ## Síntesis Síntesis El Teorema De La Deducción conecta el nivel meta de asumir hipótesis para derivar conclusiones con la representación a nivel objeto de esa relación como implicación; facilita el desarrollo de pruebas cuando la descarga de supuestos está permitida, pero su aplicación exige atención a las provisiones específicas del sistema.