En lógica matemática , un teorema de deducción es un metateorema que justifica hacer pruebas condicionales a partir de una hipótesis en sistemas que no axiomatizan explícitamente esa hipótesis, es decir, para probar una implicación A → B , es suficiente asumir A como hipótesis y luego proceder a derivar B . Los teoremas de deducción existen tanto para la lógica proposicional como para la lógica de primer orden . [1] El teorema de deducción es una herramienta importante en los sistemas de deducción de estilo Hilbert porque permite escribir demostraciones más comprensibles y generalmente mucho más cortas de lo que sería posible sin él. En algunos otros sistemas de prueba formales, la misma conveniencia la proporciona una regla de inferencia explícita; por ejemplo la deducción natural la llama introducción de implicaciones .
Con más detalle, el teorema de deducción de la lógica proposicional establece que si una fórmula es deducible a partir de un conjunto de supuestos, entonces la implicación es deducible de ; en símbolos, implica . En el caso especial donde está el conjunto vacío , la afirmación del teorema de deducción se puede escribir de manera más compacta como: implica . El teorema de deducción para la lógica de predicados es similar, pero viene con algunas restricciones adicionales (que, por ejemplo, se cumplirían si fuera una fórmula cerrada ). En general, un teorema de deducción necesita tener en cuenta todos los detalles lógicos de la teoría bajo consideración, por lo que técnicamente cada sistema lógico necesita su propio teorema de deducción, aunque las diferencias suelen ser menores.
El teorema de deducción es válido para todas las teorías de primer orden con los sistemas deductivos habituales [2] para la lógica de primer orden. [3] Sin embargo, existen sistemas de primer orden en los que se añaden nuevas reglas de inferencia para las cuales falla el teorema de deducción. [4] En particular, el teorema de deducción no se cumple en la lógica cuántica de Birkhoff - von Neumann , porque los subespacios lineales de un espacio de Hilbert forman una red no distributiva .
En los ejemplos, puede ver que hemos agregado tres reglas de inferencia virtuales (o adicionales y temporales) a nuestra lógica axiomática normal. Se trata de "hipótesis", "reiteración" y "deducción". Las reglas normales de inferencia (es decir, el "modus ponens" y los diversos axiomas) siguen estando disponibles.
1. La hipótesis es un paso en el que se añade una premisa adicional a las ya disponibles. Entonces, si su paso anterior S se dedujo como:
luego se suma otra premisa H y se obtiene:
Esto se simboliza pasando del nivel n -ésimo de sangría al nivel n +1 y diciendo [b]
2. La reiteración es un paso en el que se reutiliza un paso anterior. En la práctica, esto sólo es necesario cuando se quiere tomar una hipótesis que no es la más reciente y utilizarla como paso final antes de un paso de deducción.
3. La deducción es un paso en el que se elimina la hipótesis más reciente (aún disponible) y se antepone al paso anterior. Esto se muestra eliminando la sangría de un nivel de la siguiente manera: [b]
En las versiones axiomáticas de la lógica proposicional, uno suele tener entre los esquemas de axiomas (donde P , Q y R se reemplazan por cualquier proposición):
Estos esquemas de axiomas se eligen para permitir derivar fácilmente el teorema de deducción a partir de ellos. Así que podría parecer que estamos dando una petición de principio. Sin embargo, pueden justificarse comprobando que son tautologías que utilizan tablas de verdad y que el modus ponens preserva la verdad.
A partir de estos esquemas de axiomas se puede deducir rápidamente el esquema del teorema P → P (reflexividad de la implicación), que se utiliza a continuación:
Supongamos que tenemos que Γ y H juntos prueban C , y queremos demostrar que Γ prueba H → C. Para cada paso S en la deducción que es una premisa en Γ (un paso de reiteración) o un axioma, podemos aplicar modus ponens al axioma 1, S → ( H → S ), para obtener H → S. Si el paso es H en sí (un paso de hipótesis), aplicamos el esquema del teorema para obtener H → H. Si el paso es el resultado de aplicar modus ponens a A y A → S , primero nos aseguramos de que estos se hayan convertido a H → A y H →( A → S ) y luego tomamos el axioma 2, ( H →( A → S ))→(( H → A )→( H → S )), y aplique modus ponens para obtener ( H → A )→( H → S ) y luego nuevamente para obtener H → S . Al final de la prueba tendremos H → C como se requiere, excepto que ahora solo depende de Γ, no de H. Entonces el paso de deducción desaparecerá, consolidado en el paso anterior que fue la conclusión derivada de H.
Para minimizar la complejidad de la prueba resultante, se debe realizar algún procesamiento previo antes de la conversión. Cualquier paso (aparte de la conclusión) que en realidad no dependa de H debe moverse hacia arriba antes del paso de hipótesis y quitarle la sangría un nivel. Y se deben eliminar cualquier otro paso innecesario (que no se utiliza para llegar a la conclusión o que puede omitirse), como las reiteraciones que no son la conclusión.
Durante la conversión, puede resultar útil poner todas las aplicaciones del modus ponens al axioma 1 al comienzo de la deducción (justo después del paso H → H ).
Al convertir un modus ponens, si A está fuera del alcance de H , entonces será necesario aplicar el axioma 1, A →( H → A ) y modus ponens para obtener H → A. De manera similar, si A → S está fuera del alcance de H , aplique el axioma 1, ( A → S ) → ( H → ( A → S )) y el modus ponens para obtener H → ( A → S ). No debería ser necesario hacer ambas cosas, a menos que el paso del modus ponens sea la conclusión, porque si ambos están fuera del alcance, entonces el modus ponens debería haberse movido hacia arriba antes de H y, por lo tanto, también estar fuera del alcance.
Según la correspondencia Curry-Howard , el proceso de conversión anterior para el metateorema de deducción es análogo al proceso de conversión de términos del cálculo lambda a términos de lógica combinatoria , donde el axioma 1 corresponde al combinador K y el axioma 2 corresponde al combinador S . Tenga en cuenta que el combinador I corresponde al esquema del teorema P → P .
Si uno pretende convertir una prueba complicada usando el teorema de deducción en una prueba lineal sin usar el teorema de deducción, entonces probablemente sería útil demostrar estos teoremas de una vez por todas al principio y luego usarlos para ayudar con la conversión. :
ayuda a convertir los pasos de la hipótesis.
ayuda a convertir el modus ponens cuando la premisa mayor no depende de la hipótesis, reemplaza el axioma 2 y evita el uso del axioma 1.
ayuda a convertir el modus ponens cuando la premisa menor no depende de la hipótesis, reemplaza el axioma 2 y evita el uso del axioma 1.
Estos dos teoremas juntos pueden usarse en lugar del axioma 2, aunque la demostración convertida sería más complicada:
La ley de Peirce no es una consecuencia del teorema de deducción, pero puede usarse con el teorema de deducción para demostrar cosas que de otro modo no sería posible demostrar.
También se puede utilizar para obtener el segundo de los dos teoremas, que se puede utilizar en lugar del axioma 2.
Demostramos el teorema de deducción en un sistema deductivo de cálculo proposicional estilo Hilbert. [7]
Sea un conjunto de fórmulas yy fórmulas , tales que . Queremos demostrarlo .
Desde entonces , hay una prueba de from . Probamos el teorema por inducción sobre la longitud de prueba n ; por lo tanto, la hipótesis de inducción es que para cualquier , y tal que haya una prueba de desde de longitud hasta n , se cumple.
Si n = 1 entonces es miembro del conjunto de fórmulas . Así , ya sea, en cuyo caso es simplemente , que es derivable por sustitución de p → p , que es derivable de los axiomas, y por tanto también , o está en , en cuyo caso ; se sigue del axioma p → ( q → p ) con sustitución que y por tanto por modus ponens que .
Ahora supongamos la hipótesis de inducción para pruebas de longitud hasta n , y sea una fórmula demostrable a partir de una prueba de longitud n +1. Entonces hay dos posibilidades:
Así, en todos los casos el teorema se cumple también para n +1, y por inducción se demuestra el teorema de deducción.
El teorema de deducción también es válido en lógica de primer orden de la siguiente forma:
Aquí, el símbolo significa "es una consecuencia sintáctica de". A continuación indicamos en qué se diferencia la demostración de este teorema de deducción de la del teorema de deducción en cálculo proposicional.
En las versiones más comunes de la noción de prueba formal, existen, además de los esquemas de axiomas del cálculo proposicional (o la comprensión de que todas las tautologías del cálculo proposicional deben tomarse como esquemas de axiomas por derecho propio), axiomas cuantificadores . y además del modus ponens , una regla adicional de inferencia , conocida como regla de generalización : "A partir de K , infiere ∀ vK ".
Para convertir una prueba de G de T ∪{ F } a una de F → G de T , se tratan pasos de la prueba de G que son axiomas o resultan de la aplicación de modus ponens de la misma manera que para las pruebas en Lógica proposicional. Los pasos que resultan de la aplicación de la regla de generalización se tratan mediante el siguiente axioma cuantificador (válido siempre que la variable v no esté libre en la fórmula H ):
Como en nuestro caso se supone que F es cerrado, podemos considerar que H es F. Este axioma permite deducir F →∀ vK a partir de F → K y la generalización, que es justo lo que se necesita siempre que se aplica la regla de generalización a algún K en la prueba de G.
En lógica de primer orden, la restricción de que F sea una fórmula cerrada se puede relajar dado que las variables libres en F no han variado en la deducción de G de . En el caso de que una variable libre v en F haya variado en la deducción, escribimos (el superíndice en el torniquete indica que v ha variado) y la forma correspondiente del teorema de deducción es . [8]
Para ilustrar cómo se puede convertir una deducción natural a la forma axiomática de prueba, la aplicamos a la tautología Q →(( Q → R )→ R ). En la práctica, suele ser suficiente saber que podemos hacer esto. Normalmente utilizamos la forma deductiva natural en lugar de la prueba axiomática, mucho más larga.
Primero, escribimos una prueba usando un método similar a la deducción natural:
En segundo lugar, convertimos la deducción interna en una prueba axiomática:
En tercer lugar, convertimos la deducción externa en una prueba axiomática:
Estos tres pasos se pueden enunciar de manera sucinta utilizando la correspondencia Curry-Howard :
