Proving $\vdash_{HPI}A\vee(B\vee C) \rightarrow (A\vee B)\vee C $

Question

Prove $\vdash_{HPI}A\vee(B\vee C) \rightarrow (A\vee B)\vee C $

From the axioms :

A1) A→(B→A)

A2) (A→(B→C))→((A→B)→(A→C))

A3) $(A\rightarrow B)\rightarrow((A\rightarrow\neg B)\rightarrow \neg A)$

A4) $\neg A\rightarrow A\rightarrow B$

A5) (A∧B)→A

A6) (A∧B)→B

A7) A→(B→(A∧B))

A8) A→(A∨B)

A9) B→(A∨B)

A10) (A→B)→((C→B)→((A∨C)→B))

and MP

I know by the deduction theorem it is enough to show $A\vee(B\vee C) \vdash_{HPI} (A\vee B)\vee C $.

It's clearly true because of associativity. However, I'm not sure how to prove it formally using only the axioms above.

Thanks

Answer 1

In the Hilbert-style proof system for propositional calculus above, we can use the "derived rule" of Hypothetical Syllogism :

$A \to B, B \to C \vdash A \to C$.

With it, we have:

1) $B \to (A \lor B)$

2) $(A \lor B) \to (A \lor B) \lor C$

3) $B \to (A \lor B) \lor C$ --- from 1) and 2) by HS

4) $C \to (A \lor B) \lor C$

5) $B \lor C \to (A \lor B) \lor C$ --- from 3) and 4) by A10) and Modus Ponens twice

6) $A \to (A \lor B)$

7) $(A \lor B) \to (A \lor B) \lor C$

8) $A \to (A \lor B) \lor C$ --- from 6) and 7) by HS

9) $A \lor (B \lor C) \to (A \lor B) \lor C$ --- from 5) and 8) by A10) and Modus Ponens twice.

---

In order to prove Hypothetical Syllogism, we have :

1. $A \rightarrow B$ --- premise

2. $B \rightarrow C$ --- premise

3. $(B \rightarrow C) \rightarrow (A \rightarrow (B \rightarrow C))$ --- A1)

4. $A \rightarrow (B \rightarrow C)$ --- from 2) and 3) by MP

5. $(A \rightarrow (B \rightarrow C)) \rightarrow ((A \rightarrow B) \rightarrow (A \rightarrow C))$ --- A2)

6. $(A \rightarrow B) \rightarrow (A \rightarrow C)$ --- from 4) and 5) by MP

7. $A \rightarrow C$ --- from 1) and 6) by MP.