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

Converso del teorema de la deducción

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 en los sistemas de deducción natural

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.

Véase también

• Metalógica

Notas y referencias

1. Hunter, Geoffrey (1971). «Sección 26». Metalogic: An Introduction to the Metatheory of Standard First-Order Logic. University of California Press. 

•   Datos: Q1182249