Formal proof of $(A\lor B)∨C \leftrightarrow A\lor(B\lor C)$

Question

$A\lor B$ by definition $\neg A\implies B$

Deduction rules:

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)$

These are axiom schemas

How to prove $(A\lor B)∨C \iff A\lor(B\lor C)$

where we need to prove $(A\lor B)∨C \implies A\lor(B\lor C)$ and $A\lor(B\lor C) \implies (A\lor B)∨C$

This is not a homework problem.

Answer 1

As per my answer to your previous post , I'll assume that we have available the Deduction Th, that is provable (together with $\vdash A ⇒ A$) from A1) and A2) only.

---

For : $[¬A⇒(¬B⇒C)] \Leftrightarrow [¬(¬A⇒B)⇒C]$, we need some preliminary Lemma :

Lemma 1 : $A ⇒ B, B ⇒ C \vdash A ⇒ C$ --- Syllogism "derived rule" : easily provable with DT

Lemma 2 : $¬¬A ⇒ A$ --- Double Negation :

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

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

c) $¬¬A ⇒ (¬A ⇒ ¬¬¬A)$ --- from a) and b) by Lemma 1

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

e) $¬¬A ⇒ (¬¬A ⇒ A)$ --- from c) and d) by Lemma 1

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

g) $¬¬A ⇒ A$ --- from e), f) and $\vdash ¬A ⇒ ¬A$, by MP twice.

Lemma 3 : $A ⇒ ¬¬A$ --- Double Negation :

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

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

c) $A ⇒ ¬¬A$ --- from a) and b) by MP.

Lemma 4 : $(¬B ⇒ A) ⇒ (¬A ⇒ B)$ --- provable from axiom A3), with Lemma 2 and Lemma 1.

Lemma 5 : $(A ⇒ B) ⇒ (¬¬A ⇒ ¬¬B)$ --- provable from Lemma 2, Lemma 3 and Lemma 1.

Lemma 6 : $(A ⇒ B) ⇒ (¬B ⇒ ¬A)$ --- provable from Lemma 5, axiom A3) and Lemma 1.

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

a) $¬A ⇒ ((¬A⇒B) ⇒ B)$ --- from $¬A, ¬A ⇒ B \vdash B$ and DT

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

c) $¬A ⇒ (¬B ⇒ ¬(¬A⇒B))$ --- from a) and b) by Lemma 1.

---

Now for the main proof :

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

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

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

4) $¬(¬A⇒B)$ --- from 2), 3) and Lemma 7, by Modus Ponens twice

5) $C$ --- from 4) and 1) by MP

6) $¬B⇒C$ --- from 3) and 5) by Deduction Th, discharging assumption [b]

7) $¬A⇒(¬B⇒C)$ --- from 2) and 6) by Deduction Th, discharging assumption [a]

8) $[¬(¬A⇒B)⇒C] ⇒ [¬A⇒(¬B⇒C)]$ --- from 1) and 7), discharging the premise 1)

---

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

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

11) $¬B ⇒ C$ --- from 9) and 10) by MP

12) $¬C ⇒ B$ --- from 11) and Lemma 4 by MP

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

14) $B$ --- from 13) and 12) by MP

15) $¬A ⇒ B$ --- from 10) and 14) by DT, discharging assumption [c]

16) $¬C ⇒ (¬A ⇒ B)$ --- from 13) and 15) by DT, discharging assumption [d]

17) $¬(¬A ⇒ B) ⇒ C$ --- from 16) and Lemma 4 by MP

18) $[¬A⇒(¬B⇒C)] ⇒ [¬(¬A ⇒ B) ⇒ C]$ --- from 9) and 17) by DT, discharging the premise 9).

---

16) The bi-conditional follows from 8) and 18).