Teorema de la deducció

La teorema de la deducció és un metateorema de la llògica proposicional, la llògica de primer orde i uns atres sistemes llògics, que és prou utilisat per a demostrar atres metateoremas. Es tracta d'una formalisació de la tècnica de demostració ordinària segons la qual per a demostrar que des seguix B, n'hi ha prou en supondre A i a partir d'això aplegar a la conclusió de que B.

Més formalment, la teorema establix que si una fòrmula B és deduible (en un sistema deductivo S) a partir del conjunt de fòrmules $\Gamma \cup \{A\}$, llavors A → B és deduible a partir de $\Gamma$ solament. En símbols:

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

O alternativament, en la notació del càlcul de secuentes:

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

En el cas especial a on $\Gamma$ és el conjunt buit, la teorema de la deducció diu que:

$A{⊢}_{S}B$   implica   ${⊢}_{S}A\to B$

La teorema de la deducció sembla haver segut demostrat per primera volta per Alfred Tarski en 1921, pero la primera demostració publicada és de Jacques Herbrand en 1930.

Converso de la teorema de la deducció

A partir de la teorema de la deducció, és fàcil demostrar que si A → B és deduible (en un sistema deductivo S) a partir de $\Gamma$, llavors B és deduible a partir de $\Gamma \cup \{A\}$. Simbòlicament:

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

Açò, junt en la teorema de la deducció, permet establir el metateorema:

$\Gamma \cup \{A\}{⊢}_{S}B$   si i només si   $\Gamma {⊢}_{S}A\to B$

I quan $\Gamma$ és el conjunt buit:

$A{⊢}_{S}B$   si i només si   ${⊢}_{S}A\to B$

La teorema en els sistemes de deducció natural

La teorema de la deducció s'utilisa en els sistemes de deducció natural com a regla d'introducció del condicional material. La regla diu que si suponent A s'aplega a la conclusió de que B, llavors es pot afirmar que A → B, introduint aixina un condicional material. Per eixemple, una demostració que fa us de la regla d'introducció del condicional material podria ser:

Demostrar: $\varphi \to \varphi$
Pas	Fòrmula	Raó
1	$\varphi$	Supòsit.
2	$\varphi \vee \varphi$	Des de (1) per introducció de la disjunció.
3	$(\varphi \vee \varphi )\wedge \varphi$	Des de (1) i (2) per introducció de la conjunció.
4	$\varphi$	Des de (3) per eliminació de la conjunció.
5	$\varphi ⊢\varphi$	Resum de (1) fins a (4).
6	$⊢\varphi \to \varphi$	Des de (5) per introducció del condicional. Q.E.D.

Vore també

• Metalógica