Teorema de la deducción

Metateorema en la lógica matemática

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 , entonces A → B es deducible a partir de solamente.[1]​ En símbolos:

  implica  

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

  implica  

En el caso especial donde es el conjunto vacío, el teorema de la deducción dice que:[1]

  implica  

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 editar

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  , entonces B es deducible a partir de  .[1]​ Simbólicamente:

    implica    

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

    si y sólo si    

Y cuando   es el conjunto vacío:

    si y sólo si    

El teorema en los sistemas de deducción natural editar

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:  
Paso Fórmula Razón
1   Supuesto.
2   Desde (1) por introducción de la disyunción.
3   Desde (1) y (2) por introducción de la conjunción.
4   Desde (3) por eliminación de la conjunción.
5   Resumen de (1) hasta (4).
6   Desde (5) por introducción del condicional. Q.E.D.

Véase también editar

Notas y referencias editar

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