# Intuitionistic logic and derivation

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?

• The second sequence also has one formula on the right, which is a conjunction $A\land B$. Nov 1, 2018 at 20:17
• It's probably also worth noting that multiple formulas on the right (which, as Berci states, is not what's happening here) are usually joined disjunctively. Nov 1, 2018 at 20:30
• I'll try to explain me better. I had this exercise: Only one of the following sequents is derivable in Intuitionistic Logic: exhibit a derivation of it in G.IL. A ∧ B ↔ ¬(¬A ∨ ¬B) (where ↔ is intended as the "both direction sequent". It follows we have 2 statement to prove. The solution was that only A ∧ B ⊢ ¬(¬A ∨ ¬B) is derivable. I'm trying to understand why Nov 1, 2018 at 20:31
• I wrongly assumed that the problem was the initial count of formula after the sequent thinking that the first expression had count = 1 and the second one count > 1. But I see right now that the problem occurs during the actual proof of the expression. Where we end up with statement of this type ¬¬A⊢A that is not provable in an IL environment by the non-application of the law of excluded middle Nov 1, 2018 at 23:19
• Indeed, it is not about the sequent calculus. Intuitionistic Logic accepts most of the rules of inference that build Classical Logic, with the exceptions being the Law of Excluded Middle and its coprovable rules. This means that you may introduce negation, but cannot eliminate double negations. So most classical equivalences can only be constructively proven in one direction of entailment. Nov 1, 2018 at 23:27

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.
$$\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.
• Think about why you can't prove $\neg \neg A \vdash A$ in your favoured intuitionist sequent calculus ... Nov 1, 2018 at 21:30