Teorema de deducción

Metateorema en lógica matemática

En lógica matemática , un teorema de deducción es un metateorema que justifica hacer demostraciones condicionales a partir de una hipótesis en sistemas que no axiomatizan explícitamente esa hipótesis, es decir, para demostrar 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, por lo general, mucho más cortas de lo que sería posible sin él. En ciertos otros sistemas de demostración formal, la misma conveniencia la proporciona una regla de inferencia explícita; por ejemplo, la deducción natural lo llama introducción de implicación .

En 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 suposiciones , entonces la implicación es deducible a partir de ; en símbolos, implica . En el caso especial donde es el conjunto vacío , la afirmación del teorema de deducción puede escribirse 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, si es 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 consideración, por lo que cada sistema lógico técnicamente necesita su propio teorema de deducción, aunque las diferencias suelen ser menores. ${\displaystyle B}$ ${\displaystyle \Delta \cup \{A\}}$ ${\displaystyle A\to B}$ ${\displaystyle \Delta }$ ${\displaystyle \Delta \cup \{A\}\vdash B}$ ${\displaystyle \Delta \vdash A\to B}$ ${\displaystyle \Delta }$ ${\displaystyle A\vdash B}$ ${\displaystyle \vdash A\to B}$ ${\displaystyle A}$

