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 , 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]- ↑ 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.