Prove $\lnot \lnot B$

Question

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.

Answer 1

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.

Answer 2

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).