2
$\begingroup$

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?

$\endgroup$
6
  • 1
    $\begingroup$ The second sequence also has one formula on the right, which is a conjunction $A\land B$. $\endgroup$
    – Berci
    Nov 1, 2018 at 20:17
  • 1
    $\begingroup$ 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. $\endgroup$ Nov 1, 2018 at 20:30
  • $\begingroup$ 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 $\endgroup$ Nov 1, 2018 at 20:31
  • 1
    $\begingroup$ 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 $\endgroup$ Nov 1, 2018 at 23:19
  • 1
    $\begingroup$ 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. $\endgroup$ Nov 1, 2018 at 23:27

1 Answer 1

3
$\begingroup$

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.

$\endgroup$
4
  • $\begingroup$ I think I got it. Even because we couldn't "move" the formula ¬(¬A∨¬B) to the right of the sequent because otherwise we end up with two formula to the right, like this: ⊥ ⊢ A ∧ B, (¬A ∨ ¬B) that is not admissible. Is that right? $\endgroup$ Nov 1, 2018 at 21:02
  • $\begingroup$ Think about why you can't prove $\neg \neg A \vdash A$ in your favoured intuitionist sequent calculus ... $\endgroup$ Nov 1, 2018 at 21:30
  • 1
    $\begingroup$ I know that you can't prove it because we assume using IL that the "tertium non datur" or "middle excluded" it's not true. so we cannot prove ¬¬A⊢A. $\endgroup$ Nov 1, 2018 at 21:34
  • $\begingroup$ Yes. The law of excluded middle and rule of double negation elimination are coprovable: you can prove one if and only if you admit the other. @CraigMontevecchi $\endgroup$ Nov 1, 2018 at 22:48

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .