En lógica matemática , un teorema de deducción es un metateorema que justifica hacer pruebas condicionales - para probar una implicación A → B , asumir A como una hipótesis y luego proceder a derivar B - en sistemas que no tienen una regla de inferencia explícita para esto. Existen teoremas deducción por tanto la lógica proposicional y lógica de primer orden . [1] El teorema de la deducción es una herramienta importante en los sistemas de deducción al estilo de Hilbert.porque permite escribir pruebas más comprensibles y, por lo general, mucho más breves de lo que sería posible sin él. En algunos otros sistemas formales de prueba, la misma conveniencia la proporciona una regla de inferencia explícita; por ejemplo, la deducción natural lo llama introducción de implicación .
Más detalladamente, el teorema de la deducción lógica proposicional establece que si una fórmula es deducible de un conjunto de supuestos entonces la implicación es deducible de ; en simbolos, implica . En el caso especial dondees 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 se cumplirían, por ejemplo, sies una fórmula cerrada ). En general, un teorema de deducción debe tener en cuenta todos los detalles lógicos de la teoría en cuestión, por lo que cada sistema lógico necesita técnicamente su propio teorema de deducción, aunque las diferencias suelen ser menores.
El teorema de la 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 agregan nuevas reglas de inferencia para las que falla el teorema de deducción. [4] Más notablemente, 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 .
Ejemplos de deducción
- "Demuestre" el axioma 1:
- P 1. hipótesis
- Q 2. hipótesis
- P 3. reiteración de 1
- Q → P 4. deducción de 2 a 3
- P → ( Q → P ) 5. deducción de 1 a 4 QED
- "Demuestre" el axioma 2:
- P → ( Q → R ) 1. hipótesis
- P → Q 2. hipótesis
- P 3. hipótesis
- Q 4. modus ponens 3,2
- Q → R 5. modus ponens 3,1
- R 6. modus ponens 4,5
- P → R 7. deducción de 3 a 6
- P → Q 2. hipótesis
- ( P → Q ) → ( P → R ) 8. deducción de 2 a 7
- P → ( Q → R ) 1. hipótesis
- ( P → ( Q → R )) → (( P → Q ) → ( P → R )) 9. deducción de 1 a 8 QED
- Usando el axioma 1 para mostrar (( P → ( Q → P )) → R ) → R :
- ( P → ( Q → P )) → R 1. hipótesis
- P → ( Q → P ) 2. axioma 1
- R 3. modus ponens 2,1
- (( P → ( Q → P )) → R ) → R 4. deducción de 1 a 3 QED
Reglas virtuales de inferencia
En los ejemplos, puede ver que hemos agregado tres reglas de inferencia virtuales (o extra y temporales) a nuestra lógica axiomática normal. Estos son "hipótesis", "reiteración" y "deducción". Las reglas normales de inferencia (es decir, "modus ponens" y los diversos axiomas) siguen estando disponibles.
1. La hipótesis es un paso en el que se agrega una premisa adicional a las ya disponibles. Entonces, si su paso anterior S se dedujo como:
luego se agrega otra premisa H y se obtiene:
Esto se simboliza moviéndose del n-ésimo nivel de sangría al n + 1-ésimo nivel y diciendo
- S paso anterior
- Hipótesis H
- S paso anterior
2. La repetición es un paso en el que se reutiliza un paso anterior. En la práctica, esto solo es necesario cuando se quiere tomar una hipótesis que no es la hipótesis más reciente y usarla como el paso final antes de un paso de deducción.
3. La deducción es un paso en el que uno elimina la hipótesis más reciente (aún disponible) y la antepone al paso anterior. Esto se muestra quitando la sangría de un nivel de la siguiente manera:
- Hipótesis H
- ......... (otros pasos)
- C (conclusión extraída de H )
- Deducción H → C
Conversión de prueba usando el metateorema de deducción a prueba axiomática
En las versiones axiomáticas de la lógica proposicional, uno generalmente tiene entre los esquemas de axioma (donde P , Q y R se reemplazan por cualquier proposición):
- El axioma 1 es: P → ( Q → P )
- El axioma 2 es: ( P → ( Q → R )) → (( P → Q ) → ( P → R ))
- Modus ponens es: de P y P → Q inferir Q
Estos esquemas de axiomas se eligen para que uno pueda derivar fácilmente el teorema de deducción de ellos. Así que podría parecer que estamos planteando la pregunta. Sin embargo, se pueden justificar comprobando que son tautologías utilizando tablas de verdad y que modus ponens conserva la verdad.
A partir de estos esquemas de axiomas, se puede deducir rápidamente el esquema del teorema P → P (reflexividad de implicación) que se utiliza a continuación:
- ( P → (( Q → P ) → P )) → (( P → ( Q → P )) → ( P → P )) del esquema del axioma 2 con P , ( Q → P ), P
- P → (( Q → P ) → P ) del esquema de axioma 1 con P , ( Q → P )
- ( P → ( Q → P )) → ( P → P ) del modus ponens aplicado al paso 2 y al paso 1
- P → ( Q → P ) del esquema de axioma 1 con P , Q
- P → P del modus ponens aplicado al paso 4 y al paso 3
Supongamos que tenemos que Γ y H demuestran C , y queremos demostrar que Γ demuestra H → C . Para cada paso de S en la deducción que es una premisa en Γ (un paso reiteración) o un axioma, podemos aplicar modus ponens con el axioma 1, S → ( H → S ), para obtener H → S . Si el paso es H en sí (un paso hipótesis), aplicamos el teorema de esquema 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 aplicar modus ponens para obtener ( H → a ) → ( H → S ) y luego de nuevo para obtener H → S . Al final de la prueba tendremos H → C según sea necesario, excepto que ahora sólo depende de Γ, no en H . Por lo que el paso de la 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 un procesamiento previo antes de la conversión. Cualquier paso (que no sea la conclusión) que en realidad no dependa de H debe moverse hacia arriba antes del paso de hipótesis y sin sangría un nivel. Y cualquier otro paso innecesario (que no se utiliza para llegar a la conclusión o que se puede omitir), como las reiteraciones que no son la conclusión, debe eliminarse.
Durante la conversión, puede ser útil poner todas las aplicaciones del modus ponens al axioma 1 al comienzo de la deducción (justo después del paso H → H ).
Cuando se convierte un modus ponens, si A está fuera del alcance de H , entonces será necesario aplicar axioma 1, A → ( H → A ponens), y el modus 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 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ía fuera del alcance.
Según la correspondencia de 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 de cálculo lambda a términos de lógica combinatoria , donde el axioma 1 corresponde al combinador K y el axioma 2 al combinador S . Tenga en cuenta que los que combinator corresponde al esquema teorema P → P .
Teoremas útiles
Si uno tiene la intención de convertir una demostración complicada usando el teorema de deducción en una prueba de línea recta sin usar el teorema de deducción, entonces probablemente sería útil probar 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 principal 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 se pueden usar 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 la deducción, pero puede usarse con el teorema de la deducción para probar cosas que de otro modo no se podrían probar.
También se puede usar para obtener el segundo de los dos teoremas que se pueden usar en lugar del axioma 2.
Prueba del teorema de la deducción
Demostramos el teorema de la deducción en un sistema deductivo de cálculo proposicional al estilo de Hilbert. [5]
Dejar ser un conjunto de fórmulas y y fórmulas, tales que . Queremos demostrar que.
Desde , hay una prueba de de . Demostramos el teorema por inducción sobre la longitud de prueba n ; por tanto, la hipótesis de inducción es que para cualquier, y tal que hay una prueba de de de longitud hasta n , sostiene.
Si n = 1 entonces es miembro del conjunto de fórmulas . Por lo tanto, ya sea, en ese caso es simple que es derivable por sustitución de p → p que es derivable de los axiomas, por lo tanto también ; o es en , en ese caso ; se sigue del axioma p → (q → p) con sustitución que y por lo tanto por modus ponens que .
Supongamos ahora la hipótesis de inducción para pruebas de longitud hasta n , y supongamos ser una fórmula demostrable de con prueba de longitud n +1. Entonces hay tres posibilidades:
- es miembro del conjunto de fórmulas ; en este caso procedemos como para n = 0.
- se llega mediante una sustitución en una fórmula φ. Entonces φ se prueba a partir decon un máximo de n pasos, por lo tanto, según la hipótesis de inducción, donde podemos escribir A y φ con diferentes variables. Pero entonces podemos llegar de a por la misma sustitución que se utiliza para derivar de φ; por lo tanto.
- se llega usando modus ponens. Entonces hay una fórmula C tal que prueba y , y luego se usa modus ponens para demostrar . Las pruebas de y están con un máximo de n pasos, y por la hipótesis de inducción tenemos y . Por el axioma (p → (q → r)) → ((p → q) → (p → r)) con sustitución se sigue que, y al usar modus ponens dos veces tenemos .
Así, en todos los casos, el teorema es válido también para n +1, y por inducción se demuestra el teorema de la deducción.
El teorema de la deducción en la lógica de predicados
El teorema de la deducción también es válido en lógica de primer orden en 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 el 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 el entendimiento 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 la regla de generalización : "De K , infiere ∀ vK ".
Para convertir una prueba de G de T ∪ { F } a una de F → G de T , se tratan los pasos de la prueba de G que son axiomas o resultan de la aplicación del 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 a través del siguiente axioma cuantificador (válido siempre que la variable v no esté libre en la fórmula H ):
- (∀ v ( H → K )) → ( H → ∀ vK ).
Dado que en nuestro caso F se supone que está cerrada, podemos tomar H siendo F . Este axioma permite deducir F → ∀ vK de F → K y generalización, que es justo lo que se necesita cada vez que se aplica la regla de generalización a algunos 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 se han variado en la deducción de G de . En el caso de que una variable libre v en F se haya variado en la deducción, escribimos (el superíndice en el torniquete indica que v se ha variado) y la forma correspondiente del teorema de deducción es . [6]
Ejemplo de conversión
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 usamos 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:
- Q 1. hipótesis
- Q → R 2. hipótesis
- R 3. modus ponens 1,2
- ( Q → R ) → R 4. deducción de 2 a 3
- Q 1. hipótesis
- Q → (( Q → R ) → R ) 5. deducción de 1 a 4 QED
En segundo lugar, convertimos la deducción interna en una prueba axiomática:
- ( Q → R ) → ( Q → R ) 1. esquema del teorema ( A → A )
- (( Q → R ) → ( Q → R )) → ((( Q → R ) → Q ) → (( Q → R ) → R )) 2. axioma 2
- (( Q → R ) → Q ) → (( Q → R ) → R ) 3. modus ponens 1,2
- Q → (( Q → R ) → Q ) 4. axioma 1
- Q 5. hipótesis
- ( Q → R ) → Q 6. modus ponens 5,4
- ( Q → R ) → R 7. modus ponens 6,3
- Q → (( Q → R ) → R ) 8. deducción de 5 a 7 QED
En tercer lugar, convertimos la deducción externa en una prueba axiomática:
- ( Q → R ) → ( Q → R ) 1. esquema del teorema ( A → A )
- (( Q → R ) → ( Q → R )) → ((( Q → R ) → Q ) → (( Q → R ) → R )) 2. axioma 2
- (( Q → R ) → Q ) → (( Q → R ) → R ) 3. modus ponens 1,2
- Q → (( Q → R ) → Q ) 4. axioma 1
- [(( Q → R ) → Q ) → (( Q → R ) → R )] → [ Q → ((( Q → R ) → Q ) → (( Q → R ) → R ))] 5. axioma 1
- Q → ((( Q → R ) → Q ) → (( Q → R ) → R )) 6. modus ponens 3,5
- [ Q → ((( Q → R ) → Q ) → (( Q → R ) → R ))] → ([ Q → (( Q → R ) → Q )] → [ Q → (( Q → R ) → R ))]) 7. axioma 2
- [ Q → (( Q → R ) → Q )] → [ Q → (( Q → R ) → R ))] 8. modus ponens 6,7
- Q → (( Q → R ) → R )) 9. modus ponens 4,8 QED
Estos tres pasos se pueden enunciar de manera sucinta utilizando la correspondencia Curry-Howard :
- primero, en el cálculo lambda, la función f = λa. λb. ba tiene tipo q → ( q → r ) → r
- segundo, por eliminación lambda en b, f = λa. si (ka)
- tercero, por eliminación lambda en a, f = s (k (si)) k
Ver también
Notas
- ^ Kleene 1967, p. 39, 112; Shoenfield 1967, pág. 33
- ^ Por ejemplo, los sistemas deductivos al estilo de Hilbert , la deducción natural , el cálculo secuencial , el método de cuadros y la resolución —ver Lógica de primer orden
- ^ Se puede encontrar una verificación explícita de este resultado en https://github.com/georgydunaev/VerifiedMathFoundations/blob/master/SHEN.v
- ^ Kohlenbach, 2008, p. 148
- ^ Teorema de deducción, de Curtis Franks en la Universidad de Notre Dame , consultado el 21 de julio de 2020
- ^ Kleene, Stephen (1980). Introducción a las metamatemáticas . Holanda Septentrional. págs. 102-106. ISBN 9780720421033.
Referencias
- Carl Hewitt (2008), "ORG para una computación en la nube de cliente escalable, robusta y amigable con la privacidad", IEEE Internet Computing , 12 (5): 96–99, doi : 10.1109 / MIC.2008.107 . Septiembre / Octubre de 2008
- Kohlenbach, Ulrich (2008), Teoría de prueba aplicada: interpretaciones de prueba y su uso en matemáticas , Springer Monographs in Mathematics, Berlín, Nueva York: Springer-Verlag , ISBN 978-3-540-77532-4, MR 2445721
- Kleene, Stephen Cole (2002) [1967], lógica matemática , Nueva York: Dover Publications , ISBN 978-0-486-42533-7, Señor 1950307
- Rautenberg, Wolfgang (2010), A Concise Introduction to Mathematical Logic (3.a ed.), Nueva York : Springer Science + Business Media , doi : 10.1007 / 978-1-4419-1221-3 , ISBN 978-1-4419-1220-6.
- Shoenfield, Joseph R. (2001) [1967], Lógica matemática (2ª ed.), AK Peters , ISBN 978-1-56881-135-2
enlaces externos
- Introducción a la lógica matemática de Vilnis Detlovs y Karlis Podnieks Podnieks es un tutorial completo. Consulte la Sección 1.5.
- "Teorema de la deducción"