Teorema de deducción: interpretación
En el libro "Un recorrido por la lógica matemática", de Robert S. Wolf, el teorema de la deducción se especifica de la siguiente manera:
Si t $\cup$ {PAGS} $\vdash$ Q, luego T $\vdash$ (PAGS $\to$ Q)
Donde T es una teoría de primer orden y P & Q son algunas fórmulas, en el lenguaje de esta teoría de primer orden. Entonces, ¿es correcta la siguiente interpretación del teorema de deducción?
Si Q es derivable / demostrable de T $\cup$ {P}, entonces se puede decir que - si P es derivable de T (es decir, P es un teorema de T), entonces Q también es derivable de T.
Además, ¿esta interpretación captura la esencia del teorema de deducción?
PD: otra pregunta titulada Teorema de la deducción: intuición , parece centrarse principalmente en los aspectos sintácticos del teorema y el cálculo de predicados en general, más que en su semántica.
Respuestas
¿Es correcta la siguiente interpretación del teorema de deducción?
No. Lo que escribes es
Si $T \cup \{P\} \vdash Q$, Entonces sí $T \vdash P$, luego $T \vdash Q$.
Esto es lo mismo que decir
(1) Si $T \cup \{P\} \vdash Q$, luego $T \nvdash P$ o $T \vdash Q$.
Pero esto no es equivalente a
(2) Si $T \cup \{P\} \vdash Q$, luego $T \vdash P \to Q$.
Puede ser el caso que $P$ no es demostrable, pero $P \to Q$tampoco lo es. Luego "$T \nvdash P$ o $T \vdash Q$"aguanta, pero"$T \vdash P \to Q$"no lo hace. Entonces (1) $\not \Rightarrow$ (2).
Esto es lo que se entiende en los comentarios por "trivialización": "si $T \vdash P$ luego $T \vdash Q$"(= lo que escribiste) se vuelve trivialmente cierto si $T \nvdash P$, es decir, si $P$es indemostrable. Pero "$T \vdash P \to Q$"(= lo que dice el teorema de la deducción) no: solo porque no podemos probar $P$ no significa que podamos probar $P\to Q$- como observó. De ahí por qué "$T \vdash P \to Q$"es una afirmación más sólida de que" Si $T \vdash P$ luego $T \vdash Q$".
La esencia del teorema de la deducción es que se puede cambiar entre tener un teorema dependiente de un supuesto abierto y demostrar un enunciado condicional:
si hay una prueba de$Q$ que todavía depende de la suposición $P$, entonces habrá una prueba en la teoría del enunciado $P \to Q$. Este es el efecto inmediato de la técnica de prueba condicional (ver p. 14).
Y para la dirección inversa del teorema de deducción, si puede probar$P \to Q$, entonces podrás probar $Q$ bajo el supuesto de que $P$. Esto es una consecuencia de la regla de inferencia del modus ponens (ver p. 13).
Combinando las dos direcciones, el teorema de deducción simplemente justifica lo que queremos decir con una prueba de "$\to$".
Tiene usted toda la razón al señalar que la noción central de un sistema formal es la de prueba más que la de verdad. Pero tenga en cuenta que normalmente estamos interesados en diseñar un sistema de prueba "útil" que esté "en línea" con la noción de verdad: una afirmación debe poder demostrarse en una teoría exactamente cuando es verdadera en todos los modelos de la teoría . Después de todo, el objetivo de un sistema de prueba es tener un dispositivo mecánico para probar rigurosamente las afirmaciones que consideramos verdaderas. Entonces, mientras que la noción de una prueba de$\to$ está formulado en términos de reglas de inferencia, la forma en que se utilizan estas reglas refleja la tabla de verdad para $\to$: Un sistema de prueba debe ser (y en cuanto al sistema de prueba presentado en el libro de Wolf, es) sólido con la semántica: Lo que se puede probar es verdadero (de acuerdo con las definiciones de la tabla de verdad) en todas las estructuras; el sistema (con suerte) no resulta sin sentido aleatorio.