It is necessary to prove the derivability: $\vdash((\lnot B \to B) \to \lnot \lnot B)$.
My steps:
$\lnot B \to B \vdash \lnot \lnot B$
1)$\lnot B \to B$ - hypothesis
2)$(((\lnot B) \to B)) \to (((\lnot B) \to B) \to \lnot \lnot B)$ (A3)
3)$(((\lnot B) \to \lnot \lnot B) \to \lnot \lnot B)$ (1,2 MP)
But then I don't understand what to do.

  • $\begingroup$ Can you list the precise axioms you're using? It seems it's a Hilbert calculus, but different textbooks may use different names for the axioms... $\endgroup$ Oct 27 '21 at 21:51

Your application of A3 seems problematic, you can do a more careful inspection to see is your step 2) really correct by invoking A3 of your system, which seems Hilbert $H_2$ axiom system:

A3: $(\neg A\to \neg B)\to ((\neg A\to B)\to A)$

One way to proceed is to use proof by negation, assume $\lnot B$, then using MP you can easily get $B$ and clearly you arrive at $\bot$, a contradiction. So you then can safely conclude $(\lnot B \to B) \to \lnot \lnot B$.

  • $\begingroup$ Sorry, I don't understand how to use the negation proof, could you explain? $\endgroup$
    – Rey Legar
    Oct 26 '21 at 14:30
  • $\begingroup$ @ReyLegar See reference post in this site here. Hope it helps. It's a common proof method applicable to both classical and intuitionistic logics. $\endgroup$
    – mohottnad
    Oct 26 '21 at 14:36

Not the answer you're looking for? Browse other questions tagged or ask your own question.