Prueba $( \lnot C \implies \lnot B) \implies (B \implies C)$ sin el Teorema de la Deducción

Question

Se trata del Ejercicio 1.47 (d) de "Lógica Matemática" de Elliot Mendelson. El ejercicio consiste en demostrar $(\lnot C\implies\lnot B)\implies(B\implies C)$ utilizando los tres axiomas $(A1,A2,A3)$ sin utilizar el teorema de la Deducción (y sin ninguna hipótesis).

Los axiomas son:

$A1: B\implies(C\implies B)$

$A2: (B\implies(C\implies D))\implies((B\implies C)\implies(B\implies D))$ $A3: (\lnot C\implies\lnot B)\implies((\lnot C\implies B)\implies C)$

La única regla de inferencia es MP.

Tengo una prueba pero es larga. Mi prueba se basa en la prueba del Lemma 1.11 (d) que prueba $(\lnot C\implies\lnot B)\implies(B\implies C)$ sino que utiliza el Teorema de la Deducción (Proposición 1.9). Entonces, como sugiere Mendelson en el ejercicio 1.49, aplico el proceso utilizado para demostrar el Teorema de la Deducción a los pasos. Para ser precisos, asumo $(\lnot C\implies\lnot B)$ como hipótesis $H$ . Si $C_1,C_2,\dots,C_n$ es una prueba de $(B\implies C)$ que utiliza $H$ entonces paso a paso demuestro $H\implies C_i$ para $i=1,\dots,n$ . El último paso es $H\implies C_n$ que es lo que queremos demostrar.

Este camino requiere alrededor de 4 usos de Axioma1, 4 de Axioma2, 1 Axioma3, y 9 usos de Modus Ponens.

¿Me falta una prueba más corta?

Answer 1

Puedo probarlo "independientemente" del Teorema de la deducción ...pero la prueba es bastante más larga...

Los axiomas son :

1. $F \rightarrow (G \rightarrow F)$

2. $(F \rightarrow (G \rightarrow H))\rightarrow ((F \rightarrow G) \rightarrow (F \rightarrow H))$

3. $(\neg G \rightarrow \neg F) \rightarrow ((\neg G \rightarrow F) \rightarrow G)$

---

---

Para facilitar la lectura, organizaré la prueba con algunos resultados preliminares :

T1 : $P \rightarrow P$

1) $P \rightarrow ((Q \rightarrow P) \rightarrow P)$ --- Ax.1

2) $P \rightarrow (Q \rightarrow P)$ --- Ax.1

3) $(1) \rightarrow ((2) \rightarrow (P \rightarrow P))$ --- Ax.2

4) $P \rightarrow P$ --- de 3), 1) y 2) por Modus Ponens dos veces.

---

T2 : $(Q \rightarrow R) \rightarrow ((P \rightarrow Q) \rightarrow (P \rightarrow R))$

1) $(P \rightarrow (Q \rightarrow R)) \rightarrow ((P \rightarrow Q) \rightarrow (P \rightarrow R))$ --- Ax.2

2) $(1) \rightarrow ((Q \rightarrow R) \rightarrow (1))$ --- Ax.1

3) $(Q \rightarrow R) \rightarrow (1)$ --- de 1) y 2) por Modus Ponens

4) $(Q \rightarrow R) \rightarrow (P \rightarrow (Q \rightarrow R))$ --- Ax.1

5) $(3) \rightarrow ((4) \rightarrow ((Q \rightarrow R) \rightarrow ((P \rightarrow Q) \rightarrow (P \rightarrow R))))$ --- Ax.2

6) $(Q \rightarrow R) \rightarrow ((P \rightarrow Q) \rightarrow (P \rightarrow R))$ --- de 5), 3) y 4) por MP dos veces.

---

T3 : $P \rightarrow ((P \rightarrow Q) \rightarrow Q)$

1) $(P \rightarrow Q) \rightarrow (P \rightarrow Q)$ --- T1

2) $(1) \rightarrow (((P \rightarrow Q) \rightarrow P) \rightarrow ((P \rightarrow Q) \rightarrow Q))$ --- Ax.2

3) $((P \rightarrow Q) \rightarrow P) \rightarrow ((P \rightarrow Q) \rightarrow Q)$ --- de 1) y 2) por MP

4) $P \rightarrow ((P \rightarrow Q) \rightarrow P)$ --- Ax.1

5) $(3) \rightarrow ((4) \rightarrow (P \rightarrow ((P \rightarrow Q) \rightarrow Q)))$ --- T2

6) $P \rightarrow ((P \rightarrow Q) \rightarrow Q)$ --- de 5), 3) y 4) por MP dos veces.

---

