Proof of transitivity in Hilbert Style

We can use the following axioms: $$\begin{align} &A\to(B\to A)&\tag{A1}\\ &[A\to(B\to C)]\to[(A\to B)\to(A\to C)]&\tag{A2}\\ &(\lnot A\to\lnot B)\to(B\to A)&\tag{A3} \end{align}$$

We need to prove: $$A\to B, B\to C\vdash A\to C$$

The hint is to use The Deduction Theorem.

I can't for the love of me figure it out, please help :(


Solution 1:

I assume you can use modus ponens as a deductive rule. Here is a Hilbert-style proof. As you can see, there is no reason to use the deduction theorem.

  1. $A \to B$ [assumption]
  2. $B \to C$ [assumption]
  3. $(B \to C) \to (A \to (B \to C))$ [by A1]
  4. $A \to (B \to C)$ [modus ponens, 2 and 3]
  5. $(A \to (B \to C)) \to ((A \to B) \to (A \to C))$ [by A2]
  6. $(A \to B) \to (A \to C)$ [modus ponens, 4 and 5]
  7. $A \to C$ [modus ponens, 1 and 6]