Proving $(p \to q) \to ((q \to r) \to (p \to r))$ from Hilbert formal system for positive implicational formal system?

Question

How to prove suffixing $(p \to q) \to ((q \to r) \to (p \to r))$ from weakening and self-distribution axioms and MP. So, in system with axioms $$A1. p \to (q \to p))$$ $$A2. (p \to (q \to r)) \to ((p \to q) \to (p \to r))$$ and MP figure, how to prove that suffixing statement is a theorem (without Deduction theorem).

Answer 1

Here is complete answer. Thanks for help.

1. $(q \to r) \to (p \to (q \to r))$ A1
2. $(p \to (q \to r)) \to ((p \to q) \to (p \to r))$ A2
3. $(2) \to ((q \to r)\to (2))$ A1
4. $(q \to r) \to (2)$ MP 2,3
5. $(4) \to ((1) \to ((q \to r) \to ((p \to q) \to (p \to r))))$ A2
6. $(1) \to ((q \to r) \to ((p \to q) \to (p \to r)))$ MP 4,5
7. $(q \to r) \to ((p \to q) \to (p \to r))$ MP 1,6
8. $(7) \to (((q \to r) \to (p \to q)) \to ((q \to r) \to (p \to r)))$ A2
9. $((q \to r) \to (p \to q)) \to ((q \to r) \to (p \to r))$ MP 7,8
10. $(p \to q) \to ((q \to r) \to (p \to q))$ A1
11. $(9) \to ((p \to q) \to (9))$ A1
12. $(p \to q) \to (9)$ MP 9,11
13. $(12) \to (((p \to q) \to ((q \to r) \to (p \to q))) \to ((p \to q) \to ((q \to r) \to (p \to r))))$ A2
14. $((p \to q) \to ((q \to r) \to (p \to q))) \to ((p \to q) \to ((q \to r) \to (p \to r)))$ MP 12,13
15. $(p \to q) \to ((q \to r) \to (p \to r))$ MP 10,14

Answer 2

Let's first prove Hypothetical Syllogism (HS), i.e. that $\{p \rightarrow q , q \rightarrow r \} \vDash p \rightarrow r)$:

1. $p \rightarrow q$ Premise

2. $q \rightarrow r$ Premise

3. $(q \rightarrow r) \rightarrow (p \rightarrow (q \rightarrow r))$ Axiom 1

4. $p \rightarrow (q \rightarrow r)$ MP 2,3

5. $(p \rightarrow (q \rightarrow r)) \rightarrow ((p \rightarrow q) \rightarrow (p \rightarrow r))$ Axiom 2

6. $(p \rightarrow q) \rightarrow (p \rightarrow r)$ MP 4,5

7. $p \rightarrow r$ MP 1,6

And now that you have HS:

1. $(q \rightarrow r) \rightarrow (p \rightarrow (q \rightarrow r))$ Axiom 1

2. $(p \rightarrow (q \rightarrow r)) \rightarrow ((p \rightarrow q) \rightarrow (p \rightarrow r))$ Axiom 2

3. $(q \rightarrow r) \rightarrow ((p \rightarrow q) \rightarrow (p \rightarrow r))$ HS 1,2

4. $((q \rightarrow r) \rightarrow ((p \rightarrow q) \rightarrow (p \rightarrow r))) \rightarrow (((q \rightarrow r) \rightarrow (p \rightarrow q)) \rightarrow ((q \rightarrow r) \rightarrow (p \rightarrow r)))$ Axiom 2

5. $((q \rightarrow r) \rightarrow (p \rightarrow q)) \rightarrow ((q \rightarrow r) \rightarrow (p \rightarrow r))$ MP 3,4

6. $(p \rightarrow q) \rightarrow ((q \rightarrow r) \rightarrow (p \rightarrow q))$ Axiom 1

7. $(p \rightarrow q) \rightarrow ((q \rightarrow r) \rightarrow (p \rightarrow r))$ HS 5,6