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.^[1]​ 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 ${\displaystyle \Gamma \cup \{A\}}$, entonces A → B es deducible a partir de ${\displaystyle \Gamma }$ solamente.^[1]​ En símbolos:

${\displaystyle \Gamma \cup \{A\}\vdash _{S}B}$   implica   ${\displaystyle \Gamma \vdash _{S}A\to B}$

O alternativamente, en la notación del cálculo de secuentes:

${\displaystyle \Gamma ,A\vdash _{S}B}$   implica   ${\displaystyle \Gamma \vdash _{S}A\to B}$

En el caso especial donde ${\displaystyle \Gamma }$ es el conjunto vacío, el teorema de la deducción dice que:^[1]​

${\displaystyle A\vdash _{S}B}$   implica   ${\displaystyle \vdash _{S}A\to B}$

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]​

A partir del teorema de la deducción, es fácil demostrar que si A → B es deducible (en un sistema deductivo S) a partir de ${\displaystyle \Gamma }$, entonces B es deducible a partir de ${\displaystyle \Gamma \cup \{A\}}$.^[1]​ Simbólicamente:

${\displaystyle \Gamma \vdash _{S}A\to B}$   implica   ${\displaystyle \Gamma \cup \{A\}\vdash _{S}B}$

Esto, junto con el teorema de la deducción, permite establecer el metateorema:^[1]​

${\displaystyle \Gamma \cup \{A\}\vdash _{S}B}$   si y sólo si   ${\displaystyle \Gamma \vdash _{S}A\to B}$

Y cuando ${\displaystyle \Gamma }$ es el conjunto vacío:

${\displaystyle A\vdash _{S}B}$   si y sólo si   ${\displaystyle \vdash _{S}A\to B}$

El teorema de la deducción se utiliza en los sistemas de deducción natural como regla de introducción del condicional material. 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. Por ejemplo, una demostración que hace uso de la regla de introducción del condicional material podría ser:

Demostrar: ${\displaystyle \phi \to \phi \,}$
Paso	Fórmula	Razón
1	${\displaystyle \phi \,}$	Supuesto.
2	${\displaystyle \phi \lor \phi }$	Desde (1) por introducción de la disyunción.
3	${\displaystyle (\phi \lor \phi )\land \phi }$	Desde (1) y (2) por introducción de la conjunción.
4	${\displaystyle \phi \,}$	Desde (3) por eliminación de la conjunción.
5	${\displaystyle \phi \vdash \phi }$	Resumen de (1) hasta (4).
6	${\displaystyle \vdash \phi \to \phi }$	Desde (5) por introducción del condicional. Q.E.D.

• Metalógica