Formal deductions on Hilbert system

Question

I have proved {(α→β),(β →γ)} ⊢ (α→γ) } using formal deductions using Modus Ponens and the three axiom of H2 : A1: A -> (B-> A) A2: (A-> (B->C)) -> ((A-> B) -> ( A -> C)) A3: (( ¬ A) -> ( ¬B)) -> ( B -> A)

However now my professor is asking me to prove : (1) (α→β) ⊢ (β →γ)→(α→γ) and (2) ⊢ (α→β)->((β →γ)→(α→γ)). I am stuck on it since proving their existence with the deduction theorem is not enough. I must use formal deductions, any help for this ? Thank you

Answer 1

OK, let's call your first proven pattern HS (for Hypothetical Syllogism). We can nicely exploit that one for the next two. First, let's prove $\vdash (A \rightarrow B) \rightarrow ((B \rightarrow C) \rightarrow (A \rightarrow C))$:

1. $(B \rightarrow C) \rightarrow (A \rightarrow (B \rightarrow C))$ Axiom 1

2. $(A \rightarrow (B \rightarrow C)) \rightarrow ((A \rightarrow B) \rightarrow (A \rightarrow C))$ Axiom 2

3. $(B \rightarrow C) \rightarrow ((A \rightarrow B) \rightarrow (A \rightarrow C))$ HS 1,2

4. $((B \rightarrow C) \rightarrow ((A \rightarrow B) \rightarrow (A \rightarrow C))) \rightarrow (((B \rightarrow C) \rightarrow (A \rightarrow B)) \rightarrow ((B \rightarrow C) \rightarrow (A \rightarrow C)))$ Axiom 2

5. $((B \rightarrow C) \rightarrow (A \rightarrow B)) \rightarrow ((B \rightarrow C) \rightarrow (A \rightarrow C))$ MP 3,4

6. $(A \rightarrow B) \rightarrow ((B \rightarrow C) \rightarrow (A \rightarrow B))$ Axiom 1

7. $(A \rightarrow B) \rightarrow ((B \rightarrow C) \rightarrow (A \rightarrow C))$ HS 5,6

This makes the proof of $\vdash (B \rightarrow C) \rightarrow ((A \rightarrow B) \rightarrow (A \rightarrow C))$ trivial:

1. $A \rightarrow B$ Assumption

2. $(A \rightarrow B) \rightarrow ((B \rightarrow C) \rightarrow (A \rightarrow C))$ (we just proved this)

3. $(B \rightarrow C) \rightarrow (A \rightarrow C)$ MP 1,2