Es mi derivación de $\vdash (\forall x)(B \implies C) \implies ((\forall x)B \implies (\forall x)C)$ ¿correcto?
Estoy leyendo Introducción a la lógica matemática de Mendelson. Estoy en el capítulo 2 "Lógica de primer orden y teoría de modelos". Los axiomas son:
($A1$): $B ⇒ (C ⇒ B)$
($A2$): $(B ⇒ (C ⇒ D)) ⇒ ((B ⇒ C) ⇒ (B ⇒ D))$
($A3$): $(¬C ⇒ ¬B) ⇒ ((¬C ⇒ B) ⇒ C)$
($A4$): $(∀x_i)B(x_i) ⇒ B(t)$ si $B(x_i)$
($A5$): $(∀x_i)(B ⇒ C) ⇒ (B ⇒ (∀x_i)C)$
Las reglas son:
- Modus ponens: $C$ sigue desde $B$ y $B ⇒ C$. (MP)
- Generalización: $(∀x_i)B$ sigue desde $B$. (Gen)
El ejercicio 2.27a (de la sección 2.4) es $⊢ (∀x)(B ⇒ C) ⇒ ((∀x)B ⇒ (∀x)C)$ y noté que la derivación que Mendelson da en las soluciones difiere de la mía (usé Axiom 5 una vez y no usé la regla Gen, y Mendelson no usó Axiom 5 pero usó la regla Gen), así que quería preguntar:
- ¿Mi derivación es correcta?
- Si es incorrecto, ¿cuál es el error?
Mi derivación (usando el teorema de deducción) es la siguiente:
- $(∀x)(B ⇒ C)$ Hip
- $(∀x)B$ Hip
- $(∀x)(B ⇒ C) ⇒ (B ⇒ (∀x)C)$ Axioma (A5)
- $B ⇒ (∀x)C$ MP 1,3
- $(∀x)B ⇒ B$ Axioma (A4)
- $B$ MP 2,5
- $(∀x)C$ MP 4,6
- $(∀x)(B ⇒ C), (∀x)B ⊢ (∀x)C$ 1-7
- $(∀x)(B ⇒ C) ⊢ (∀x)B ⇒ (∀x)C$ 1-8 corolario 2.6 (Mendelson)
- $⊢ (∀x)(B ⇒ C) ⇒ ((∀x)B ⇒ (∀x)C)$ 1-9 corolario 2.6 (Mendelson)
La derivación de Mendelson (usando el teorema de deducción) es la siguiente:
- $(∀x)(B ⇒ C)$ Hip
- $(∀x)B$ Hip
- $(∀x)(B ⇒ C) ⇒ (B ⇒ C)$ Axioma (A4)
- $B ⇒ C$ 1, 3, MP
- $(∀x)B ⇒ B$ Axioma (A4)
- $B$ 2, 5, MP
- $C$ 4, 6, MP
- $(∀x)C$ 7, Gen
- $(∀x)(B ⇒ C), (∀x)B ⊢ (∀x)C$ 1-8
- $(∀x)(B ⇒ C) ⊢ (∀x)B ⇒ (∀x)C$ 1-9, Corolario 2.6
- $⊢ (∀x)(B ⇒ C) ⇒ ((∀x)B ⇒ (∀x)C)$ 1-10, Corolario 2.6
Respuestas
Su intento de derivación es incorrecto. De hecho, en axioma$A5$, hay una condición secundaria : la fórmula$B$ no debe contener apariciones libres de la variable $x$ (esta condición secundaria debe informarse en el libro de texto de Mendelson), mientras que en la fórmula desea probar $B$ puede contener apariciones gratuitas de $x$. Por lo tanto, el tercer paso de su derivación es incorrecto: no puede justificar la fórmula$∀x(B \to C) \to (B \to ∀x C)$ como una instancia de axioma $A5$, porque $x$ puede ocurrir gratis en $B$.
Por el contrario, la derivación de Mendelson es, por supuesto, perfectamente correcta. En particular, no utiliza ningún axioma con tales restricciones.
Por cierto, tenga en cuenta también que el uso de la regla de generalización se ve afectado por una condición secundaria: puede derivar $\forall x B$ desde $B$ siempre que la variable $x$no ocurre libre en ninguna hipótesis de la derivación. La derivación de Mendelson respeta esta condición secundaria cuando usa la regla de generalización.
Las condiciones secundarias son importantes, porque evitan derivar fórmulas que no deberían ser demostrables.