Prove this $\vdash_{_L}\mathscr{\left((\neg B)\rightarrow B\right)\rightarrow B}$

Question

The axioms of L are:

$\mathrm {(A1)} \quad \mathscr{\left(B\to\left(C\to B\right)\right)} \\ \mathrm {(A2)} \quad \mathscr{\left(\left(B\to\left(C\to D\right)\right)\to \left(\left(B \to C \right)\to \left(B \to D \right)\right)\right) }\\ \mathrm{(A3)}\;\;\; \mathscr{\left(\left(\left(\neg C \right)\to \left(\neg B \right)\right) \;\;\to \;\left(\left(\left(\neg C \right)\to B \right)\to C \right)\right)}$

What I understand is that $\mathscr{(B \to D) = \,\left((\neg B\to B)\to B\,\right)}$ must be equal, so $\mathscr{B}$ becomes $((\neg \mathscr{B})) \to \mathscr{B})$, and $\mathscr{D}$ becomes $\mathscr{B}$

Please write the proof in details

So, I write what I know:

$$\mathscr{\left\{\left((\neg B) \to B \right)\to(C\to B)\right\}\to \left\{(((\neg B) \to B \right)\to C)\to \left(((\neg B) \to B \right)\to B)\}} \;(A2)$$

I cannot go further .

Answer 1

For what I suspect would be the intended theorem, I don't know why you've started with a form of axiom 2. And I don't know why you seem to have concluded that any proof will begin with that axiom, or even have that axiom as you've used it. Let's substitute B for C in axiom (3), and please excuse me using plainer letters.

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

The consequent is ((($\lnot$B)$\rightarrow$B)$\rightarrow$B), which I suspect you seek to prove. The antecedent is (($\lnot$B)$\rightarrow$($\lnot$B)).

Now can you construct a proof?

Answer 2

I could be misunderstanding the context of your question, but it should not be the case that the two formulae $B\rightarrow D$ and $(\neg B \rightarrow B)\rightarrow B$ are equivalent, as the first is false when $B$ is true and $D$ is false, and the second is a tautology.

That being said, why does this not just follow from the truth table? You are trying to prove that something is a tautology, and there is only one atom to tabulate over.

Answer 3

Please allow me to use some more readable symbols.

First, let's show that $\vdash_L \varphi \rightarrow \varphi$ (ID):

$1. \varphi \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi) \quad (A1)$

$2. (\varphi \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi)) \rightarrow ((\varphi \rightarrow (\varphi \rightarrow \varphi)) \rightarrow (\varphi \rightarrow \varphi)) \quad (A2)$

$3. (\varphi \rightarrow (\varphi \rightarrow \varphi)) \rightarrow (\varphi \rightarrow \varphi) \quad MP \ 1,2$

$4. \varphi \rightarrow (\varphi \rightarrow \varphi)\quad (A1)$

$5. \varphi \rightarrow \varphi \quad MP \ 3,4$

Now you can prove $\neg \varphi \rightarrow \varphi \vdash_L \varphi$:

$1. \neg \varphi \rightarrow \varphi \quad Premise$

$2. \neg \varphi \rightarrow \neg \varphi \quad ID$

$3. (\neg \varphi \rightarrow \neg \varphi) \rightarrow ((\neg \varphi \rightarrow \varphi) \rightarrow \varphi) \quad (A3)$

$4. (\neg \varphi \rightarrow \varphi) \rightarrow \varphi \quad MP 2,3$

$5. \varphi \quad MP 1,4$

By the Deduction Theorem, we therefore have $\vdash_L (\neg \varphi \rightarrow \varphi) \rightarrow \varphi $