Prove that {A ⇒ ¬C, ¬A ⇒ B} ⊢ C ⇒ B using only Modus Ponens, the typical theorem (A → ¬C) → (C → ¬A) and 3 axioms.

Question

I have an exercise where I have to prove the given sentence {A ⇒ ¬C, ¬A ⇒ B} ⊢ C ⇒ B using only Modus Ponens, the typical theorem (A → ¬C) → (C → ¬A) and the following three axioms:

1. A→(B→A)
2. (A→(B→C))→((A→B)→(A→C))
3. (¬A→¬B)→((¬A→B)→A)

what I've done so far is

1. A ⇒ ¬C Premise
2. (A → ¬C) → (C → ¬A) from the Typical Theorem
3. (C → ¬A) M.P 1,2
4. ¬A ⇒ B Premise ...

However I'm getting a bit confused on what substitutions to do given the 3 axioms in order proceed.

Any ideas anyone? Thank you!

Answer 1

You need an intermediate result (sometimes called Hypothetical Syllogism):

Lemma : $A \rightarrow B, B \rightarrow C \vdash A \rightarrow C$

(1) $A \rightarrow B$ --- assumed

(2) $B \rightarrow C$ --- assumed

(3) $\vdash (B \rightarrow C) \rightarrow (A \rightarrow (B \rightarrow C))$ --- Ax1

(4) $A \rightarrow (B \rightarrow C)$ --- from (2) and (3) by Modus Ponens

(5) $\vdash [A \rightarrow (B \rightarrow C)] \rightarrow [(A \rightarrow B) \rightarrow (A \rightarrow C)]$ --- Ax2

(6) $(A \rightarrow B) \rightarrow (A \rightarrow C)$ --- from (4) and (5) by Modus Ponens

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

Now the main result:

(1) $A \to ¬C$ --- premise

(2) $¬A \to B$ --- premise

(3) $C \to \lnot A$ --- from (1) and the Typical Theorem by MP

(4) $C \to B$ --- from (3), (1) and Lemma.