El teorema de deducción se cumple para todas las teorías de primer orden con los sistemas deductivos ^[2] habituales para la lógica de primer orden. ^[3] Sin embargo, hay sistemas de primer orden en los que se añaden nuevas reglas de inferencia para las que el teorema de deducción falla. ^[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 .

Ejemplos de deducción

1. "Demuestre" el axioma 1: P →( Q → P ) ^[a]

   • 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
2. "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. modo de puesta 3,1
       • R 6. Modus ponens 4,5
     • P → R 7. deducción de 3 a 6
   • ( P → Q )→( P → R ) 8. deducción de 2 a 7

   • ( P →( Q → R ))→(( P → Q )→( P → R )) 9. deducción de 1 a 8 QED
3. Usando el axioma 1 para demostrar (( 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

A partir de los ejemplos, se puede ver que hemos añadido tres reglas de inferencia virtuales (o adicionales y temporales) a nuestra lógica axiomática normal. Estas 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 añade una premisa adicional a las ya existentes. Por lo tanto, si el paso anterior S se dedujo como:

${\displaystyle E_{1},E_{2},...,E_{n-1},E_{n}\vdash S,}$

Luego se agrega otra premisa H y se obtiene:

${\displaystyle E_{1},E_{2},...,E_{n-1},E_{n},H\vdash H.}$

Esto se simboliza pasando del n -ésimo nivel de sangría al n +1-ésimo nivel y diciendo ^[b]

• S paso anterior
  • Hipótesis H

2. La reiteración es un paso en el que se reutiliza un paso anterior. En la práctica, esto solo es necesario cuando se desea 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 a la del paso anterior. Esto se muestra eliminando la sangría de un nivel de la siguiente manera: ^[b]

• Hipótesis H
• ......... (otros pasos)
• C (conclusión extraída de H )

• Deducción H → C

Conversión de prueba mediante el metateorema de deducción a prueba axiomática

En las versiones axiomáticas de la lógica proposicional, normalmente se tienen entre los esquemas axiomáticos (donde P , Q y R se sustituyen por cualquier proposición):

• El axioma 1 es: P →( Q → P )
• El axioma 2 es: ( P →( Q → R ))→(( P → Q )→( P → R ))
• El modus ponens es: de P y P → Q inferimos Q

Estos esquemas axiomáticos se han elegido para que sea fácil derivar de ellos el teorema de deducción, por lo que podría parecer que estamos dando por sentado el problema. Sin embargo, se pueden justificar comprobando que son tautologías mediante tablas de verdad y que el modus ponens preserva la verdad.

A partir de estos esquemas axiomáticos se puede deducir rápidamente el esquema de teorema P → P (reflexividad de implicación), que se utiliza a continuación:

1. ( P →(( Q → P )→ P ))→(( P →( Q → P ))→( P → P )) del esquema de axioma 2 con P , ( Q → P ), P
2. P →(( Q → P )→ P ) del esquema de axioma 1 con P , ( Q → P )
3. ( P →( Q → P ))→( P → P ) del modus ponens aplicado al paso 2 y al paso 1
4. P →( Q → P ) del esquema de axioma 1 con P , Q
5. P → P del modus ponens aplicado al paso 4 y al paso 3

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 han convertido en H → A y H →( A → S ) y luego tomamos el axioma 2, ( H →( A → S ))→(( H → A )→( H → S )), y aplicamos modus ponens para obtener ( H → A )→( H → S ) y luego de nuevo 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 era la conclusión derivada de H .

Para minimizar la complejidad de la prueba resultante, se debe realizar un preprocesamiento antes de la conversión. Todos los pasos (que no sean la conclusión) que no dependan realmente de H deben desplazarse hacia arriba antes del paso de hipótesis y quitarles la sangría un nivel. Y todos los demás pasos innecesarios (que no se utilizan para obtener la conclusión o se pueden omitir), como las reiteraciones que no son la conclusión, deben 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 ).

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 modus ponens para obtener H →( A → S ). No debería ser necesario hacer ambas cosas, a menos que el paso de 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 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 corresponde al combinador S. Nótese que el combinador I corresponde al esquema del teorema P → P .

Teoremas útiles

Si uno pretende convertir una prueba complicada que utiliza el teorema de deducción en una prueba lineal que no utiliza 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:

${\displaystyle A\to A}$

Ayuda a convertir los pasos de la hipótesis.

${\displaystyle (B\to C)\to ((A\to B)\to (A\to C))}$

ayuda a convertir el modus ponens cuando la premisa mayor no depende de la hipótesis, reemplaza el axioma 2 evitando el uso del axioma 1.

${\displaystyle (A\to (B\to C))\to (B\to (A\to C))}$

ayuda a convertir el modus ponens cuando la premisa menor no depende de la hipótesis, reemplaza el axioma 2 evitando el uso del axioma 1.

Estos dos teoremas en conjunto se pueden utilizar en lugar del axioma 2, aunque la prueba convertida sería más complicada:

${\displaystyle (A\to B)\to ((B\to C)\to (A\to C))}$

${\displaystyle (A\to (A\to C))\to (A\to C)}$

La ley de Peirce no es una consecuencia del teorema de deducción, pero puede usarse con éste para demostrar cosas que de otra manera no sería posible demostrar.

${\displaystyle ((A\to B)\to A)\to A}$

También se puede utilizar para obtener el segundo de los dos teoremas, que puede utilizarse en lugar del axioma 2.

Prueba del teorema de deducción

Demostramos el teorema de deducción en un sistema deductivo de cálculo proposicional al estilo de Hilbert. ^[7]

Sea un conjunto de fórmulas y y fórmulas, tales que . Queremos demostrar que . ${\displaystyle \Delta }$ ${\displaystyle A}$ ${\displaystyle B}$ ${\displaystyle \Delta \cup \{A\}\vdash B}$ ${\displaystyle \Delta \vdash A\to B}$

Como , hay una prueba de a partir de . Demostramos 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 hay una prueba de a partir de longitud hasta n , se cumple. ${\displaystyle \Delta \cup \{A\}\vdash B}$ ${\displaystyle B}$ ${\displaystyle \Delta \cup \{A\}}$ ${\displaystyle \Delta }$ ${\displaystyle A}$ ${\displaystyle B}$ ${\displaystyle B}$ ${\displaystyle \Delta \cup \{A\}}$ ${\displaystyle \Delta \vdash A\to B}$

Si n = 1 entonces es miembro del conjunto de fórmulas . Por lo tanto o bien , en cuyo caso es simplemente , que es derivable por sustitución de p → p , que es derivable de los axiomas, y por lo tanto también , o bien es en , en cuyo caso ; se sigue del axioma p → ( q → p ) con sustitución que y por lo tanto por modus ponens que . ${\displaystyle B}$ ${\displaystyle \Delta \cup \{A\}}$ ${\displaystyle B=A}$ ${\displaystyle A\to B}$ ${\displaystyle A\to A}$ ${\displaystyle \Delta \vdash A\to B}$ ${\displaystyle B}$ ${\displaystyle \Delta }$ ${\displaystyle \Delta \vdash B}$ ${\displaystyle \Delta \vdash B\to (A\to B)}$ ${\displaystyle \Delta \vdash A\to B}$

Supongamos ahora la hipótesis de inducción para demostraciones de longitud hasta n , y sea una fórmula demostrable a partir de una demostración de longitud n + 1. Entonces hay dos posibilidades: ${\displaystyle B}$ ${\displaystyle \Delta \cup \{A\}}$

1. ${\displaystyle B}$es miembro del conjunto de fórmulas ; en este caso procedemos como para n = 1. ${\displaystyle \Delta \cup \{A\}}$
2. ${\displaystyle B}$se llega a usando modus ponens. Entonces hay una fórmula C tal que demuestra y , y luego se usa modus ponens para demostrar . Las demostraciones de y son con como máximo 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 . ${\displaystyle \Delta \cup \{A\}}$ ${\displaystyle C}$ ${\displaystyle C\to B}$ ${\displaystyle B}$ ${\displaystyle C}$ ${\displaystyle C\to B}$ ${\displaystyle \Delta \vdash A\to C}$ ${\displaystyle \Delta \vdash A\to (C\to B)}$ ${\displaystyle \Delta \vdash (A\to (C\to B))\to ((A\to C)\to (A\to B))}$ ${\displaystyle \Delta \vdash A\to B}$

Así pues, 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 en la lógica de predicados

El teorema de deducción también es válido en lógica de primer orden en la siguiente forma:

• Si T es una teoría y F , G son fórmulas con F cerrada , y , entonces . ${\displaystyle T\cup \{F\}\vdash G}$ ${\displaystyle T\vdash F\rightarrow G}$

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 del cálculo proposicional. ${\displaystyle \vdash }$

En las versiones más comunes de la noción de prueba formal, existen, además de los esquemas axiomáticos del cálculo proposicional (o el entendimiento de que todas las tautologías del cálculo proposicional deben tomarse como esquemas axiomáticos 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 , inferir ∀ vK ".

Para convertir una prueba de G de T ∪{ F } en 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 mediante el siguiente axioma cuantificador (válido siempre que la variable v no sea libre en la fórmula H ):

• (∀ v ( H → K )) → ( H →∀ vK ).

Como en nuestro caso se supone que F es cerrado, podemos tomar H como F . Este axioma permite deducir F →∀ vK a partir de F → K y 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 puede ser relajada dado que las variables libres en F no han sido variadas en la deducción de G a partir de . En el caso de que una variable libre v en F haya sido variada en la deducción, escribimos (el superíndice en el torniquete indica que v ha sido variada) y la forma correspondiente del teorema de deducción es . ^[8] ${\displaystyle T\cup \{F\}}$ ${\displaystyle T\cup \{F\}\vdash ^{v}G}$ ${\displaystyle T\vdash (\forall vF)\rightarrow G}$

Ejemplo de conversión

Para ilustrar cómo se puede convertir una deducción natural en 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 natural-deductiva 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 →(( 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 pueden resumirse sucintamente utilizando la correspondencia Curry-Howard :

• En primer lugar, en el cálculo lambda, la función f = λa. λb. ba tiene el tipo q → ( q → r ) → r
• En segundo lugar, por eliminación lambda en b, f = λa. si (ka)
• En tercer lugar, por eliminación lambda en a, f = s (k (si)) k

Véase también

• Teorema de eliminación de cortes
• Prueba condicional
• Zurra
• Cálculo proposicional
• Ley de Peirce

Notas

1. Véase la explicación de la Notación § a continuación.
2. se denota con sangría y la conclusión se denota sin sangría ^[5] como se cita en ^[6]

1. Kleene 1967, pág. 39, 112; Shoenfield 1967, pág. 33
2. Por ejemplo, los sistemas deductivos de estilo Hilbert , la deducción natural , el cálculo secuencial , el método de tablas y la resolución (véase Lógica de primer orden ).
3. Se puede encontrar una verificación explícita de este resultado en https://github.com/georgydunaev/VerifiedMathFoundations/blob/master/SHEN.v
4. Kohlenbach 2008, pág. 148
5. Fredric B. Fitch (1952) Lógica simbólica: una introducción
6. Peter Smith (13 de octubre de 2010) Tipos de sistemas de prueba, páginas 5 y siguientes
7. Teorema de deducción, de Curtis Franks de la Universidad de Notre Dame, consultado el 21 de julio de 2020
8. Kleene, Stephen (1980). Introducción a las metamatemáticas . Holanda Septentrional. Págs. 102-106. ISBN. 9780720421033.

Referencias

• Carl Hewitt (2008), "ORGs para computación en la nube escalable, robusta y respetuosa con la privacidad", IEEE Internet Computing , 12 (5): 96–99, doi :10.1109/MIC.2008.107, S2CID  27828219.Septiembre/Octubre 2008
• Kohlenbach, Ulrich (2008), Teoría de la prueba aplicada: interpretaciones de la prueba y su uso en matemáticas , Springer Monographs in Mathematics, Berlín, Nueva York: Springer-Verlag , ISBN 978-3-540-77532-4, Sr.  2445721
• Kleene, Stephen Cole (2002) [1967], Lógica matemática , Nueva York: Dover Publications , ISBN 978-0-486-42533-7, Sr.  1950307
• Rautenberg, Wolfgang (2010), Una introducción concisa a la lógica matemática (3.ª 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 es un tutorial completo. Consulte la Sección 1.5.
• "Teorema de deducción"