T4 : $(P \rightarrow (Q \rightarrow R)) \rightarrow (Q \rightarrow (P \rightarrow R))$

1) $((P \rightarrow Q) \rightarrow (P \rightarrow R)) \rightarrow ((Q \rightarrow (P \rightarrow Q)) \rightarrow (Q \rightarrow (P \rightarrow R)))$ --- T2

2) $(P \rightarrow (Q \rightarrow R)) \rightarrow ((P \rightarrow Q) \rightarrow (P \rightarrow R))$ --- Ax.2

3) $Q \rightarrow (P \rightarrow Q)$ --- Ax.1

4) $(1) \rightarrow ((2) \rightarrow ((P \rightarrow (Q \rightarrow R)) \rightarrow ((3) \rightarrow (Q \rightarrow (P \rightarrow R)))))$ --- T2

5) $(P \rightarrow (Q \rightarrow R)) \rightarrow ((3) \rightarrow (Q \rightarrow (P \rightarrow R)))$ --- de 4), 1) y 2) por MP dos veces

6) $(3) \rightarrow ((3) \rightarrow (Q \rightarrow (P \rightarrow R))) \rightarrow (Q \rightarrow (P \rightarrow R))$ --- T3

7) $((3) \rightarrow (Q \rightarrow (P \rightarrow R))) \rightarrow (Q \rightarrow (P \rightarrow R))$ --- de 6) y 3) por MP

8) $(7) \rightarrow ((5) \rightarrow ((P \rightarrow (Q \rightarrow R)) \rightarrow (Q \rightarrow (P \rightarrow R))))$ --- T2

9) $(P \rightarrow (Q \rightarrow R)) \rightarrow (Q \rightarrow (P \rightarrow R))$ --- de 8), 7) y 5) por MP dos veces.

---

---

Ahora la prueba :

1) $(\neg C \rightarrow \neg B) \rightarrow ((\neg C \rightarrow B) \rightarrow C)$ --- Ax.3

2) $B \rightarrow (\neg C \rightarrow B)$ --- Ax.1

3) $(\neg C \rightarrow B) \rightarrow ((\neg C \rightarrow \neg B) \rightarrow C)$ --- de 1) y T4 por Modus Ponens

4) $B \rightarrow ((\neg C \rightarrow \neg B) \rightarrow C)$ --- de T2, 3) y 2) por MP dos veces

5) $(\neg C \rightarrow \neg B) \rightarrow (B \rightarrow C)$ --- de T4 y 4) por MP

Answer 2

Actualmente estoy leyendo el texto de Mendelson, y así es como probé el ejercicio 1.47(d) . Requiere tanto los resultados de los ejercicios 1.47(a) y (c) que son partes previas del mismo ejercicio.

He aquí los axiomas:

(A1) $A\Rightarrow \left(B\Rightarrow A\right)$ .

(A2) $\left(A\Rightarrow \left(B\Rightarrow C\right)\right)\Rightarrow\left(\left(A\Rightarrow B\right)\Rightarrow\left(A\Rightarrow C\right)\right)$ .

(A3) $\left(\neg B\Rightarrow\neg A\right)\Rightarrow\left(\left(\neg B\Rightarrow A\right)\Rightarrow B\right)$ .

La única regla de inferencia es el Modus Ponens:

(MP) $\left\langle A, A\Rightarrow B, B\right\rangle$

Los resultados anteriores ya deberías haberlos probado dentro de la misma sección:

1.47(a) $\mathcal{A}\Rightarrow\mathcal{B}, \mathcal{B}\Rightarrow\mathcal{C}\vdash_{L}\mathcal{A}\Rightarrow\mathcal{C}$ .

1.47(c) $\mathcal{A}\Rightarrow\left(\mathcal{B}\Rightarrow\mathcal{C}\right)\vdash_{L}\mathcal{B}\Rightarrow\left(\mathcal{A}\Rightarrow\mathcal{C}\right)$ .

He aquí la prueba del ejercicio:

1. $\varphi\Rightarrow\left(\neg\psi\Rightarrow\varphi\right)$ de (A1) .

2. $\left(\neg\psi\Rightarrow\neg\varphi\right)\Rightarrow\left(\left(\neg\psi\Rightarrow\varphi\right)\Rightarrow\psi\right)$ de (A3) .

3. $\left(\neg\psi\Rightarrow\varphi\right)\Rightarrow\left(\left(\neg\psi\Rightarrow\neg\varphi\right)\Rightarrow\psi\right)$ de 1.47(c) utilizando 2.

4. $\varphi\Rightarrow\left(\left(\neg\psi\Rightarrow\neg\varphi\right)\Rightarrow\psi\right)$ de 1.47(a) utilizando 1. y 3.

