Prueba Formal de las $(A\lor B)∨C \leftrightarrow A\lor(B\lor C)$

Question

$A\lor B$ , por definición, $\neg A\implies B$

Deducción de las reglas:

1. $A\implies (B\implies A)$
2. $(A\implies (B\implies C))\implies ((A\implies B)\implies(A\implies C))$
3. $(\neg B\implies \neg A)\implies(A\implies B)$

Estos son esquemas de axioma

Cómo demostrar a $(A\lor B)∨C \iff A\lor(B\lor C)$

donde tenemos que demostrar $(A\lor B)∨C \implies A\lor(B\lor C)$ $A\lor(B\lor C) \implies (A\lor B)∨C$

Esta no es una tarea problema.

Answer 1

Según mi respuesta a tu anterior post , voy a asumir que tenemos disponible la Deducción de Th, que es comprobable (junto con $\vdash A ⇒ A$) de A1) y A2).

---

Para : $[¬A⇒(¬B⇒C)] \Leftrightarrow [¬(¬A⇒B)⇒C]$, necesitamos algunos preliminar Lema :

Lema 1 : $A ⇒ B, B ⇒ C \vdash A ⇒ C$ --- Silogismo ", derivada de la regla" : fácilmente comprobable con DT

Lema 2 : $¬¬A ⇒ A$ --- Doble Negación :

a) $¬¬A ⇒ (¬¬¬¬A ⇒ ¬¬A)$ --- axioma A1)

b) $(¬¬¬¬A ⇒ ¬¬A) ⇒ (¬A ⇒ ¬¬¬A)$ --- axioma A3)

c) $¬¬A ⇒ (¬A ⇒ ¬¬¬A)$ --- de a) y b) por el Lema 1

d) $(¬A ⇒ ¬¬¬A) ⇒ (¬¬A ⇒ A)$ --- axioma A3)

e) $¬¬A ⇒ (¬¬A ⇒ A)$ --- de c) y d) por el Lema 1

f) $(¬¬A ⇒ (¬¬A ⇒ A)) ⇒ [(¬¬A ⇒ ¬¬A) ⇒ (¬¬A ⇒ A)]$ --- axioma A2)

g) $¬¬A ⇒ A$ --- a e), f) y $\vdash ¬A ⇒ ¬A$, por MP dos veces.

Lema 3 : $A ⇒ ¬¬A$ --- Doble Negación :

a) $¬¬¬A ⇒ ¬A$ --- Lexema 2

b) $(¬¬¬A ⇒ ¬A) ⇒ (A ⇒ ¬¬A)$ --- axioma A3)

c) $A ⇒ ¬¬A$ --- de a) y b) por MP.

Lema 4 : $(¬B ⇒ A) ⇒ (¬A ⇒ B)$ --- comprobable del axioma A3), con el Lema 2 y Lema 1.

Lema 5 : $(A ⇒ B) ⇒ (¬¬A ⇒ ¬¬B)$ --- comprobable de Lema 2, Lema 3 y Lema 1.

Lema 6 : $(A ⇒ B) ⇒ (¬B ⇒ ¬A)$ --- comprobable de Lema 5, axioma A3) y Lema 1.

Lema 7 : $¬A⇒(¬B⇒¬(¬A⇒B))$ :

a) $¬A ⇒ ((¬A⇒B) ⇒ B)$ --- de $¬A, ¬A ⇒ B \vdash B$ y el DT

b) $((¬A⇒B) ⇒ B) ⇒ (¬B ⇒ ¬(¬A⇒B))$ --- Lexema 6

c) $¬A ⇒ (¬B ⇒ ¬(¬A⇒B))$ --- de a) y b) por el Lema 1.

---

Ahora la principal prueba :

1) $¬(¬A⇒B)⇒C$ --- premisa

2) $¬A$ --- asumido [a]

3) $¬B$ --- asumido [b]

4) $¬(¬A⇒B)$ --- de 2), 3) y Lema 7, por Modus Ponens dos veces

5) $C$ --- de 4) y 1) por MP

6) $¬B⇒C$ --- a partir de 3) y 5) por la Deducción de la Th, la descarga de asunción [b]

7) $¬A⇒(¬B⇒C)$ --- de 2) y 6) por la Deducción de la Th, la descarga de asunción [a]

8) $[¬(¬A⇒B)⇒C] ⇒ [¬A⇒(¬B⇒C)]$ --- desde el 1) y 7), la descarga de la premisa 1)

---

9) $¬A⇒(¬B⇒C)$ --- premisa

10) $¬A$ --- asumido [c]

11) $¬B ⇒ C$ --- de 9) y 10) por MP

12) $¬C ⇒ B$ --- a partir de las 11) y el Lema 4 por MP

13) $¬C$ --- asumido [d]

14) $B$ --- a partir de 13 años) y 12) por MP

15) $¬A ⇒ B$ --- de 10) y 14) por DT, la descarga de asunción [c]

16) $¬C ⇒ (¬A ⇒ B)$ --- a partir del 13) y 15) por DT, la descarga de asunción [d]

17) $¬(¬A ⇒ B) ⇒ C$ --- a partir de 16) y el Lema 4 por MP

18) $[¬A⇒(¬B⇒C)] ⇒ [¬(¬A ⇒ B) ⇒ C]$ --- de 9) y 17) por DT, la descarga de la premisa de 9).

---

16) La bi-condicional de la siguiente manera a partir de 8) y 18).