Teorema de deducción

format_list_bulleted Contenido keyboard_arrow_down

ImprimirCitar

Metateorema en la lógica matemática

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, basta con 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. 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.

En más detalle, el teorema de deducción lógica proposicional declara que si una fórmula $B$ es deducible de un conjunto de hipótesis $Delta cup {A}$ entonces la implicación ${displaystyle Ato B}$ es deducible de $Delta$ ; en símbolos, $Delta cup {A}vdash B$ implicación ${displaystyle Delta vdash Ato B}$ . En el caso especial $Delta$ es el conjunto vacío, la reclamación de teorema de deducción puede ser más compactamente escrito como: $Avdash B$ implicación $vdash Ato B$ . El teorema de deducción para la lógica predicada es similar, pero viene con algunas restricciones adicionales (que por ejemplo estaría satisfecho si $A$ es una fórmula cerrada). En general, un teorema de deducción tiene que tener en cuenta todos los detalles lógicos de la teoría bajo consideración, por lo que cada sistema lógico necesita técnicamente su propio teorema de deducción, aunque las diferencias son generalmente menores.

El teorema de deducción es válido para todas las teorías de primer orden con los sistemas deductivos habituales de la lógica de primer orden. Sin embargo, existen sistemas de primer orden en los que se añaden nuevas reglas de inferencia en las que el teorema de deducción falla. 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

"Probar" axioma 1: P→Q→P)
- 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
"Prove" 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)→(P→R) 8. deducción de 2 a 7
()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 ponente 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 adicionales 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, 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 que ya están disponibles. Entonces, si su paso anterior S se dedujo como:

E_{1},E_{2},...,E_{{n-1}},E_{n}vdash S,

luego se agrega otra premisa H y se obtiene:

E_{1},E_{2},...,E_{{n-1}},E_{n},Hvdash H.

Esto se simboliza moviéndose desde el nivel n de sangría al nivel n+1 y diciendo

S paso anterior
- H hipótesis

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:

H hipótesis
......
C (conclusión extraída H)

H→C deducción

Conversión de prueba utilizando 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 axiomas (donde P, Q y R se reemplazan por cualquier proposiciones):

Axiom 1 es: P→Q→P)
Axiom 2 es:P→Q→R)→(P→Q)→(P→R)
Modus ponens es: P y P→Q inferente Q

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:

()P→(Q→P)→P)→(P→Q→P)→(P→P) de axiom schema 2 con P, (Q→P), P
P→(Q→P)→P) de axiom esquema 1 con P, (Q→P)
()P→Q→P)→(P→P) del modus ponente aplicado al paso 2 y paso 1
P→Q→P) de axiom esquema 1 con P, Q
P→P del modus ponente 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 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 preprocesamiento 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 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 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, estar fuera del alcance. el alcance también.

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 a el combinador S. Tenga en cuenta que el combinador I corresponde al esquema del teorema P→P.

Teoremas útiles

Si uno tiene la intención de 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 como ayuda. con la conversión:

Ato A

ayuda a convertir los pasos de la hipótesis.

{displaystyle (Bto C)to ((Ato B)to (Ato C))}

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.

{displaystyle (Ato (Bto C))to (Bto (Ato C))}

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:

{displaystyle (Ato B)to ((Bto C)to (Ato C))}

{displaystyle (Ato (Ato C))to (Ato C)}

Did you mean:

Peirce 's law is not a consequence of the deduction theorem, but it can be used with the deduction theorem to prove things that one might not otherwise be able to prove.

{displaystyle ((Ato B)to A)to A}

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

Demostración del teorema de la deducción

Demostramos el teorema de deducción en un sistema deductivo de cálculo proposicional estilo Hilbert.

Vamos $Delta$ ser un conjunto de fórmulas y $A$ y $B$ fórmulas, tal que $Delta cup {A}vdash B$ . Queremos probarlo. ${displaystyle Delta vdash Ato B}$ .

Desde $Delta cup {A}vdash B$ , hay una prueba de $B$ desde $Delta cup {A}$ . Probamos el teorema por inducción en la longitud de la prueba n; por lo tanto la hipótesis de inducción es que para cualquier $Delta$ , $A$ y $B$ tal que hay una prueba de $B$ desde $Delta cup {A}$ de longitud hasta n, ${displaystyle Delta vdash Ato B}$ sostiene.