5. $\left(\neg\psi\Rightarrow\neg\varphi\right)\Rightarrow\left(\varphi\Rightarrow\psi\right)$ de 1.47(c) utilizando 4.

Esto completa la prueba.

Es importante señalar aquí que no se utilizó el Teorema de la Deducción. Aunque no es necesario, se puede incrustar en esta demostración la demostración de 1.47(a) ou (c) siempre que se utilice uno de ellos. Los axiomas (A1) y (A3) son las únicas premisas subyacentes que justifican el primer uso de 1.47(c) .

Answer 3

No sé cómo se escriben esas rebuscadas B y esas rebuscadas C que Mendelson utiliza en ese texto. Mendelson pone paréntesis (deliberadamente) alrededor de todas las wffs cuando habla del esquema axiomático, y eso tiene sentido porque hace que la sustitución de wffs por otras wffs sea sólo cuestión de encontrar patrones de símbolos similares. No necesitamos inferir un significado y reconocer un patrón, sólo necesitamos reconocer un patrón cuando realmente escribes wffs.

Debido a la correspondencia entre las formas semánticas de enunciado de Mendelson y las wffs sintácticas de Mendelson, las wffs tienen propiedades similares a las formas de enunciado. Mendelson indica en el ejercicio 1.18 de la p. 12 de la quinta edición que, en lugar de escribir formas de enunciado como él suele hacer, se puede utilizar la notación polaca, que, según él, se parece a cualquier notación de prefijos. El siguiente sistema tiene símbolos más parecidos a la notación polaca original de Lukasiewicz, Meredith, Prior y otros autores cuyos trabajos puede leer para gratis a través de números antiguos del Norte Dame Journal of Formal Logic. Debido a la forma en que Mendelson escribe en su Schaum's Outline of Boolean Algebra, parece que podemos representar fielmente la intención de Mendelson usando mayúsculas en negrita en lugar de mayúsculas de fantasía. A continuación pongo cada esquema axiomático del sistema en notación polaca que usaré junto al esquema axiomático correspondiente del sistema de Mendelson.

  Polish               Mendelson

Ax 1 CbCcb ..................... ( B -> ( C -> B ))

Ax 2 CCbCdCCbcCbd ... (( B -> ( C -> D )) -> (( B -> C ) -> ( B -> D )))

Ax 3 CCNcNbCCNcbc .....((( $\lnot$ C ) -> ( $\lnot$ B )) -> ((( $\lnot$ C ) -> B ) -> C ))

Una demostración en un sistema que utilice la notación polaca de cierta longitud implica que se puede escribir una demostración en el sistema de Mendelson que utilice la notación de Mendelson de la misma longitud.

Axiom Schema                 1  CbCcb
Axiom Schema                 2  CCbCcdCCbcCbd
Axiom Schema                 3  CCNcNbCCNcbc
1 b/CbCcb, c/a               4  CCbCcbCaCbCcb
4 * C1-5                     5  CaCbCcb
2 b/CbCcd, c/Cbc, d/Cbd      6  CCCbCcdCCbcCbdCCCbCcdCbcCCbCcdCbd
6 * C1-7                     7  CCCbCcdCbcCCbCcdCbd
2 b/a, c/b, d/Ccb            8  CCaCbCcbCCabCaCcb
8 * C5-9                     9  CCabCaCcb
5 a/CbCCcbd                  10 CCbCCcbdCbCcb
7 c/Ccb                      11 CCCbCCcbdCbCcbCCbCCcbdCbd
11 * C10-12                  12 CCbCCcbdCbd
9 a/CNcNb, b/CCNcbc, c/d     13 CCCNcNbCCNcbcCCNcNbCdCCNcbc
13 * C3-14                   14 CCNcNbCdCCNcbc
1 b/CCbCCcbdCbd, c/a         15 CCCbCCcbdCbdCaCCbCCcbdCbd
15 * C12-16                  16 CaCCbCCcbdCbd
2 b/a, c/CbCCcbd, d/Cbd      17 CCaCCbCCcbdCbdCCaCbCCcbdCaCbd
17 * C16-18                  18 CCaCbCCcbdCaCbd
18 a/CNcNb, c/Nc, d/c        19 CCCNcNbCbCCNcbcCCNcNbCbc
14 d/b                       20 CCNcNbCbCCNcbc
19 * C20-21                  21 CCNcNbCbc

Así, una prueba puede escribirse en el sistema de Mendelson en 21 pasos si incluimos el esquema original de 3. Si no lo hacemos, puede hacerse en exactos 21 pasos. Si no lo hacemos, se puede hacer exactamente en 18 pasos.