Axiomatic Schema Substitution

Question

With the following axiomatic schema (A1 - A3)

$(A1)(B \rightarrow (C \rightarrow B))$

$(A2)((B \rightarrow (C \rightarrow D)) \rightarrow ((B \rightarrow C) \rightarrow (B \rightarrow D)))$

$(A3)(((\lnot C) \rightarrow (\lnot B)) \rightarrow (((\lnot C) \rightarrow B) \rightarrow C)) $

I'm trying to prove that $\vdash(\lnot B \rightarrow B) \rightarrow B$

I've tried doing the following, using instances of the above:

1. (A2) - $(((\lnot B) \rightarrow (B \rightarrow ((\lnot B))) \rightarrow (((\lnot B) \rightarrow B) \rightarrow ((\lnot B) \rightarrow (\lnot B))))$

2. (A1) - $((\lnot B) \rightarrow (B \rightarrow (\lnot B)))$

3. (2,3 MP) - $(((\lnot B) \rightarrow B) \rightarrow ((\lnot B) \rightarrow (\lnot B)))$

4. (A3) - $(((\lnot B) \rightarrow (\lnot B)) \rightarrow (((\lnot B) \rightarrow B)) \rightarrow B))$

First off, I know this is quite simple stuff but I can't for the life of me find a way to find an antecedent to 4. using the above schema. So I'm wondering if there's something that's obviously incorrect about the process that I'm using? Is my substitution of a $B$ wf with a $(\lnot B)$ wf okay? I'm using Mendelson's book btw

Answer 1

Let $D=B$ in $(A2)$ \begin{eqnarray*} ((B \rightarrow (C \rightarrow B)) \rightarrow ((B \rightarrow C) \rightarrow (B \rightarrow B))) \end{eqnarray*} The first clause is true ... its $(A1)$ ... so by modus ponens \begin{eqnarray*} ((B \rightarrow C) \rightarrow (B \rightarrow B)) \end{eqnarray*} Now sub $ C \rightarrow B$ for $C$ \begin{eqnarray*} ((B \rightarrow (C \rightarrow B)) \rightarrow (B \rightarrow B)) \end{eqnarray*} Again the first clause is true ... its $(A1)$ ... so by modus ponens \begin{eqnarray*} (B \rightarrow B) \end{eqnarray*} Now sub $ \lnot B $ for $B$ ... so \begin{eqnarray*} (\lnot B \rightarrow \lnot B) \end{eqnarray*} So ... your fourth line & MP will give you the required result.

Answer 2

Another approach, you can establish

$$X \to Y \vdash (R \to X) \to (R \to Y)$$

Using only A1 and A2. Then use that schema to establish

$$\lnot B \to B \vdash (\lnot B \to \lnot B) \to (\lnot B \to B)$$

Then with A3 as $$(\lnot B \to \lnot B) \to (\lnot B \to B) \vdash B$$

And just stitch things together.