Si n = 1 entonces $B$ es miembro del conjunto de fórmulas $Delta cup {A}$ . Así o ${displaystyle B=A}$ , en cuyo caso ${displaystyle Ato B}$ es simplemente ${displaystyle Ato A}$ , que es derivable por sustitución de p → p, que es derivable de los axiomas, y por lo tanto también ${displaystyle Delta vdash Ato B}$ , o $B$ está dentro $Delta$ , en cuyo caso ${displaystyle Delta vdash B}$ ; sigue del axioma p →q → p) con sustitución que ${displaystyle Delta vdash Bto (Ato B)}$ y por lo tanto por modus ponente que ${displaystyle Delta vdash Ato B}$ .

Ahora asumamos la hipótesis de inducción para pruebas de longitud hasta n, y dejar $B$ ser una fórmula provable $Delta cup {A}$ con una prueba de longitud n+1. Luego hay dos posibilidades:

$B$ es miembro del conjunto de fórmulas $Delta cup {A}$ ; en este caso procedemos en n= 1.
$B$ se llega utilizando modus ponens. Entonces hay una fórmula C tales que $Delta cup {A}$ prueba $C$ y ${displaystyle Cto B}$ , y modus ponente se utiliza para probar $B$ . Las pruebas de $C$ y ${displaystyle Cto B}$ están con n pasos, y por la hipótesis de inducción tenemos ${displaystyle Delta vdash Ato C}$ y ${displaystyle Delta vdash Ato (Cto B)}$ . Por el axiomap →q → r) → (p → q) →p → r)) con sustitución sigue que ${displaystyle Delta vdash (Ato (Cto B))to ((Ato C)to (Ato B))}$ , y usando modus ponentes dos veces tenemos ${displaystyle Delta vdash Ato B}$ .

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 la deducción en 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 cerrado, y ${displaystyle Tcup {F}vdash G}$ , entonces ${displaystyle Tvdash Frightarrow G}$ .

Aquí, el símbolo $vdash$ significa "es una consecuencia sintáctica de". Indicamos a continuación cómo la prueba de este teorema de deducción difiere de la del teorema de deducción en cálculo proposición.

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 ser tomados como esquemas de axiomas por derecho propio), axiomas cuantificadores y, además del modus ponens, una regla de inferencia adicional, conocida como regla de generalización: "De K, inferir ∀ vK."

Para convertir una prueba de G de T∪{F} a una de F→ G de T, uno reparte con pasos de la prueba de G que son axiomas o resultan de la aplicación del modus ponens en el de la misma manera que para las pruebas en lógica proposicional. Pasos que resultan de la aplicación de la regla de La generalización se trata mediante el siguiente axioma cuantificador (válido siempre que la variable v no está libre en la fórmula H):

(Firmado)v()H→K)→(H→vK).

Dado que en nuestro caso se supone que F es cerrado, podemos tomar H como F. Este axioma permite uno para deducir F→∀vK de F→K y la generalización, que es justo lo que se necesita siempre que la regla de generalización se aplica a algún K en la prueba de G.

En la 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 ha sido variada en la deducción de G de ${displaystyle Tcup {F}}$ . En el caso de que una variable libre v en F ha sido variada en la deducción, escribimos ${displaystyle Tcup {F}vdash ^{v}G}$ (el superscripto en el torntil indicando que v ha sido variado) y la forma correspondiente del teorema de deducción es ${displaystyle Tvdash (forall vF)rightarrow G}$ .

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 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:

Q 1. hipótesis
- Q→R 2. hipótesis
- R 3. modus ponente 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. theorem schemaA→A)
()Q→R)→(Q→R)→((((())Q→R)→Q)→(Q→R)→R) 2. axioma 2
()Q→R)→Q)→(Q→R)→R) 3. modus ponente 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. theorem schemaA→A)
()Q→R)→(Q→R)→((((())Q→R)→Q)→(Q→R)→R) 2. axioma 2
()Q→R)→Q)→(Q→R)→R) 3. modus ponente 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

Did you mean:

These three steps can be stated succinctly using the Curry–Howard correspondence:

primero, en el cálculo de lambda, la función f = λa. λb. b a tiene tipo q →q → r) → r
segundo, por eliminación de la lambda en b, f = λa. s i (k a)
tercero, por eliminación de la lambda en a, f = s (k i)) k

Contenido relacionado

Más resultados...