Prove $\lnot \lnot B$ Prove: $\lnot \lnot B$ from $\lnot \lnot A \implies \lnot \lnot B, \lnot(A \implies B) $
I cant use excluded middle: $B \lor \lnot B$
So I choose $\lnot B$ as hypothesis and will try to get $B$ which will prove $\lnot \lnot B$
$1. \lnot B$ hypothesis
$2. \lnot \lnot A \implies \lnot \lnot B$ hypothesis
$3. \lnot(A \implies B)$ hypothesis
Any idea what to do next? I have tried something like this:
$4. \lnot(A \implies B) \implies ((A \implies B) \implies B)$ axiom
$5. (A \implies B) \implies B$ MP(4, 3)
Now to get B I need $A \implies B$ which is imposible to get in this proof so this is clearly not the way to go.
 A: I'll try to prove it in intuitionistic logic (that is, I'll try that without excluded middle.)
Lemma. It is a theorem of intuitionistic logic:
$$\lnot p\lor q\to (p\to q)$$
Proof of this lemms is not difficult: if $\lnot p$ holds, then $p\to q$ since $p\to \bot$ and $\bot \to q$ and if $q$ holds then $p\to q$ since $p,q\vdash q$ and deduction theorem.
In addition, you can check that these theorems are hold in intuitionistic logic:
(a) $\lnot\lnot\lnot p\to\lnot p$ (so $\lnot p\leftrightarrow \lnot\lnot\lnot p$)
(b) $(p\to q)\to (\lnot q\to\lnot p)$
so $\lnot \lnot A\to\lnot\lnot B$ is equivalent to $\lnot B\to\lnot A$. So we just check that
$$\lnot B\to\lnot A,\lnot(A\to B),\lnot B\vdash \bot.$$
But since $\lnot B\to\lnot A$ and $\lnot B$ implies $\lnot A$ and it implies $\lnot A\lor B$. But by lemma, it gives $A\to B$. We know that $A\to B$ and $\lnot(A\to B)$ are contradictory (without excluded middle!) Therefore, by deduction theorem we get
$$\lnot B\to\lnot A,\lnot(A\to B),\vdash \lnot B\to \bot$$
and we know that $p\to\bot$ and $\lnot p$ are equivalent.
A: I'll give you a solution equivalent to Tetori's one in Natural Deduction :
1) $B$ --- assumed [a]
2) $A \rightarrow B$ --- from 1) by $\rightarrow$I
3) $\lnot (A \rightarrow B)$ --- premise [1]
4) $\bot$ --- from 2)-3) by $\rightarrow$E
5) $\lnot B$ --- from 1) and 4) by $\rightarrow$I, discharging assumption [a]
6) $A$ --- assumed [b]
7) $\lnot A$ --- assumed [c]
8) $\bot$ --- from 6)-7) by $\rightarrow$E
9) $B$ --- from 8) by $\bot$E
10) $A \rightarrow B$ --- from 6)-9) by $\rightarrow$I, discharging assumption [b]
11) $\bot$ --- from 10)-3) by $\rightarrow$E
12) $\lnot \lnot A$ --- from 7)-11) by $\rightarrow$I, discharging assumption [c]
13) $\lnot \lnot A \rightarrow \lnot \lnot B$ --- premise [2]
14) $\lnot \lnot B$ --- from 12)-13) by $\rightarrow$E


$\lnot (A \rightarrow B), \lnot \lnot A \rightarrow \lnot \lnot B \vdash \lnot \lnot B$ --- from 3), 13) and 14).


