It is my first approach to intuitionistic logic (IL) and, even if I understand the principle behind it, I struggle understanding when a sequent is derivable in IL and when is not. I know that IL allows only one formula "on the right" of the sequent " ⊢ ". But then I also know that:
$A \land B \vdash \lnot (\lnot A \lor \lnot B)$ is derivable in IL
$\lnot(\lnot A \lor \lnot B) \vdash A \land B$ is not derivable in IL
Why is this the case? Why the first sequent has only one formula to the right and the second sequent has more than one?
It might help to develop your intuitions(!) here if you first consider how we derive $A$ from $\neg(\neg A \lor \neg B)$ in a classical natural deduction framework.
The obvious line of proof goes like this:
$\quad \neg(\neg A \lor \neg B)\\ \quad \quad \quad | \quad \neg A \\ \quad \quad \quad | \quad (\neg A \lor \neg B)\\ \quad \quad \quad | \quad \bot \\ \quad \neg\neg A\\ \quad A$
But ahah! The last step is inadmissible in intuitionistic logic, and so the proof fails there. We can't derive $A$ in intuitionistic logic (nor can we derive $B$, nor a fortiori their conjunction). We can derive $(\neg\neg A \land \neg\neg B)$ but can't get rid of the dratted double negations.