Prove $\vdash (\lnot B \rightarrow \lnot A) \rightarrow (( \lnot B \rightarrow A) \rightarrow B)$

Give a hilbert style proof

$$ \vdash (\lnot B \rightarrow \lnot A) \rightarrow (( \lnot B \rightarrow A) \rightarrow B)$$

How could I prove it ? When I apply deduction theorem, do I take $ ((\lnot B \rightarrow \lnot A) \rightarrow ( \lnot B \rightarrow A)) $ as a whole and move it to the left side because the parentheses or I can split it and do it like the following :

$$ (\lnot B \rightarrow \lnot A ) , (\lnot B \rightarrow A ) \vdash B$$

Lists of axioms and theorems.

Solution 1:

Basically, we can use 2.4.11 Theorem : $\vdash B \rightarrow A \equiv \lnot B \lor A$ [page 70] and using 2.4.4 Theorem (Double Negation) : $\vdash \lnot \lnot A \equiv A$ [page 67] (and Leibniz) to have :

$\vdash (\lnot B \rightarrow A) \equiv (B \lor A)$.

In the same way :

$\vdash (\lnot B \rightarrow \lnot A) \equiv (B \lor \lnot A)$.

Now we apply 2.5.5 Corollary : $A \lor B, \lnot A \lor B \vdash B$ [page 80], to get :

$(\lnot B \rightarrow \lnot A), (\lnot B \rightarrow A) \vdash B$.

Ex 20, page 109, ask to prove it using "the deduction theorem and resolution"; this means to apply, after the two initial transformations, 2.5.4 Theorem (Cut Rule) [page 79] : $A \lor B, \lnot A \lor C \vdash B \lor C$.

In this way, we get :

$(\lnot B \rightarrow \lnot A), (\lnot B \rightarrow A) \vdash B \lor B$.

The result follows by Idempotency of $\lor$ [page 43] and with the application of the Deduction Theorem twice :

$\vdash (\lnot B \rightarrow \lnot A) \rightarrow ((\lnot B \rightarrow A) \rightarrow B) $.