Si A→(B∧C), demostrar (D→A) → (D→C) sin usar prueba condicional.

Question

La versión de prueba condicional de esto es bastante fácil. Sin embargo, resolver esto sin prueba condicional parece ser bastante difícil.

Intenté convertir la premisa en:

1. ~A v (BC)

2. (~AvB) (~AvC)

Intenté usar la introducción de la disyunción para transformar (~AvC) en (DA) (DC) pero fallé.

¿Alguna idea de cómo debería proceder? ¿Tal vez la introducción de la disyunción no es la forma correcta de abordar este problema?

Answer 1

1) $A \to (B \land C)$ --- premisa

2) $\lnot A \lor (B \land C)$ --- de 1) por Implicación material

3) $(\lnot A \lor B) \land (\lnot A \lor C)$ --- de 2) por Distributividad

4) $(\lnot A \lor C)$ --- de 3) por Eliminación de la conjunción

5) $(\lnot A \lor C) \lor \lnot D" --- de 4) por Introducción de la disyunción

6) $[(\lnot D \lor C) \lor D] \land [(\lnot D \lor C) \lor \lnot A]$ --- de 5) usando : $[(\lnot A \lor C) \lor \lnot D] \equiv [(\lnot A \lor C) \lor \lnot D] \land TRUE$ y : $TRUE \equiv (D \lor \lnot D) \lor C$ y Asociatividad y Conmutatividad

7) $(\lnot D \lor C) \lor (D \land \lnot A)$ --- de 6) por Distributividad

8) $\lnot (\lnot D \lor A) \lor (\lnot D \lor C)$ --- de 7) por Leyes de De Morgan

9) $(\lnot D \lor A) \to (\lnot D \lor C)$ --- de 9) por Implicación material

10) $(D \to A) \to (D \to C)$ --- de 9) por Implicación material.

---

Por supuesto, con Deducción natural la prueba es mucho más fácil.

Answer 2

Puedes probar esto a través de lo que podría llamarse "prefixación" CCpqCCrpCrq, lo que no está muy lejos en términos de desprendimiento condensado del conjunto de axiomas.

Yo uso notación polaca. Las reglas de formación son:

1. Todas las letras del alfabeto latino son fórmulas bien formadas.
2. Si $\alpha$ y $\beta$ califican como fórmulas bien formadas, también lo hacen C$\alpha$$\beta$ y K$\alpha$$\beta$.

Entonces, queremos demostrar CaKbc $\vdash$ CCdaCdc.

Los axiomas que usaré son CpCqp - Recursión de Prefijación de Variables, CCpCqrCCpqCpr - Distribución de C-Self, CKpqq - eliminación de conjunción a la derecha. También uso desprendimiento condensado. Nota que podemos hacer sustituciones para cualquier letra, excepto para a, b, c y d en lo siguiente.

axioma      1 CpCqp
axioma      2 CCpCqrCCpqCpr
axioma      3 CKpqq
D1.2       4 CpCCqCrsCCqrCqs
D2.4       5 CCpCqCrsCpCCqrCqs
D5.1       6 CCpqCCrpCrq
suposición 7 CaKbc
D6.3       8 CCpKqrCpr
D8.7       9 Cac
D6.9      10 CCpaCpc

Y CCpaCpc se presenta como una fórmula bien formada más general del caso especial CCdaCdc.